Re: [Haskell-cafe] On the purity of Haskell
On Dec 29, 2011, at 2:16 PM, Steve Horne wrote: Of course you can extract values out of IO actions to work with them - the bind operator does this for you nicely, providing the value as an argument to the function you pass to the right-hand argument of the bind. But that function returns another IO action anyway - although you've extracted a value out and the value affects a computation, all you can do with it in the long run is return another IO action. Even so, that value can only be extracted out at run-time, after the action is executed. So, consider the following... getAnIntFromTheUser :: IO Int From a pure functional point of view, that should return the same action every time. Well, the partially evaluated getAnIntFromTheUser has the same structure each time - but the actual Int packaged inside the action isn't decided until runtime, when the action is executed. At compile-time, that action can only be partially evaluated - the final value OF THE ACTION depends on what Int the user chooses to give because that Int is a part of the action value. Howdy Steve, You are correct that Haskell is not, strictly speaking pure - no language that does anything useful (e.g. IO) can possibly be purely functional. But there seems to be a certain amount of language policing in the Haskell community - pure means what we mean when we use it to describe Haskell, and don't you dare use it otherwise. Ok, but that just leads to riddles like when is a pure language impure? A: when it isn't pure. Several posts to this thread have insisted that IO values are really values like any other values, can be reasoned about, etc. and that the process yielding the value (including possible side-effects) is therefore irrelevant or secondary or etc.. Well, you can reason about them indirectly, by virtue of their types, but you can't reason about the values themselves, because they are non-deterministic and undecidable. And the process clearly is relevant, since it motivates the use of the value in the first place. Not much point in a pure IO value that does not cause IO, and if the side effects were truly irrelevant to the use of such values then we would not need monads to order their evaluation. So the argument that all of Haskell is immaculately, purely functional is pure hooey, for me at least. I completely understand what people mean when they talk like this; I just think it's a misuse of English. Now one way of understanding all this is to say that it implicates the static/dynamic (compile-time/run-time) distinction: you don't know what e.g. IO values are until runtime, so this distinction is critical to distinguishing between pure and impure. I gather this is your view. I think that is reasonable, but with the caveat that it must be at the right level of abstraction. I don't think ASTs etc. enter into it - those are implementation techniques, and the only generalization we can apply to compilers is that they do implement the language definition, not how they do it (not all C compilers use ASTs). The right level of abstraction (IMHO) is the distinction between atemporality and temporality. The functional stuff is atemporal, which means among other things that evaluation is unordered (evaluation being a temporal process). Adding IO etc. capabilities to the purely functional fragment of a language infects it with temporality. But we can model temporality using order, so we can dispense with the notion of run-time and say that IO etc. stuff adds an ordered fragment to the unordered fragment. One goal of the language is then to enforce a strict correspondence between the order of events outside the program (e.g. keystrokes) and events inside the program (getchar). The beauty of the monad solution is not that it magically transforms non-functional stuff like IO into functional stuff, but that it exploits type discipline to make such operations *mimic* purely functional stuff in a sense - but only at the level of typing. Impure operations then have purely functional type discipline while remaining essentially non-functional. So I think of Haskell as a quasi-pure or hybrid language. C on the other hand is totally impure (except for predefined constants like '1'). For totally pure languages you have to look elsewhere, e.g. logics - there are no pure programming languages. It's fairly easy to grasp the point by going back to Turing's original insight. The cornerstone of his ideas was not the machine but the human calculator working with pencil and paper, finite memory, etc. So to see the diff all you have to do is think about what a human does with a problem (program) written on paper. Give the human calculator a computable task - add 2+2 - and you can be confident you will receive a definite answer in a finite amount of time. Lard this with a non-computable step - add 2 + 2 + getInt - and all bets are off. In this case,
Re: [Haskell-cafe] On the purity of Haskell
On Dec 30, 2011, at 10:34 AM, Artyom Kazak wrote: Gregg Reynolds d...@mobileink.com писал(а) в своём письме Fri, 30 Dec 2011 17:23:20 +0200: Regarding side-effects, they can be (informally) defined pretty simply: any non-computational effect caused by a computation is a side-effect. I wonder: can writing to memory be called a “computational effect”? If yes, then every computation is impure. If no, then what’s the difference between memory and hard drive? Great question! It suggests that the line between computation and its side effects is not as clear-cut as we (well, I) thought. If computations are Platonistic, mathematico-logical things, then is actual computation a side-effect of the Platonic Idea? Heh heh. By the way, the Data.HashTable is in IO monad. Is it impure? Would it be pure if designers had chosen to use ST instead? Dunno, somebody else will have to answer that one. -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 30, 2011, at 10:19 AM, Conal Elliott wrote: On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus apfel...@quantentunnel.de wrote: The function f :: Int - IO Int f x = getAnIntFromTheUser = \i - return (i+x) is pure according to the common definition of pure in the context of purely functional programming. That's because f 42 = f (43-1) = etc. Put differently, the function always returns the same IO action, i.e. the same value (of type IO Int) when given the same parameter. Two questions trouble me: How can we know whether this claim is true or not? time t: f 42 (computational process implementing func application begins…) t+1: keystroke = 1 t+2: 43 (… and ends) time t+3: f 42 t+4: keystroke = 2 t+5: 44 Conclusion: f 42 != f 42 (This seems so extraordinarily obvious that maybe Heinrich has something else in mind.) -Gregg___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 30, 2011, at 11:04 AM, Colin Adams wrote: On 30 December 2011 16:59, Gregg Reynolds d...@mobileink.com wrote: On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus apfel...@quantentunnel.de wrote: The function f :: Int - IO Int f x = getAnIntFromTheUser = \i - return (i+x) is pure according to the common definition of pure in the context of purely functional programming. That's because f 42 = f (43-1) = etc. Put differently, the function always returns the same IO action, i.e. the same value (of type IO Int) when given the same parameter. time t: f 42 (computational process implementing func application begins…) t+1: keystroke = 1 t+2: 43 (… and ends) time t+3: f 42 t+4: keystroke = 2 t+5: 44 Conclusion: f 42 != f 42 (This seems so extraordinarily obvious that maybe Heinrich has something else in mind.) This seems such an obviously incorrect conclusion. f42 is a funtion for returning a program for returning an int, not a function for returning an int. My conclusion holds: f 42 != f 42. Obviously, so I won't burden you with an explanation. ;) -Gregg___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 30, 2011, at 11:20 AM, Colin Adams wrote: On 30 December 2011 17:17, Gregg Reynolds d...@mobileink.com wrote: On Dec 30, 2011, at 11:04 AM, Colin Adams wrote: On 30 December 2011 16:59, Gregg Reynolds d...@mobileink.com wrote: On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus apfel...@quantentunnel.de wrote: The function f :: Int - IO Int f x = getAnIntFromTheUser = \i - return (i+x) is pure according to the common definition of pure in the context of purely functional programming. That's because f 42 = f (43-1) = etc. Conclusion: f 42 != f 42 (This seems so extraordinarily obvious that maybe Heinrich has something else in mind.) This seems such an obviously incorrect conclusion. f42 is a funtion for returning a program for returning an int, not a function for returning an int. My conclusion holds: f 42 != f 42. Obviously, so I won't burden you with an explanation. ;) -Gregg Your conclusion is clearly erroneous. proof: f is a function, and it is taking the same argument each time. Therefore the result is the same each time. That's called begging the question. f is not a function, so I guess your proof is flawed. It seems pretty clear that we're working with different ideas of what constitutes a function. When I use the term, I intend what I take to be the standard notion of a function in computation: not just a unique mapping from one input to one output, but one where the output is computable from the input. Any function that depends on a non-computable component is by that definition not a true function. For clarity let's call such critters quasi-functions, so we can retain the notion of application. Equality cannot be defined for quasi-functions, for obvious reasons. f is a quasi-function because it depends on getAnIntFromUser, which is not definable and is obviously not a function. When applied to an argument like 42, it yields another quasi-function, and therefore f 42 = f 42 is false, or at least unknown, and the same goes for f 42 != f 42 I suppose. -Gregg___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 30, 2011, at 11:11 AM, Chris Smith wrote: time t: f 42 (computational process implementing func application begins…) t+1: keystroke = 1 t+2: 43 (… and ends) time t+3: f 42 t+4: keystroke = 2 t+5: 44 Conclusion: f 42 != f 42 That conclusion would only follow if the same IO action always produced the same result when performed twice in a row. That's obviously untrue, so the conclusion doesn't follow. What you've done is entirely consistent with the fact that f 42 = f 42... it just demonstrates that whatever f 42 is, it doesn't always produce the same result when you o it twice. What Conal is getting at is that we don't have a formal model of what an IO action means. Right, and my little counter-example is intended to support that. Nevertheless, we know because f is a function We do? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 30, 2011, at 11:19 AM, Heinrich Apfelmus wrote: Conal Elliott wrote: Heinrich Apfelmus wrote: The function f :: Int - IO Int f x = getAnIntFromTheUser = \i - return (i+x) is pure according to the common definition of pure in the context of purely functional programming. That's because f 42 = f (43-1) = etc. Put differently, the function always returns the same IO action, i.e. the same value (of type IO Int) when given the same parameter. Two questions trouble me: How can we know whether this claim is true or not? What does the claim even mean, i.e., what does the same IO action mean, considering that we lack a denotational model of IO? I think you can put at least these troubles to rest by noting that f 42 and f (43-1) are intentionally equal, even though you're not confident on their extensional meaning. (I think you meant intensionally). Ok, I think I can go with that, something like f 42 means the sum of 42 and the user input. And I suppose one could argue that the extension of f is well-defined as the set of integer pairs. But that does not make f a (computable) function, because the mapping from domain to co-domain remains undefined, dependent as it is on IO. -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 30, 2011, at 11:43 AM, Conal Elliott wrote: roof: f is a function, and it is taking the same argument each time. Therefore the result is the same each time. That's called begging the question. f is not a function, so I guess your proof is flawed. It seems pretty clear that we're working with different ideas of what constitutes a function. When I use the term, I intend what I take to be the standard notion of a function in computation: not just a unique mapping from one input to one output, but one where the output is computable from the input. Any function that depends on a non-computable component is by that definition not a true function. For clarity let's call such critters quasi-functions, so we can retain the notion of application. Equality cannot be defined for quasi-functions, for obvious reasons. f is a quasi-function because it depends on getAnIntFromUser, which is not definable and is obviously not a function. When applied to an argument like 42, it yields another quasi-function, and therefore f 42 = f 42 is false, or at least unknown, and the same goes for f 42 != f 42 I suppose. -Gregg Please don't redefine function to mean computable function. Besides distancing yourself from math, I don't think doing so really helps your case. No redefinition involved, just a narrowing of scope. I assume that, since we are talking about computation, it is reasonable to limit the discussion to the class of computable functions - which, by the way, are about as deeply embedded in orthodox mathematics as you can get, by way of recursion theory. What would be the point of talking about non-computable functions for the semantics of a programming language? And on what do you base your claim that getAnIntFromUser is not definable? Sorry, not definable might a little strong. Not definable in the way we can define computable functions work better? In any case I think you probably see what I'm getting at. Or that applying it (what?) to 42 gives a quasi-function? I can't think of a way to improve on what I've already written at the moment - it too would depend on IO - so if my meaning is not clear, so be it. Wait, here's another way of looking at it. Think of IO actions as random variables. So instead of getAnIntFromUser, use X as an integer random variable yielding something like: f :: Int - IO Int f x = X = \i - return (i+x) I would not call this f a function because I don't think it answers to the commonly accepted definition of a function. Ditto for the result of applying it to 42. Others obviously might consider it a function. De gustibus non set disputandem. -Gregg -Gregg___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 30, 2011, at 11:21 AM, Conal Elliott wrote: And I also raised a more fundamental question than whether this claim of sameness is true, namely what is equality on IO? Without a precise consistent definition of equality, the claims like f 42 == f (43 - 1) are even defined, let alone true. And since the conversation is about Haskell IO, I'm looking for a definition that applies to all of IO, not just some relatively well-behaved subset like putchar/getchar+IORefs+threads. Well, you'll no doubt be glad to know I think I've said about all I need to say on this topic, but I'll add one more thing. Threads like this I often find useful even when I disagree vehemently with various parties. In this case an old idea I'd forgotten about was suddenly dislodged by the discussion. A few years ago - the last time I got involved in a discussion on Haskell semantics - I spent some time sketching out ideas for using random variables to provide definitions (or at least notation) for stuff like IO. I'm not sure I could even find the notes now, but my recollection is that it seemed like a promising approach. One advantage is that this eliminates the kind of informal language (like user input) that seems unavoidable in talking about IO. Instead of defining e.g. readChar or the like as an action that does something and returns an char (or however standard Haskell idiom puts it), you can just say that readChar is a random char variable and be done with it. The notion of doing an action goes away. The side-effect of actually reading the input or the like can be defined generically by saying that evaluating a random variable always has some side-effect; what specifically the side effect is does not matter. I mention this as a possible approach for anybody looking for a better way of accounting for IO in Haskell. Cheers, Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 29, 2011, at 9:16 AM, Donn Cave wrote: Quoth Gregg Reynolds d...@mobileink.com, On Wed, Dec 28, 2011 at 2:44 PM, Heinrich Apfelmus apfel...@quantentunnel.de wrote: The beauty of the IO monad is that it doesn't change anything about purity. Applying the function bar :: Int - IO Int to the value 2 will always give the same result: bar 2 = bar (1+1) = bar (5-3) Strictly speaking, that doesn't sound right. Look again at the sentence you trimmed off the end: Of course, the point is that this result is an *IO action* of type IO Int, it's not the Int you would get when executing this action. I believe that more or less points to the key to this discussion. If it didn't make sense to you, or didn't seem relevant to the question of pure functions, then it would be worth while to think more about it. Ok, let's parse it out. …it's not the int you would get 'when executing this action. Close, but no cooky: it's not any kind of int at all (try doing arithmetic with it). IO Int is a piece of rhetoric for the mental convenience of the user; Haskell does not and cannot know what the result of an IO action is, because it's outside the scope of the language (and computation). (The Int part of IO Int refers to the input, not the output; it's just a sort of type annotation.) It's not even a computation, unless you want to take a broad view and include oracles, interaction, etc. in your definition of computation. -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Wed, Dec 28, 2011 at 2:44 PM, Heinrich Apfelmus apfel...@quantentunnel.de wrote: The beauty of the IO monad is that it doesn't change anything about purity. Applying the function bar :: Int - IO Int to the value 2 will always give the same result: bar 2 = bar (1+1) = bar (5-3) Strictly speaking, that doesn't sound right. The result of an IO operation is outside of the control (and semantics) of the Haskell program, so Haskell has no idea what it will be. Within the program, there is no result. So Int - IO Int is not really a function - it does not map a determinate input to a determinate output. The IO monad just makes it look and act like a function, sort of, but what it really does is provide reliable ordering of non-functional operations - invariant order, not invariant results. To respond to original post: no language that supports IO can be purely functional in fact, but with clever design it can mimic a purely functional language. Cheers Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 29, 2011, at 11:29 AM, Antoine Latter wrote: On Thu, Dec 29, 2011 at 11:14 AM, Gregg Reynolds d...@mobileink.com wrote: On Dec 29, 2011, at 11:01 AM, Iustin Pop wrote: And to clarify better my original email: yes, (bar x) always gives you back the same IO action; More precisely: the same *type*. I'm confused - what do you mean by type? I don't think that Iustin's statement needs any sort of qualifier - (bar x) always returns the same IO action when called with the same value for x, no matter how many times you call it. Maybe it doesn't need qualification, but my guess is that most people read IO Int to mean something like IO action of type int. But computation does not involve action. Action is just an explanatory device - a kind of macguffin - to help explain what's going on with IO, which is non-computational. But it is a type, and in Haskell it's all about the types. IO Int is a type designator, not an action designator. A minor point maybe, but germane to the original post (I hope). -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 29, 2011, at 11:01 AM, Iustin Pop wrote: On Thu, Dec 29, 2011 at 05:55:24PM +0100, Iustin Pop wrote: On Thu, Dec 29, 2011 at 05:51:57PM +0100, Jerzy Karczmarczuk wrote: Iustin Pop:: In practice too: bar _ = do s- readFile /tmp/x.txt return (read s) Once you're in a monad that has 'state', the return value doesn't strictly depend anymore on the function arguments. Nice example. PLEASE, show us the trace of its execution. Then, the discussion might be more fruitful Sorry? I did the same mistake of misreading the grand-parent's IO Int vs. Int, if that's what you're referring to. Otherwise, I'm confused as what you mean. And to clarify better my original email: yes, (bar x) always gives you back the same IO action; More precisely: the same *type*. but the results of said IO action are/can be different when executed. -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 29, 2011, at 12:33 PM, Donn Cave wrote: Quoth Gregg Reynolds d...@mobileink.com, .. A minor point maybe, but germane to the original post (I hope). It isn't - I mean, I'm not really sure what your point is, but the example really returns the same IO value, not just one of the same type. Consider an example with implementation: wint :: Int - IO Int wint a = let s = show a in do putStr s return (length s) Now the expression wint 994 is a value of type IO Int, and any instance of that expression is the same value Ok, but if that were all there is to it we would not need monads. I guess it may boil down to a matter of taste in definition and exposition - to me any account of stuff like IO Int that omits mention of the fact that, well, IO is involved, is incomplete. But then I like the theoretical and even philosophical side of things where others tend to want to get on with writing useful code. ;) And the original post was if I remember about purity/impurity etc. - an action is not the same as the action's result. Nor is a computation the same as the computation's result. The critical difference is that computations are deterministic processes, and actions (IO, rand, etc.) are not. Therefore they are not functions, their evaluation must be ordered, and they cannot even in principle be fully modeled in purely functional terms. At least I don't see how they can. You can use this value in pure Haskell expressions with confidence. Because they are monadic, not because they are values like other values. -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On the purity of Haskell
On Dec 29, 2011, at 1:21 PM, Heinrich Apfelmus wrote: Why would IO Int be something special or mysterious? I don't know if it is special or mysterious, but I'm pretty sure IO is non-deterministic, non-computable, etc. In other words not the same as computation. It's an ordinary value like everything else; it's on the same footing as [Char], Maybe Int, Int - String, Bool, and so on. I see no difference between the list [1,2,3] :: [Int] and the action pick a random number between 1 and 6 :: IO Int . We'll have to agree to disagree - I see a fundamental difference. But that's ok, nothing says everybody has to agree on the One True Way to think about computing. Cheers, Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Category theory as a design tool
On Tue, Jun 21, 2011 at 11:30 PM, Arnaud Bailly arnaud.oq...@gmail.com wrote: (2nd try, took my gloves off...) Hello Café, I have been fascinated by Cat. theory for quite a few years now, as most people who get close to it I think. I am a developer, working mostly in Java for my living and dabbling with haskell and scala in my spare time and assuming the frustration of having to live in an imperative word. More often than not, I find myself trying to use constructs from FP in my code, mostly simple closures and typical data types (eg. Maybe, Either...). I have read with a lot of interest FPS (http://homepages.mcs.vuw.ac.nz/~tk/fps/) which exposes a number of OO patterns inspired by FP. Are there works/thesis/books/articles/blogs that try to use Cat. theory explicitly as a tool/language for designing software (not as an underlying formalisation or semantics)? Is the question even meaningful? You might try: Category Theory for Computing Sciencehttp://www.cwru.edu/artsci/math/wells/pub/ctcs.html (Barr and Wells) and Conceptual Mathematics: a first introduction to categorieshttp://books.google.com/books/about/Conceptual_mathematics.html?id=o1tHw4W5MZQC (Lawvere) Kinship and Mathematical Categories (by Lawvere) is also interesting. -Gregg Thanks in advance, Arnaud ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Category theory as a design tool
On Wed, Jun 22, 2011 at 2:59 PM, Arnaud Bailly arnaud.oq...@gmail.comwrote: Hello Greg and Alexander, Thanks for your replies. Funnily, I happen to own the 3 books you mentionned :-) My interest in category theory is a long standing affair... Note that owning a book, having read (most of) it and knowing a theory (or at least its principles and main concepts) is really quite a different thing from being able to apply it. Although I am certainly able to understand the Yoneda lemma, I am certainly unable to Well, you're way ahead of me. I don't even get adjunctions, to tell you the truth. By which I mean that I have no intuition about them; it's not so hard to understand the formal definition, but it's another thing altogether to grasp the deep significance. recognize the opportunity of using that knowledge to derive some new knowledge about something else. And being able to define a topoi is very different from being able to construct one or infer one out of a given category. This is an actual limitation of myself of course. Indeed. But I'll bet your next paycheck that eventually CT will replace set theory as the basic mode of thinking about math, even at elementary levels. It just awaits that brilliant writer who can connect the dots appropriately. Alexander's advice about using diagrams and simple notations is something I often try to do and something which most of the times end in writing a bunch of functions and data types in Haskell... What I am really looking for is a more systematic way of thinking about systems (or system fragments, or components) in a categorical way, perhaps starting with a bunch of arrows in some abstract category with objects as components and trying to infer new objects out of categorical consturctions which are made possible by the current diagrams (eg. what would be a pullback in such a category ? What would be its meaning ? Does the question itself have a meaning ?). Maybe this is really foggy and on the verge to fall into abstract nonsense... Long live abstract nonsense! Completely off topic: a few months ago I had an idea about using category theory to provide rigorous semantics for the web (esp. rdf stuff etc.) I'll probably never find time to work out the details, but it's a fun exercise in any case; if you want to mess around with applying CT to the real world maybe you can coem up with improvements. See http://blog.mobileink.com/2011/03/resource-token-exchange.html. It's a bit of a mess, and some of it I would radically revise, but it might give you some ideas, if you're interested in the semantic web thingee. Best regards, arnaud ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Python is lazier than Haskell
On Thu, Apr 28, 2011 at 11:38 PM, Ben Lippmeier b...@ouroborus.net wrote: On 27/04/2011, at 7:30 PM, Henning Thielemann wrote: If Haskell is great because of its laziness, then Python must be even greater, since it is lazy at the type level. Laziness at the value level causes space leaks, and laziness at the type level causes mind leaks. Neither are much fun. If the designers could find a way to support laziness at the programmer level I for one would be very grateful. -G ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad based on http://en.wikipedia.org/wiki/Monad_(category_theory)
On Mon, Jan 17, 2011 at 9:46 PM, C K Kashyap ckkash...@gmail.com wrote: I am not able to fully understand how those diagrams translate to haskell - I can guess that T^2 - T referes to things like concat operation but not able to relate it to bind. I found it useful to work out the correspondence between monoids and monads; lots of introductory texts on CT give the example of the category Mon so I won't bore you with an account here. Thinking about monoids and monads helped me move past element-centric thinking toward the arrow-centric way of thinking in CT. In particular it's helpful to work out how the mu operator of a monad (which composes arrows) is a kind of abstraction of monoid operators (which combine elements). What you end up with is the monad as a device you can use to make non-monoidal things behave like monoids - closure, associativity, identity. For bind, google around for Kleisli Category and Kleisli star. I think of the latter as a kind of hybrid of a function and a functor, although I'm not entirely sure that's correct. -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Denotational semantics for the lay man.
On Mon, Jan 17, 2011 at 12:55 PM, David Sankel cam...@gmail.com wrote: Hello All, I've recently had the opportunity to explain in prose what denotational semantics are to a person unfamiliar with it. I was trying to get across the concept of distilling the essence out of some problem domain. I wasn't able to get the idea across so I'm looking for some simple ways to explain it. Does anyone know of a way to explain what's the meaning and objective of distilling the essence without introducing more jargon. One thing that comes to mind is how Newton's equations for gravity were a distillation of the essence of the way things fall. A stick figure as an iconic image of a person serves as a symbol of person; i.e. it denotes person. It works because of the parts and their arrangement. Ditto for mathematical expressions: the whole is equal to the sum of its parts (and the way they are arranged.) The individual parts (e.g. the symbol '3') are not iconic, but the way the whole system works corresponds exactly with the way we imagine mathematical objects work. Google around for correspondence theory of truth and you might find some useful material. It might be useful to introduce Platonism (see wikipedia.) Also try boiling it down to compositionality, substitutability, and equality. It might also help to draw a contrast with what is not denotational. Denotational semantics depends essentially on the fiction of univocality, namely that every symbol has one delimited meaning: it means what it means, and nothing else. But in fact univocality is not possible even in theory; you cannot circumscribe the the proliferation of meanings. A simple example: 2+3 denotes (the same thing as) 5; it may also be taken to denote a computation that yields 5. But it does not denote the energy consumed in carrying out that computation. A horribly inefficient algorithm may have the same denotation as a very efficient one. Another way of putting it is that denotation is about extensionality to the exclusion of intensional meanings. Going beyond extensionality is where Category Theory enters the picture. HTH -Gregg Reynolds ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lambda Calculus: Bound and Free formal definitions
On Wed, Dec 29, 2010 at 9:22 PM, Mark Spezzano mark.spezz...@chariot.net.au wrote: Duh, Sorry. Yes, there was a typo the second one should read If E is a combination E1 E2 then X is bound in E if and only if X is bound in E1 or is bound in E2. Seems odd. I recommend you always work from at least three different texts. Here's Hindley and Seldinhttp://www.amazon.com/Lambda-Calculus-Combinators-Introduction-Roger-Hindley/dp/0521898854/ref=dp_ob_title_bk : An occurrence of a variable x in a term P is called - *bound* if it is in the scope of a \x in P (NB: using \ as lambda) - *bound and binding* iff it is the x in \x - *free* otherwise The tricky question is: bound to what, exactly? -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] OT: Monad co-tutorial: the Compilation Monad
This is a little off-topic, since it isn't specifically about Haskell, but since Haskell is the home of the monad tutorial it isn't completely irrelevant. The monad tutorial genre is well-known; it's often written somebody who has just learned the concept trying to explain it, often in highly imaginative terms (e.g. a monad is just like a giant squid, with special tentacles). I propose monad co-tutorial for attempts, often by an amateur (e.g. me) to work out how a monad appears in an unexpected place. In particular, I recently suffered through a few days of learning to deal with Ant and Maven2, which got me thinking about build systems in general, which got me thinking about the (meta-)language used in such systems, which got me thinking about What It's Really All About. Lo and behold - a monad! I think, anyway. The basic idea is that program texts (source or object code) are to programs as sentences are to propositions. Compilation transforms one representation into another. This can be viewed in terms of the unit natural transformation of a monad of transformations over program representations. The multiplication component captures the fact that program text transformations can be chained, as in macro expansion, phased optimization, etc. I'm not sure if this works, but it fits my somewhat limited idea of monads, so I wrote an article http://blog.mobileink.com/ about it and I'd appreciate any corrections. I expect if it does work somebody has already done something like it, so I would appreciate any pointers to more info. My real goal is to think about better language for software build systems, since what we have now is pretty weak, in my view. One thing that follows from thinking in terms of monads is that we can discard the notion of dependency of object code of source code in favor of a notion of equivalence (i.e. unit transform). My hunch is that thinking along such lines might lead to an improved metalanguage for build DSLs. Thanks, Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell is a scripting language inspired by Python.
On Thu, Nov 4, 2010 at 4:48 PM, Richard O'Keefe o...@cs.otago.ac.nz wrote: On 4/11/2010, at 9:08 PM, Stephen Tetley wrote: Did Haskell get significant whitespace from Python - doubtful as Python possibly wasn't visible enough at the time, but you never know. Python did not originate indentation-based syntax. Occam has it too. I first came across the idea in a rather old book which I *think* was by Reynolds. I had absolutely nothing to do with it. However, I must say that it is obvious to anybody properly schooled in philology and hermeneutics, to say nothing of theology and geometry, that both Python and Haskell stole their whitespace ideas from the medieval scribes who invented interword spaces. As is well known, the reason Roman computers never caught on is because they didn't use white space in their programming languages. For more info, see Space Between Words; The origins of silent reading by Paul Saenger, Stanford U Press, 1997. I'm not joking; anybody who enjoys thinking about computation will find it very enjoyable. It's one of those historical works that makes you realize that what you thought was trivial (e.g. whitespace) is actually of enormous import. Doesn't COBOL have significant layout anyway as an inspiration to both? Yes and no. What it actually has relates strongly to punched cards and is more like assemblers of the day. Columns 1 to 6 were for the sequence number. Column 7 is called the indicator area. Columns 8 to 11 are Area A. Certain structure keywords and labels must go in that area. Columns 12 to 72 are Area B. Normal statements go in that area. Indentation *within* area B has no significance whatever. Columns 73 to 80 have a name (the Identification Field) but And I thought I was the last mainframer alive! (I'm sure you'll agree calling COBOL an inspiration of Haskell might be a wee bit of a stretch.) Anyway, anybody who has ever wondered why 80 cols is a standard width now knows. -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Category Theory woes
On Thu, Feb 18, 2010 at 7:48 AM, Nick Rudnick joerg.rudn...@t-online.dewrote: IM(H??)O, a really introductive book on category theory still is to be written -- if category theory is really that fundamental (what I believe, due to its lifting of restrictions usually implicit at 'orthodox maths'), than it should find a reflection in our every day's common sense, shouldn't it? Goldblatt works for me. * the definition of open/closed sets in topology with the boundary elements of a closed set to considerable extent regardable as facing to an «outside» (so that reversing these terms could even appear more intuitive, or «bordered» instead of closed and «unbordered» instead of open), Both have a border, just in different places. As an example, let's play a little: Arrows: Arrows are more fundamental than objects, in fact, categories may be defined with arrows only. Although I like the term arrow (more than 'morphism'), I intuitively would find the term «reference» less contradictive with the actual intention, as this term Arrows don't refer. Categories: In every day's language, a category is a completely different thing, without the least Not necesssarily (for Kantians, Aristoteleans?) If memory serves, MacLane says somewhere that he and Eilenberg picked the term category as an explicit play on the same term in philosophy. In general I find mathematical terminology well-chosen and revealing, if one takes the trouble to do a little digging. If you want to know what terminological chaos really looks like try linguistics. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Category Theory woes
On Thu, Feb 18, 2010 at 1:31 PM, Daniel Fischer daniel.is.fisc...@web.dewrote: Am Donnerstag 18 Februar 2010 19:55:31 schrieb Nick Rudnick: Gregg Reynolds wrote: -- you agree with me it's far away from every day's common sense, even for a hobby coder?? I mean, this is not «Head first categories», is it? ;-)) With «every day's common sense» I did not mean «a mathematician's every day's common sense», but that of, e.g., a housewife or a child... Doesn't work. You need a lot of training in abstraction to learn very abstract concepts. Joe Sixpack's common sense isn't prepared for that. True enough, but I also tend to think that with a little imagination even many of the most abstract concepts can be illustrated with intuitive, concrete examples, and it's a fun (to me) challenge to try come up with them. For example, associativity can be nicely illustrated in terms of donning socks and shoes - it's not hard to imagine putting socks into shoes before putting feet into socks. A little weird, but easily understandable. My guess is that with a little effort one could find good concrete examples of at least category, functor, and natural transformation. Hmm, how is a cake-mixer like a cement-mixer? They're structurally and functionally isomorphic. Objects in the category Mixer? Both have a border, just in different places. Which elements form the border of an open set?? The boundary of an open set is the boundary of its complement. The boundary may be empty (happens if and only if the set is simultaneously open and closed, clopen, as some say). Right, that was what I meant; the point being that boundary (or border, or periphery or whatever) is not sufficient to capture the idea of closed v. open. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Linguistic hair-splitting
On Sat, Jan 30, 2010 at 1:24 AM, Conal Elliott co...@conal.net wrote: I call it an m or (more specifically) an Int m or a list of Int. For instance, a list or an Int list or a list of Int. - Conal On Wed, Jan 27, 2010 at 12:14 PM, Luke Palmer lrpal...@gmail.com wrote: On Wed, Jan 27, 2010 at 11:39 AM, Jochem Berndsen joc...@functor.nl wrote: Now, here's the question: Is is correct to say that [3, 5, 8] is a monad? In what sense would this be a monad? I don't quite get your question. I think the question is this: if m is a monad, then what do you call a thing of type m Int, or m Whatever. Luke Conal's is the most sensible approach - what do you call it amounts to what sort of a thing is it, and the best we can say in that respect is er, its a thing of type m Whatever. (My preference, if maximal explicitness is needed, is to say it's a token of its type; some say term of type m Whatever.) Trying to classify such a thing as value, object, computation, reduction etc. inevitably (and necessarily) leads to tail-chasing since those notions are all essentially equivalent. Plus they miss the essential point, which is the typing. Original poster would probably find Martin-Lof's philosophically-tinged writings very good on this - clear, reasonably simple, and revelatory, if you've never closely looked at intuitionistic logic before. Truth of a proposition, evidence of a judgment, validity of a proofhttp://www.jstor.org/pss/20116466is especially readable, as is On the meanings of the Logical Constants and the Justifications of the Logical Laws http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.html. Presents a completely new (to me) way of thinking about what is it, really? questions about computation, monads, etc., i.e. ask not what is it? but how do you know? or even how do you make it? The Stanford article on types and tokenshttp://plato.stanford.edu/entries/types-tokens/is also very enlightening in this respect. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Category Theory woes
On Tue, Feb 2, 2010 at 5:26 AM, Mark Spezzano mark.spezz...@chariot.net.auwrote: Hi all, Has anyone else found it frustratingly difficult to find details on easy-to-diget material on Category theory. The Chapter that I'm stuck on is actually labeled Preliminaries and so I reason that if I can't I've looked through at least a dozen. For neophytes, the best of the bunch BY FAR is Goldblatt, Topoi: the categorial analysis of logichttp://digital.library.cornell.edu/cgi/t/text/text-idx?c=math;cc=math;q1=Goldblatt;view=toc;idno=gold010. Don't be put off by the title. He not only explains the stuff, but he explains the problems that motivated the invention of the stuff. He doesn't cover monads, but he covers all the basics very clearly, so once you've got that down you can move to another author for monads. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] consulting and contracting
On Tue, Dec 15, 2009 at 3:19 PM, Anton van Straaten an...@appsolutions.comwrote: Without that advocacy, this client would have used Java by default. As it was, the first of I'd be interested in how you pulled that off. Enlightened client, or slick sales pitch? Where I work I would consider it a minor miracle just to get people to consider using a wiki for collaboration. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Why?
On Thu, Dec 10, 2009 at 9:13 AM, John D. Earle johndea...@cox.net wrote: Most of the discussion centers on the benefits of functional programming and laziness. Haskell is not merely a lazy functional language. It is a pure lazy functional language. I may need to explain what laziness is. Laziness is where you work through the logic in its entirely before acting on the result. In strict evaluation the logic is worked out in parallel with execution which doesn't make complete sense, but it does allow for an architecture that is close to the machine. Just to roil the waters a bit: no programming language can ever hope to be purely functional, for the simple reason that real computation (i.e. computation involving IO, interactivity) cannot be functional. Functional programming is an unfortunate misnomer. On the other hand, languages can be algebraic. The whole point is provability, not function-ness. More generally: judging by the many competing proposals addressing the issue of how to think formally about real computation (just google stuff like hypercomputation, interactive computation, etc.; Jack Copelandhttp://www.hums.canterbury.ac.nz/phil/people/copeland.shtml#articleshas lots of interesting stuff on this) is still an open question. Soare has three essential papers http://www.people.cs.uchicago.edu/%7Esoare/History/on the subject. I guess the moral of the story is that the concepts and the terminology are both still unstable, so lots of terms in common use are rather ill-defined and misleading (e.g. functional programming). Lazyness is just a matter of how one attaches an actual computation to an expression; a better term would be something like delayed evaluation or just-in-time computation. You don't have to work through any logic to have laziness. Just think about how one reads a mathematical text - you need not actually compute subformulae or even analyze them logically in order to work with them. This applies right down to expressions like 2+3 - one probably would compute 5 on reading that, but what about 12324/8353? You'd leave the computation until you absolutely had to do it - i.e. one would probably try to eliminate it algebraically first. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Why?
On Thu, Dec 10, 2009 at 11:16 AM, John D. Earle johndea...@cox.net wrote: Dear Gregg, You wrote, Just think about how one reads a mathematical text - you need not actually compute subformulae or even analyze them logically in order to work with them. I hate to have to say this, but do you realize that algebra is concerned with functions among other things and it is the fact that these expressions are functions and not that they are algebraic that gives them this property? Hi John, I'd say algebra is mostly concerned with equalities and substitutions and doesn't much care about functions. The equation for a circle is not a function but that doesn't mean we can't use algebra to manipulate it. Algebras might use the concept of function but they are not necessarily _about_ functions. One could even argue that the lambda calculus isn't about functions - it's just a calculus, after all. Haskell goes by the rules of that calculus; whether the expressions involved denote functions is not relevant. The computer is just performs symbol calculus. Generally all formal semantics can be reduced to syntactic calculus as far as I can see. Functional programming is not a misnomer. It is called functional programming because you are quite literally working with functions. Except when you're not. IO operations are never functions, for example, so IO expressions never denote functions. FP languages do not (and cannot) eliminate the side effectful nature of such operations; the best they can do is what Haskell does, namely circumscribe them so that they are well-behaved and thus can be properly managed (algebraically). But that doesn't make them functions. So for me at least algebraic better describes how Haskell works; what you're working with is expressions and you reason about them algebraically. You can do this reliably not because everything is a function but because non-functions are well-behaved. Functions have a profound simplifying effect. No argument there. But the expressive power that comes with first-class functions is not what distinguishes Haskell et al. - lots of non-FP languages support them these days. The truth is as Haskell has demonstrated that much of the complexity in computer programming is artificial and doesn't need to be there. It makes having to prove correctness a lot easier, but that is not the only motivation behind Haskell and other functional programming languages. The push has been getting performance up to a point where the language may be regarded as respectable. Sure, but that's only possible because the properties of programs are provable, which is what makes it possible to reliably transform a program into an equivalent but more efficient form. -Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] seems like I'm on the wrong track
On Tue, Dec 1, 2009 at 7:01 PM, Michael P Mossey m...@alumni.caltech.edu wrote: Perhaps someone could either (1) help me do what I'm trying to do, or (2) show me a better way. In this one example, in a OO way of thinking, I have data called AssignedNumbers that assigns integers to unique strings and keeps track of the used integers and next available integer (the choice of available integer could follow a number of conventions so I wanted to hide that in an ADT.) So it has an associated function: What do the numbers and strings mean? Can you use an algebraic type instead of strings? Do particular numbers have meaning or are they just serial numbers? Can you compute some sort of checksum for the strings rather than rely on an external list of numbers? If you must have a list of numbers, can you embed it in a specialized string type, so that numbers get assigned as a side-effect of string construction? In other words, would it help to think more in terms of specific types rather than generic numbers and strings? -G ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] seems like I'm on the wrong track
On Tue, Dec 1, 2009 at 7:55 PM, Michael Mossey m...@alumni.caltech.edu wrote: Thanks for the reply. Was there something specific you were referring to, or Maybe http://plucky.cs.yale.edu/cs431/reading.htm Chapter 9 An Algebra of Music. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] I miss OO
On Thu, Nov 26, 2009 at 1:50 AM, Eugene Kirpichov ekirpic...@gmail.com wrote: I argue that in the situation you provided, the pitch, duration, timbre and instrument are essential attributes of the dot, whereas time is the position of the dot on paper and should be separated from its essence. `Timing', maybe, or temporal `position', `locus', etc., although position also applies to pitch (as interval). Anything but `time', which is guaranteed to induce confusion. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] I miss OO
On Wed, Nov 25, 2009 at 2:51 PM, Michael Mossey m...@alumni.caltech.edu wrote: So if I have objects/data note1, cursor1, and staff1, Python: note1.time() cursor1.time() staff1.time() Haskell needs something like note_time note1 cursor_time cursor1 staff_time staff1 Modeling musical stuff could provide an excellent illustration of the difference between OO and the Haskell way; it's the difference between metaphysical engineering and constructive mathematics. Think algebra. Haskell isn't just about types, its about algebraic types: structures and operations (signatures). So instead of asking ``what kind of object is a note?'', ask ``what is the algebra of notes?'' And not ``what kind of mathematical object is a note?'' but ``what kind of alegebraic formula describes (constructs) a note?'' You get a type constructor and some data constructors, which are essentially algebraic formulae that allow you to construct (i.e. refer to, describe) note values using values of other types. Then you add some operators, which are defined using those constructive formulae (deconstruction via pattern matching.) Type classing allows you to use the same names for operations on different algebras. Etc. Then ``how do I access the time contained in this note? becomes ``how do I construct a formula describing the time value used to construct this note?''. I.e. it's all about the algebraic notations rather than the metaphysics of ``objects'', and Haskell gives you a variety of ways to do this, as other responses in the thread have pointed out. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] I miss OO
On Thu, Nov 26, 2009 at 6:44 AM, Stephen Tetley stephen.tet...@gmail.com wrote: 2009/11/26 Gregg Reynolds d...@mobileink.com: Modeling musical stuff could provide an excellent illustration of the difference between OO and the Haskell way; it's the difference between metaphysical engineering and constructive mathematics. Hmm, Stephen Travis Pope's SmOKe - a design that has been the basis of various state-of-the-art Smalltalk music systems - seems pretty concrete to me rather than metaphysical. http://heaveneverywhere.com/stp/PostScript/icmc.94.mode.pdf Looks interesting, but what I was trying to get at - ``metaphysical engineering'' just popped into my head and sounded kinda cool so I went with it - is that these are two radically different ways of thinking about what we're doing when we write programs. For example, Pope talks about music in terms of properties, but then says [t]hese properties may be music-specific _objects_ (such as pitches or spatial positions)... (emphasis added). This is standard OO-speak; there's nothing wrong with it, the point is just that the domain of interest is viewed as a collection of ``objects'' and their behaviors, where ``object'' is the word we use for lack of a better term to refer to things that exist - hence metaphysics. Are there _really_ any objects involved, especially where properties are concerned? Not for me, though others may differ. In any case, the overall picture is that programs are combinations of such objects, so the program is viewed as the description of a kind of machine - hence engineering. In order to describe music, the programmer describes a machine. By contrast, a ``purely functional'' approach (I prefer ``algebraic'' as more accurate or at least more revealing) might construe such properties in terms of types and operations on values of the types, which capture the notion of property directly without implicating objects in any way. A music library would be viewed in terms of a language (algebra), with customized names for domain-specific types and operations, that the programmer can use to describe music instead of describing a machine that produces music. Which makes the programmer a litterateur rather than a constructor of machines, among other things. Cheers, Gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What *is* a DSL?
On Thu, Oct 8, 2009 at 6:08 AM, Colin Paul Adams co...@colina.demon.co.ukwrote: George == George Pollard por...@porg.es writes: George I'd also like to note that the canonical pronunciation of George DSL ends in -izzle. Whose canon? Interestingly, I have always assumed the canonical pronunciation of DSSSL was diesel, as JADE stands for JAmes's DSSSL Engine. I don't see why removing extra S-es should shorten the vowel. Wht vwl? U mst b Englsh. 2 n Amrcn, DSSSL is dissel; all short vowels. DSL is dee-ess-ell. Dizzle is a brbrzm. -grgg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] commending Design concepts in programming languages
On Tue, May 12, 2009 at 1:04 PM, Max Rabkin max.rab...@gmail.com wrote: On Tue, May 12, 2009 at 1:41 PM, Wolfgang Jeltsch g9ks1...@acme.softbase.org wrote: At least, I cannot remember seeing the other notation (first morphism on the left) in category theory literature so far. It’s just that my above-mentioned professor told me that category theorists would use the first-morphism-on-the-left notation. I've seen the notation f;g for g.f somewhere (and Wikipedia mentions it). I think it's less ambiguous than just fg (which I've seen for f.g too), but in Haskell we have the option of . A flipped application might be nice to go with it. How about $ ? FYI: Unicode U+2A3E Zed notation relational composition (small circle over a 9) Examples at http://staff.washington.edu/jon/z/toolkit.html#pair3 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [SoC] XML Schema Implementation
On Mon, Mar 30, 2009 at 5:16 PM, Vlad Dogaru ddv...@anaconda.cs.pub.ro wrote: Hello everyone, I am writing to judge interest in a Summer of Code proposition: an XML Schema[1] implementation, described as a possbile application here[2]. As both a tool and an inspiration, I intend to use HaXML[3]. More specifically, I would be interested in the degree the Haskell community uses XML Schema, and if you were tempted to use it if we had an implementation. To further expand the question, how useful do you consider each of these components: * a validator * a pretty-printer * a translator from XML Schema to Haskell, similar to DtdToHaskell[4] A RelaxNG - XML Schema translator would be very useful. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] about Haskell code written to be too smart
2009/3/25 Zachary Turner divisorthe...@gmail.com: On the other hand, -certain- languages are more expressive than others. As an example, I personally find English far more expressive than both Vietnamese and Japanese, yet English is far more complicated. Japanese, for Way off topic, but for what it's worth, you can take it as axiomatic that all natural languages are equally expressive, qua languages. They're also equally easy/hard overall. The areas of difficulty are just in different places. Japanese grammar is extraordinarily simple, but achieving mastery of the spoken language *in Japanese society* is next to impossible, because usage reflects social constructions. As you no doubt know, what is not said is sometimes just as expressive as what is said in Japanese; very maddening to a logorrheic American, just as an English speaker's need to explicitly articulate *everything* is no doubt annoying to Japanese. Regarding spelling and phonology: the idea that one symbol, one sound is somehow optimal is the Myth That Will Not Die. None other than Chomsky himself argued that English orthography is near-optimal for the English language. All writing systems are designed to serve speakers of the language, and many languages are poorly modeled by a one symbol, one sound system. I'm not sure there's a lesson there for formal language designers and programmers, except maybe that the expressiveness (elegance?) of a text usually depends to a great extent on the writer more than the language. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] about Haskell code written to be too smart
On Tue, Mar 24, 2009 at 1:42 PM, Manlio Perillo
manlio_peri...@libero.it wrote:
But, as an example, when you read a function like:
buildPartitions xs ns = zipWith take ns . init $ scanl (flip drop) xs ns
that can be rewritten (argument reversed) as:
takeList :: [Int] - [a] - [[a]]
takeList [] _ = []
takeList _ [] = []
takeList (n : ns) xs = head : takeList ns tail
where (head, tail) = splitAt n xs
I think that there is a problem.
This crops up all the time even in simple mathematics. One way to
provide assistance to newcomers is to provide a quasi-English reading
of the notation. Take as an example a simple set comprehension
expression (using Z email notation,
http://csci.csusb.edu/dick/samples/z.lexis.html):
{ x : Int | 0 x 10 /\ x %e Odd @ 2*x }
That's pretty opaque for beginners until they learn to read | as such
that, %e as member of and @ as generate, so that they can express
the idea in quasi-English: form a set by taking all integers x such
that ... and ..., then generate the result by doubling them or the
like. Or take | as filter and @ as map; the point is it helps to
be able to express it in something like natural language.
Do something similar for your buildPartitions definition and I'll bet
you'll end up with something much more user friendly than takeList.
-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] about Haskell code written to be too smart
On Tue, Mar 24, 2009 at 12:41 PM, Manlio Perillo manlio_peri...@libero.it wrote: I too have this feeling, from time to time. So do I, because I haven't had the time to learn what I need to learn in order to read the code smoothly. I find that when I do work out the meaning, most often the style reflects conciseness or expressiveness, not obfuscatory tricks that the language allows. Since someone is starting to write the Haskell coding style, I really suggest him to take this problem into strong consideration. Rule One of the Haskell Coding Style Handbook: learn Haskell first, then worry about style. After all, nobody in her right mind would tackle a French style manual without learning French first. Although I suppose one could argue that learning Haskell in fact involves learning various styles. ;) -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: categories and monoids
On Thu, Mar 19, 2009 at 5:43 AM, Wolfgang Jeltsch g9ks1...@acme.softbase.org wrote: Am Mittwoch, 18. März 2009 15:17 schrieben Sie: Wolfgang Jeltsch schrieb: Okay. Well, a monoid with many objects isn’t a monoid anymore since a monoid has only one object. It’s the same as with: “A ring is a field whose multiplication has no inverse.” One usually knows what is meant with this but it’s actually wrong. Wrong for two reasons: First, because the multiplication of a field has an inverse. Second, because the multiplication of a ring is not forced to have no inverse but may have one. “A ring is like a field, but without a multiplicative inverse” is, in my eyes, an acceptable formulation. We just have to agree that “without” here refers to the definition, rather than to the definitum. Note that you said: “A ring is *like* a field.”, not “A ring is a field.” which was the formulation, I criticized above. Alternatively, the fundamental notion of category theory is that of a monoid ... a category itself can be regarded as a sort of generalized monoid. -- Saunders MacLane, Categories for the Working Mathematician (preface) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Design Patterns by Gamma or equivalent
2009/3/11 Mark Spezzano mark.spezz...@chariot.net.au: I’m very familiar with the concept of Design Patterns for OOP in Java and C++. They’re basically a way of fitting components of a program so that objects/classes fit together nicely like Lego blocks and it’s useful because it also provides a common “language” to talk about concepts, like Abstract Factory, or an Observer to other programmers. In this way one programmer can instantly get a feel what another programmer is talking about even though the concepts are fundamentally abstract. Because Haskell is not OO, it is functional, I was wondering if there is some kind of analogous “design pattern”/”template” type concept that describe commonly used functions that can be “factored out” in a general sense to provide the same kind of usefulness that Design Patterns do for OOP. Basically I’m asking if there are any kinds of “common denominator” function compositions that are used again and again to solve problems. If so, what are they called? You might find it useful to read the original works upon which the whole design pattern economy is based, namely Christopher Alexander's books (http://www.patternlanguage.com/leveltwo/booksframe.htm?/leveltwo/../bookstore/bookstore.htm). I liked Notes on the Synthesis of Form, which predates his pattern language stuff. My $0.02: design patterns became popular in the imperative language community precisely because such languages lack the formal discipline of functional languages. Alexander came up with the notion of a pattern language in order to bring some kind of discipline and abstraction to observed regularities in architecture, urban design, etc. By definition such a language cannot have anything close to formal semantics, any more than a natural language lexicon can have formal semantics. Alexander's writing is very interesting and thought provoking, but I'm not sure it has much to offer the world of functional programming. Programmers used Alexander's ideas to try to bring some order to both specifications and programs. A pattern language is a natural for trying to describe a real-world problem one is trying to solve. Imperative programmers also used it to describe programming patterns. Implementations of things like Observer/VIsitor etc. are ad-hoc, informal constructions; the equivalent in a functional language is a mathematical structure (feel free to fix my terminology). I don't think one needs design patterns for Haskell; it has mathematics and more-or-less formal semantics. Who needs Visitor when you have For All? Although design patterns may still be useful for describing a real-world problems I suspect one would be better off dumping the notion of design pattern, the better to avoid cognitive dissonance when trying to think in purely functional terms. Cheers, -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Against cuteness
On Thu, Mar 12, 2009 at 9:17 PM, Benjamin L. Russell dekudekup...@yahoo.com wrote: On Thu, 12 Mar 2009 09:11:15 -0500, Gregg Reynolds d...@mobileink.com wrote: I don't think so. Bad design will lose them (and many others), but good design and cuteness are two different things. It's also possible for a good design to be cute, too. De cutibus non est disputandem. Personally I think something interesting could be done with Thoth (nice open svg image at http://en.wikipedia.org/wiki/Thoth): God of reading/writing, math. When conflated with Hermes, also of boundaries, thieves and scoundrels, etc. Then there's Haskell B. Curry himself; notice the resemblance (http://www.haskell.org/bio.html) with J. R. Bob Dobbs (http://en.wikipedia.org/wiki/J._R._%22Bob%22_Dobbs). An artist could comicize an image of Curry. Then it's only a short step to actual cultdom - why stop with a mere web community when you can legally establish a religious cult and actually ordain Ministers? (http://www.subgenius.com/scatalog/membership.htm). -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] monadic logo
At risk of becoming the most hated man in all Haskelldom, I'd like to suggest that the Haskell logo not use lambda symbols. Or at least not as the central element. Sorry, I know I'm late to the party, but the thing is there is nothing distinctive about lambda; it's common to all FPLs. Besides, Lisp/Scheme already have that franchise. What is distinctive about Haskell it's use of the monad. The Pythagorean monad symbol is wonderfully simple: http://en.wikipedia.org/wiki/Monad_(Greek_philosophy)http://en.wikipedia.org/wiki/Monad_%28Greek_philosophy%29. Something might also be done with the triad to reflect the fact that the monad in cat theory is actually a triple ( http://en.wikipedia.org/wiki/Triad_(Greek_philosophy)http://en.wikipedia.org/wiki/Triad_%28Greek_philosophy%29 ). The Cup or Monad (http://www.sacred-texts.com/chr/herm/hermes4.htm), with a little bit of work, could be turned into an amusing Haskell manifesto. Lots of interesting imagery from the gnostic tradition ( http://www.sacred-texts.com/gno/th2/index.htm), although SICP seems already to have used something similar ( http://mitpress.mit.edu/images/products/books/0262011530-f30.jpg). Hermes Trismegistus = Thrice-great Hermes - Haskell Trismegistus, Thrice-Glorious Haskell, etc. Might be too cute. There's also Leibniz' monadology - I can't think of any visual imagery to go with it, but he did end up with the best of all possible worlds hypothesis, which gives us a slogan sure to irritate: Haskell - the best of all possible languages. Not to mention Haskell Monadology as a name for the official Haskell definition, etc. Hey, at least it isn't cute. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Against cuteness
On Thu, Mar 12, 2009 at 7:07 AM, Benjamin L. Russell dekudekup...@yahoo.com wrote: Here, there are a lot of Japanese Haskell fans who love the beauty of Haskell, and you will risk losing a lot of them if you choose a mascot without any cuteness factor. A lot of my friends meet together every I don't think so. Bad design will lose them (and many others), but good design and cuteness are two different things. You can still distinguish yourself from O'Reilly without losing the cuteness factor with a logo like one of the following: We must have vastly different ideas of cute. I don't consider those examples cute. How about this as a criterion: if it makes 13-year old Japanese girls squeal kawa! then it's too cute. Also if it involves the color pink. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Against cuteness
Regarding logos/mascots: nothing personal folks, but I would like to cast a loud firm vote against all forms of cuteness, especially small furry animal cuteness. It's been done half to death, and we are not O'Reilly. Of all the billions of images from all the cultures in the world available to us we can surely find something that is witty or charming without being cute. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Against cuteness
On Wed, Mar 11, 2009 at 5:25 AM, Bulat Ziganshin bulat.zigans...@gmail.comwrote: Hello Gregg, Wednesday, March 11, 2009, 1:17:41 PM, you wrote: are not O'Reilly. Of all the billions of images from all the cultures in the world available to us we can surely find something that is witty or charming without being cute. it will not be fun :) Perhaps not, but it also won't be torture. I can't take any more cuteness. ;) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Lazy IO breaks purity
On Thu, Mar 5, 2009 at 7:08 AM, Simon Marlow marlo...@gmail.com wrote: So the argument is something like: we can think of the result of a call to unsafeInterleaveIO as having been chosen at the time we called unsafeInterleaveIO, rather than when its result is actually evaluated. This is on dodgy ground, IMO: either you admit that the IO monad contains an Oracle, or you admit it can time-travel. I don't believe in either of those things :-) Surely there's a quantum mechanical metaphor waiting to happen here. getCat :: IO Cat If getCat appears in a program text, does it denote or not? Or both? If it does, is the cat alive or dead? (Apologies to Schrodingerhttp://en.wikipedia.org/wiki/Schr%C3%B6dinger%27s_cat). -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Paper draft: Denotational design with type class morphisms
On Fri, Feb 20, 2009 at 9:12 AM, Achim Schneider bars...@web.de wrote: Robin Green gree...@greenrd.org wrote: On Fri, 20 Feb 2009 15:17:14 +0100 Achim Schneider bars...@web.de wrote: Conal Elliott co...@conal.net wrote: DRAFT version ___ comments please Conal, please, PLEASE, never, EVER again use the word meaning if you actually mean denotation. It confuses the hell out of me, especially the (I guess unintended) connotation that you analyse the meaning of a particular instance's existence on a cosmic scale. It shouldn't confuse you. Using means for denotes, and likewise meaning for denotation, is correct English, and very common usage too. (length . denotations) to mean (length . denotations) to denote (read: to denote is more defined than to mean) Following your argument through, we should talk kinda like hey, we do something with that thingy to do that-other thingy to that thingy over there. 99% of my former teachers would tear you to shreds... in mid-air (during lift-off). I can't talk about the whole of English usage, but I never saw meaning in a mathematical context where denotation would work, too, except in Conal's writings. ...and that doesn't even include that my native language isn't English but German, in which to mean nounificates using another object: It translates to Opinion instead of Denotation. deuten (to intepret, to point) is a very well-defined concept in German and doesn't like to be messed with. The distinction is very clear in technical English but often disregarded in ordinary speech. http://consc.net/papers/intension.html is very informative. -gregg, your faithful half-baked philosophaster ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
2009/2/19 Luke Palmer lrpal...@gmail.com 2009/2/19 Rick R rick.richard...@gmail.com I think the capabilities community including E and Coyotos/BitC have extensively addressed this topic. Coyotos is taking the correct approach for trusted voting platform. Since, even if your software is trustworthy, it can't be trusted if the OS on which it runs is suspect. Woah, that's a pretty interesting question! How do you write software which is protected against a malicious operating system (mind -- not erroneous, but rather somebody detecting the software you're running and changing your vote). Maybe some sort of randomized cryptographic technique, in which, with high probability, the OS either runs your program correctly or causes it to crash. It gets worse. Even if you write your OS in Haskell, how do you know your compiler hasn't been compromised? Or the hardware? The solution necessarily involves a social component, e.g. Haskell, with the development practices of OpenBSD (continuous re-auditing of everything including tools, complete openness, etc.) IOW, it'll never happen, but it might end up better than paper ballots. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
See also www.surveymonkey.com Bulat Ziganshin bulat.zigans...@gmail.com wrote: Hello haskell-cafe, http://zohopolls.com/ -- Best regards, Bulat mailto:bulat.zigans...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
But what about the side effects? Rick R rick.richard...@gmail.com wrote: I'm sure Premier Election Solutions (formerly Diebold) can provide us with an online voting solution. Their value-add services allows us to set the outcome beforehand, so, in effect, the the voting process will be determinate. Which is certainly of interest to Haskell coders. On Wed, Feb 18, 2009 at 4:05 PM, Max Rabkin max.rab...@gmail.com wrote: On Wed, Feb 18, 2009 at 10:40 PM, Anton van Straaten an...@appsolutions.com wrote: There's also the Condorcet Internet Voting Service: http://www.cs.cornell.edu/andru/civs.html This looks like exactly what we need! Any objections? --Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- We can't solve problems by using the same kind of thinking we used when we created them. - A. Einstein ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
I.e. war, plague.famine. etc. gregg reynolds d...@mobileink.com wrote: But what about the side effects? Rick R rick.richard...@gmail.com wrote: I'm sure Premier Election Solutions (formerly Diebold) can provide us with an online voting solution. Their value-add services allows us to set the outcome beforehand, so, in effect, the the voting process will be determinate. Which is certainly of interest to Haskell coders. On Wed, Feb 18, 2009 at 4:05 PM, Max Rabkin max.rab...@gmail.com wrote: On Wed, Feb 18, 2009 at 10:40 PM, Anton van Straaten an...@appsolutions.com wrote: There's also the Condorcet Internet Voting Service: http://www.cs.cornell.edu/andru/civs.html This looks like exactly what we need! Any objections? --Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- We can't solve problems by using the same kind of thinking we used when we created them. - A. Einstein ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
Ok, that might protect us against the 7 plagues, so I'm not so worried about locusts. But what about Java, PHP etc. Is the monad sufficient protection against ultra-supernatural evil? Andrew Wagner wagner.and...@gmail.com wrote: Just wrap it in a ReallySafeWePromiseMonad 2009/2/18 gregg reynolds d...@mobileink.com I.e. war, plague.famine. etc. gregg reynolds d...@mobileink.com wrote: But what about the side effects? Rick R rick.richard...@gmail.com wrote: I'm sure Premier Election Solutions (formerly Diebold) can provide us with an online voting solution. Their value-add services allows us to set the outcome beforehand, so, in effect, the the voting process will be determinate. Which is certainly of interest to Haskell coders. On Wed, Feb 18, 2009 at 4:05 PM, Max Rabkin max.rab...@gmail.com wrote: On Wed, Feb 18, 2009 at 10:40 PM, Anton van Straaten an...@appsolutions.com wrote: There's also the Condorcet Internet Voting Service: http://www.cs.cornell.edu/andru/civs.html This looks like exactly what we need! Any objections? --Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- We can't solve problems by using the same kind of thinking we used when we created them. - A. Einstein ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
Perhaps you are a subversive functor, hmm? We have monadic ways of conrolling you, fiend! Tellus who your natural tansformations are, or else! Andrew Wagner wagner.and...@gmail.com wrote: Help! Help! I'm being suppressed!! On Feb 18, 2009, at 5:05 PM, Rick R rick.richard...@gmail.com wrote: I can't comment on any quantitative side effects, but the some intangible side effects include Distrustful Populace and MaliciousDissenters. However, if ghc is run with the - XUnscrupulousPolitics flag, those can be suppressed. On Wed, Feb 18, 2009 at 4:33 PM, gregg reynolds d...@mobileink.com wrote: I.e. war, plague.famine. etc. gregg reynolds d...@mobileink.com wrote: But what about the side effects? Rick R rick.richard...@gmail.com wrote: I'm sure Premier Election Solutions (formerly Diebold) can provide us with an online voting solution. Their value-add services allows us to set the outcome beforehand, so, in effect, the the voting process will be determinate. Which is certainly of interest to Haskell coders. On Wed, Feb 18, 2009 at 4:05 PM, Max Rabkin max.rab...@gmail.com wrote: On Wed, Feb 18, 2009 at 10:40 PM, Anton van Straaten an...@appsolutions.com wrote: There's also the Condorcet Internet Voting Service: http://www.cs.cornell.edu/andru/civs.html This looks like exactly what we need! Any objections? --Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- We can't solve problems by using the same kind of thinking we used when we created them. - A. Einstein ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- We can't solve problems by using the same kind of thinking we used when we created them. - A. Einstein ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Intergalactic Telefunctors
Came up with an alternative to the container metaphor for functors that you might find amusing: http://syntax.wikidot.com/blog:9 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Intergalactic Telefunctors
On Sun, Feb 15, 2009 at 11:09 AM, Tillmann Rendel ren...@cs.au.dk wrote: Gregg Reynolds wrote: Came up with an alternative to the container metaphor for functors that you might find amusing: http://syntax.wikidot.com/blog:9 You seem to describe Bifunctors (two objects from one category are mapped to one object in another category), but Haskell's Functor class is about Endofunctors (one object in one category is mapped to an object in the same category). Therefore, your insistence on the alien Yeah, it needs work, but close enough for a sketch. BTW, I'm not talking about Haskell's Functor class, I guess I should have made that clear. I'm talking about category theory, as the semantic framework for thinking about Haskell. universe being totally different from our own is somewhat misleading, since in Haskell, we are specifically dealing with the case that the alien universe is just our own. The idea is that each type (category) is a distinct universe. The essential point about functors cross boundaries from one category to another. Moreover, you are mixing in the subject of algebraic data types (all we know about (a, b) is that (,), fst and snd exist). It's straight out of category theory. See Pierce http://mitpress.mit.edu/catalog/item/default.asp?ttype=2tid=7986 Personally, I do not see why one should explain something easy like functors in terms of something complicated like quantum entanglement. The metaphor is action-at-a-distance. Quantum entanglement is a vivid way of conveying it since it is so strange, but true. Obviously one is not expected to understand quantum entanglement, only the idea of two things linked invisibly across a boundary. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Intergalactic Telefunctors
On Sun, Feb 15, 2009 at 11:53 AM, Tillmann Rendel ren...@cs.au.dk wrote: Gregg Reynolds wrote: BTW, I'm not talking about Haskell's Functor class, I guess I should have made that clear. I'm talking about category theory, as the semantic framework for thinking about Haskell. Don't forget the part explaining this is just a sketch. In that case, I even less see why you are not introducing category theory proper. Certainly, if one wants to use a semantic framework for thinking about something, one should use the real thing, not some metaphors. The idea is that each type (category) is a distinct universe. The essential point about functors cross boundaries from one category to another. What are the categories you are talking about here? Take your pick. Moreover, you are mixing in the subject of algebraic data types (all we know about (a, b) is that (,), fst and snd exist). It's straight out of category theory. See Pierce http://mitpress.mit.edu/catalog/item/default.asp?ttype=2tid=7986 Which part specifically? Sections 1.5, 1.6, 1.9, 2.1, etc. Personally, I do not see why one should explain something easy like functors in terms of something complicated like quantum entanglement. The metaphor is action-at-a-distance. Quantum entanglement is a vivid way of conveying it since it is so strange, but true. Obviously one is not expected to understand quantum entanglement, only the idea of two things linked invisibly across a boundary. How does the fact that a morphism exists between two objects in some category link these objects together? It doesn't change the objects at all. In your own words: How can action (at-a-distance) be about mathematical values? Not between two objects in some category; between two objects in different categories. That's the whole point. Functors preserve structure. Action-at-a-distance is a metaphor meant to enliven the concept. You use a map in your home category to map remote objects, by beaming it up through the telefunctor. Your map stays home but is quantum entangled with the remote map. Heh heh. I'm not saying it's for everybody, but I think it's kinda fun. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Intergalactic Telefunctors
On Sun, Feb 15, 2009 at 12:45 PM, Anton van Straaten an...@appsolutions.com wrote: Gregg Reynolds wrote: Action-at-a-distance is a metaphor meant to enliven the concept. Kind of like the container metaphor? Yes, only, different. Non-pernicious. ;) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] IO semantics and evaluation - summary
On Sat, Feb 14, 2009 at 9:15 AM, Stuart Cook sco...@gmail.com wrote: From Fixing Haskell IO: We can summarize the SDIOH (Standard Definition of IO in Haskell) as a value of type IO a is a value, that performs, then delivers a value of type a. I think you've already made a critical mistake here. The quotes you give all describe an IO value as something that when performed results in input/output, whereas your summary describes it as something that performs. The original quotations suggest that some outside agent interprets the values and performs the actions they denote, whereas it is your summary that has made the linguistic shift to values that dance about on tables of their own accord. I see you point, and it perfectly illustrates the problem of ambiguity ( http://syntax.wikidot.com/blog:5). Action and Performance are even more ambiguous than computation and evaluation. The natural analog to the SDIOH is theatrical performance. Where is the action, on the page or on the boards? Who performs the action, the character or the thespian? Whose action is it? Even if we settle on these questions, we have to account for delivers a value. What does the performance of the action of Hamlet deliver? Dead Polonius? Catharsis? In the end it doesn't matter how one interprets action that is performed; either way, there must be an agent. No agent, no performance. As you point out, the SDIOH can be read as positing an outside agent; it can also be read to posit the value itself as performer (which must interact with an outside agent). All of which leads to the very interesting philosophical question of what a program process actually //is//: an agent acting on a computer, or a script for the computer to enact (qua agent/thespian). Either way the SDIOH effectively tries to incorporate action/agency into the formal semantics. My proposition is just that we avoid the whole mess by eliminating notions like action, performance, and delivery. Split the semantics into internal (standard denotational stuff) and external (interpretation, which can also be represented mathematically), and you get a clearer, cleaner, simpler picture with no philosophical complications. I'm working on some diagrams and simpler language; once I'm done I guess I'll find out. In my mind, Haskell programs never actually do anything. Instead they merely denote a value of type IO () that consists of tokens representing input/output primitives, glued together by pure functions. It is the job of the runtime to take that value and actually modify the world in the manner described by the program. I wouldn't try to talk you out of whatever works for you. Just scratching a rather persistent itch about clear, simple, formal, complete representations of the intersection of math and the world. Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] IO semantics and evaluation - summary
Many thanks to everybody who tried to set me straight on the thread about IO monad and evaluation semantics. I've begun summarizing the info, and I believe I've come up with a much better way of explaining IO; just flip the semantic perspective, and think in terms of interpretations instead of actions. Voila! Oxymoron (values that perform actions) eliminated. See the Computation considered harmful and Fixing Haskell IO articles at http://syntax.wikidot.com/blog Naturally I would be grateful for any corrections/comments. Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] IO semantics and evaluation - summary
Hi Daryoush, 2009/2/13 Daryoush Mehrtash dmehrt...@gmail.com I have been trying to figure out the distinction between value, function and computation. You raised a few points that I am not sure about. In Computation considered harmful. Value not so hot either. you said: I still don't like it; a lambda expression is not a computation, it's a formal *representation* of a mathematical object (a *value*). Isn't the lambda expression a representation of something (potentially with recursion) that yields a value and not the value itself? Even integer which we think of as values are represented in the same way: http://safalra.com/science/lambda-calculus/integer-arithmetic/ Excellent question, and it illustrates the problem of abstraction management very nicely. The way Church presented the lambda operator in Introduction to Mathematical Logic is very instructive. The basic idea was how to avoid having to name functions. This is a very pragmatic concern; if we didn't have the lambda operator, we would have to invent a name for every function we want to discuss, which would quickly lead to unmanageable clutter for both writer and reader. Church put it in terms like this: x + 2 is a formula, but it doesn't denote anything, since x is free. It's not completely devoid of meaning - we get the + 2 part - but it's an open sentence: not a function, not a value (or: not the name of a function or value). But there is a function /associated/ with the formula; we can denote that function, but only by introducing a name: f x = x + 2. Now f denotes the function associated with the formula. Which means we have two things: syntax, and semantics. Actually three things, since the name f is a thing. The lambda operator just allows us to do the same thing without names: the expression lambda x.x+2 denotes the function associated with the form x + 2. So a lambda abstraction expression denotes a function without naming it. IOW, the function is not the formula; it is an abstract mathematical thing. A lambda application expression - e.g. (\x - x + 2)3 denotes application of the function to an argument. Here '3' names a value; but the value and the name are distinct. Lambda calculus thinks of function application in terms of rewriting forms - it's a calculus, it just manipulates the symbolic forms. In other words, the fact that \x - x + 2 and 3 denote values isn't important; we say the application denotes 5 because of syntactic rules. 5 is just a symbol that replaces the application expression. The contrast with ZF set theory helps. In a set theoretic account, functions are just sets of ordered pairs. Application just projects the second element of the function pair whose first element is equal to the argument. The notion of algorithm or computation is totally absent; that's why ZF is so attractive for semantics. We only want to know what an expression means, not how its meaning was discovererd. So even though lambda calculus may used to describe the symbolic manipulations needed to find the value of an application, it is not accurate to say that a lambda expression represents a computation or something that yields a value, as you put it. Or at any rate that it /only/ represents a computation. It is entirely legitimate to say that (\x - x+2)3 denotes 5 (or more accurately, the value represented by the symbol '5'); that represents the set theoretic perspective. But lambda calculus licenses us the think of the same expression as a representation of the reduction chain leading to the symbol '5'. So it really depends on your perspective. In Fixing Haskell IO you say: This works well enough; GHC manages to perform IO. But it doesn't fly mathematically. Mathematical objects *never* act, sing, dance, or *do*anything. They just are. A value that acts is an oxymoron. I guess I am not sure what a mathematical object is. Do you consider Newton method a mathematical object? What would be the value : http://en.wikipedia.org/wiki/Newton's_method#Square_root_of_a_numberhttp://en.wikipedia.org/wiki/Newton%27s_method#Square_root_of_a_number Again, it all depends on perspective. A formal method can be considered a mathematical object: a sequence. Just like a lambda expression, viewed as a representation of a sequence of reductions. But here again, the representation and the thing represented are not the same. Newton's method is an algorithm, which exists independently of any particular representation, just like the integer three is independent of the symbolic conventions we use to denote it. So Newton's method can be considered a value, just as an algorithm is a kind of value, in the abstract. And the function sqrt can be considered a value, independent of any algorithm. Application of Newton's method - note I said application, not syntactic representation of application can be thought of as a value, or an algorithmic process, or a piece of syntax, etc. A syntactic
Re: [Haskell-cafe] The Haskell re-branding exercise
On Sat, Feb 7, 2009 at 11:18 AM, Paul Johnson p...@cogito.org.uk wrote: Paul Johnson wrote: A call has gone out http://www.haskell.org/pipermail/haskell-cafe/2008-December/051836.html for a new logo for Haskell. Candidates (including a couple http://www.haskell.org/haskellwiki/Image:Haskell-logo-revolution.png of mine http://www.haskell.org/sitewiki/images/f/fd/Ouroborous-oval.png) are accumulating here http://www.haskell.org/haskellwiki/Haskell_logos/New_logo_ideas. There has also been a long thread on the Haskell Cafe mailing list. So what's happening about this? I know I'm late to the party, but here's an observation anyway. It might be better to settle on an emblem first, and then a logo. Lambda is popular for functional languages, but it's not a distinctive feature of Haskell. What is distinctive of Haskell is category theory in general and the monad in particular. Both of which are strongly reminiscent of Alchemy. Believe it or not, it's possible to see the operations of the monad as the exact analog of certain aspects of Alchemy (I'm working on a detailed exposition.) Monad as Philosopher's Stone? Galleries of Alchemical emblems and symbols are easily found on the web; see for example the symbol for composition at http://www.iridius.info/current/info/ -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell Fest
Just be careful. The judge uses lazy evaluation, so if you get arrested you might spend 20 years in the holding pen. On the bright side, you can pay for stuff whenever you feel like it. 2009/2/9 Lyle Kopnicky li...@qseep.net Looks like a lot of fun! http://www.haskellchamber.com/page6.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] evaluation semantics of bind
On Mon, Feb 9, 2009 at 10:17 PM, Richard O'Keefe o...@cs.otago.ac.nz wrote: On 10 Feb 2009, at 5:07 pm, Gregg Reynolds wrote: Thanks. I see the error of my ways. So, IO expressions must be evaluated if they are in the chain leading to main. We need some standard terminology to distinguish between *evaluating* an expression and *performing* the result of an expression of type IO something. Indeed. Wrote a blog article about this proposing a semiotic approach: http://syntax.wikidot.com/blog:4 An IO expression that is passed to a function at a strict position must be evaluated whether the result is performed or not. An IO expression whose result will be performed must be evaluated before that performance can take place. Is the result of evaluation a thunk/suspension/closer? (Dash it, this really is getting us into White Knight land.) What's White Knight land? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad explanation
On Sun, Feb 8, 2009 at 6:39 PM, Richard O'Keefe o...@cs.otago.ac.nz wrote: is a good one. If you want to say that a mathematical value with a non-mathematical effect is nonsensical, more power to you. I said I don't want to get far into White Knight territory. As long as you can agree A mathematical value INTERPRETED BY a physical engine can have physical effects, we're home and dry. Here's an analogy that will make the logical contradiction clear. Forget computers and assume you have been asked to referee a paper containing a proof with the following passage: Let x = ___ (Please fill in the blank) I think you will agree that would be plainly nonsensical. It's logically equivalent to an input operation (getInt). Now back to computers. Given a program text containing the symbol '3', the computer will provide a physical representation: an electromagnetic pattern in a bit of silicon. That's a value; the pattern is to be interpreted as a datum; it is not to be executed. For getChar, the computer will also provide such a pattern, but this pattern is to be interpreted as executable code, not as a datum. Now suppose we also have an ordinary function like Add2; it too will be represented as an electromagnetic pattern, to be interpreted as executable code. getChar and Add2 are not data, except in the trivial sense that all code is data. All three have an effect only in the trivial sense that they are physically represented. In all three cases, the symbolic representation is isomorphic to the physical representation. The 3 will not be executed. When Add2 is executed, the ensuing process is isomorphic to the mathematical function so defined. But when getChar is executed, the ensuing process is not isomorphic to a mathematical function. The process interacts with the non-mathematical world, which a mathematical function can never do. So it has a side effect along with its ordinary representational effect. The point being that the metalanguage commonly used to describe IO in Haskell contains a logical contradiction. A thing cannot be both a value and a function, but e,g, getChar behaves like a function and has the type signature of a value. I believe this is part of the reason the IO monad is troublesome for beginners (I speak from experience). -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad explanation
On Mon, Feb 9, 2009 at 4:38 AM, Tony Morris tmor...@tmorris.net wrote: -BEGIN PGP SIGNED MESSAGE- Hash: SHA1 I also agree it is a value. The original post was attempting to make a distinction that does not exist. I deliberately avoided that topic. A thing cannot be both a value and a function, but e,g, getChar My original intent was to hope the poster reconsidered the whole post. You've blown my cover :) My bad, I restate: a value cannot be both static and dynamic. Or an object and a morphism. Or an element and a function. Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction. That doesn't erase the difference between object and morphism. If you do erase that difference you end up with mush. getChar /looks/ like an object, but semantically it must be a morphism. But it can't be a function, since it is non-deterministic. So actually the logical contradiction comes from the nature of the beast. Another reason it's confusing to newcomers: it's typed as IO Char, which looks like a type constructor. One would expect getChar to yield a value of type IO Char, no? But it delivers a Char instead. This is way confusing. So I take type IO foo to mean type foo, after a side effect. In a sense getChar :: IO Char isn't even a true type signature. In any case, many thanks to all who have contributed to the thread. It's sharpened my thinking revealed weaknesses in my terminology, and I expect I'll make my inevitable contribution to the infinite Haskell tutorial on the topic before too long. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] evaluation semantics of bind
On Sun, Feb 8, 2009 at 6:25 PM, Richard O'Keefe o...@cs.otago.ac.nz wrote: On 6 Feb 2009, at 4:20 am, Gregg Reynolds wrote: However, consider: getChar = \x - getChar An optimizer can see that the result of the first getChar is discarded and replace the entire expression with one getChar without changing the formal semantics. But the result of the first getChar is *NOT* discarded. **As an analogy**, think of the type IO t as (World - (t,World)) for some hidden type World, and getChar w = (c, w') -- get a character c out of world w somehow, -- changing w to w' as you go (f = g) w = let (v,w') = f w in (g v) w' In this analogy, you see that the result of getChar is a value of type IO Char (not of type Char), and that while the character part of the result of performing the result of getChar may be discarded, the changed world part is NOT. That's an implementation detail. It doesn't account for other possible IO implementations. My original question was motivated by the observation that a human reader of an expression of the form e = f , on seeing that f is constant, may pull the constant value out of f, disregard e and dispense with the application f e. So can a compiler, unless IO expressions are involved, in which case such optimizations are forbidden. I wondered if that was due to the semantics of = or the semantics of IO. To summarize what I've concluded thanks to the helpful people on haskell-cafe: The compiler can optimize e = f except for any IO expressions in e and f. IO expressions must be evaluated, due to the semantics of IO. The may not be disregarded, memoized, or substituted. IO semantics may be implemented in different ways by different compilers; these implementation techniques are not part of the formal semantics of the language, which may be expressed as above: IO expressions must be evaluated wherever and whenever they occur. The bind operator = enforces sequencing on arguments containing IO expressions, but does not force evaluation. Even bind expressions involving IO may be optimized. For example: getChar = \x - ...monster computation... putChar 'c' The compiler may discard monster computation (assuming it contains no IO expressions), but it must evaluate getChar and putChar (due to IO semantics) in the correct order (due to bind semantics). Thanks all, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad explanation
On Mon, Feb 9, 2009 at 5:32 AM, Sittampalam, Ganesh ganesh.sittampa...@credit-suisse.com wrote: My bad, I restate: a value cannot be both static and dynamic. Or an object and a morphism. Or an element and a function. Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction. That doesn't erase the difference between object and morphism. If you do erase that difference you end up with mush. getChar /looks/ like an object, but semantically it must be a morphism. But it can't be a function, since it is non-deterministic. So actually the logical contradiction comes from the nature of the beast. Another reason it's confusing to newcomers: it's typed as IO Char, which looks like a type constructor. One would expect getChar to yield a value of type IO Char, no? But it delivers a Char instead. This is way confusing. So I take type IO foo to mean type foo, after a side effect. In a sense getChar :: IO Char isn't even a true type signature. It does yield a value of type IO Char, which it also happens that you can ask the Haskell runtime to interpret by combining it with other IO values using = and invoking it from the top-level. *When interpreted in this way* it delivers a Char, but that's precisely the point at which we move to the different level of abstraction you mention above. Right; implementation of IO means also an implementation for =, not just the IO operators. I hadn't thought about that but it's hugely important for the exposition of monads and IO. The IO Char indicates that getChar, when invoked, performs some action which returns a character. (Gentle Intro, typical of many expositions.) That, plus the form of \x - putChar x used with =, plus the fact that one can do getChar at the ghci command line, plus all the other stuff - it all adds up to exasperation. Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] evaluation semantics of bind
On Mon, Feb 9, 2009 at 7:17 AM, Lennart Augustsson lenn...@augustsson.netwrote: Just to clarify a little. If you implement the IO monad in a sane way (as some kind of state monad or continuation monad) then the compiler can optimize e=f even for the IO monad. The implementation of = will ensure the sequencing of effects in e before effects in f. I think this answers one of my questions about the relation of category theory to Haskell. Bind is an implementation of the Kleisli star, but the latter, being abstract, may encode data dependency but not sequence. The IO implementation of = must ensure sequence, regardless of data dependency (e.g. even for putChar 'a' = \x - putChar 'c'). So if we wanted to write a Haskell specification with more formality and detail than the Report, we could say that the IO monad must implement the Kleisli star operator, but that would not be enough, we would also have to require that the implementation ensure sequencing. IOW, Kleisli star implementation plus a constraint on the implementation. Does that sound right? The IO monad is less magic than you seem to think it is. :) Any sufficiently advanced technology is isomorphic to magic. ;) (http://www.quotationspage.com/quote/776.html) -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Formal semantics for Haskell?
ML has a formal definition[1]; why not Haskell? Would this be a Good Thing, or a Waste Of Time? The Report strikes me as a hybrid of formal and informal. I guess that's not a problem so far, but there aren't that many implementations; if we had dozens, how could we verify conformance? A formal semantics would be useful, but it would also be Fun to use Category Theory notation in a language definition. Such a task would be way beyond my abilities, but I have come up with an idea for a formal semantics of IO and other non-deterministic elements of the language that I think is kind of interesting. It's inspired by Category Theory and the Z specification language. See my (brief) blog articlehttp://syntax.wikidot.com/blog:3 . Actually, I'm in a state of rather intense euphoria about it, so a bucket of cold water realism over my head might be a Good Thing. Then I could get some sleep instead of obsessing about category theory and Haskell. :) I propose any formal definition include the following warning, modeled on Knuth's warning about MetaFont: WARNING: Haskell can be hazardous to your other interests. Once you get hooked, you will develop intense feelings about language design; semantic models will intrude on the program texts you read. And you will perpetually be thinking of improvements to the programs that you see everywhere, including those of your own design. Thanks, gregg [1] The Definition of Standard ML (Revised); a preview is on Google Books ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Formal semantics for Haskell?
Is that () or _|_? ;) Tim Newsham news...@lava.net wrote: null___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] evaluation semantics of bind
On Mon, Feb 9, 2009 at 11:06 AM, Tillmann Rendel ren...@cs.au.dk wrote: Gregg Reynolds wrote:: My original question was motivated by the observation that a human reader of an expression of the form e = f , on seeing that f is constant, may pull the constant value out of f, disregard e and dispense with the application f e. While a human reader may well do that, but it would be correct or wrong depending on the definition of =. The same is of course true for compilers. By the way, there is no application f e. I guess it would help if I got the notation right. My intended meaning was f* e, where * is the Kleisli star. Sorry about that. An example where it would be wrong to ignore e: sum ([1, 2] = const [21]) This expression should evaluate to sum [21, 21] = 42, not sum [21] = 21. Sigh. I hate it when this happens. Just when I thought I had it figured out, it turns out I'm clueless. This is very enlightening and should definitely be included in any monad tutorial. Actually you don't even need sum and const to demo the point, [1,2] = \x - [21] evals to [21, 21] in ghci. And I have absolutely no idea why. Very mysterious, the Kleisli star. :( Back to the drawing board! -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] evaluation semantics of bind
On Mon, Feb 9, 2009 at 8:37 PM, Richard O'Keefe o...@cs.otago.ac.nz wrote: There isn't any application f e. Any human reader who does that is simply WRONG to do so. Sorry, should have written f* In your fragmentary example, monster computation may be discarded EVEN IF it contains IO expressions, it's only if they are linked into the IO chain using and/or = that the environment will perform their values. Thanks. I see the error of my ways. So, IO expressions must be evaluated if they are in the chain leading to main. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Moggi :: CT - Hask
Hi, I had a monadic revelation at about 3 am. The answer to the question what is an IO value, really? is who cares? I just posted a blog entry discussing how CT found it's way from Moggi into Haskell at http://syntax.wikidot.com/blog (hence the title; Moggi as functor). It addresses the question of what such things are and why Moggi's insight is so brilliant. Feedback welcome, but please remember this is coming from a non-mathematician who likes to write. If you find anything there that outrages your inner Russell, please correct me, but be gentle. Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Moggi :: CT - Hask
Correction: the correct response is: Nothing. On Sat, Feb 7, 2009 at 11:11 AM, Gregg Reynolds d...@mobileink.com wrote: Hi, I had a monadic revelation at about 3 am. The answer to the question what is an IO value, really? is who cares? I just posted a blog entry discussing how CT found it's way from Moggi into Haskell at http://syntax.wikidot.com/blog (hence the title; Moggi as functor). It addresses the question of what such things are and why Moggi's insight is so brilliant. Feedback welcome, but please remember this is coming from a non-mathematician who likes to write. If you find anything there that outrages your inner Russell, please correct me, but be gentle. Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Semantic web
Anybody implementing rdf or owl stuff in haskell? Seems like a natural fit. G___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Moggi :: CT - Hask
Hi Dan, On Sat, Feb 7, 2009 at 12:00 PM, Dan Doel dan.d...@gmail.com wrote: On Saturday 07 February 2009 12:11:29 pm Gregg Reynolds wrote: As far as I know, Moggi didn't really have anything directly to do with Haskell. He pioneered the idea of monads being useful in denotational semantics. But it was Wadler that recognized that they'd be useful for actually writing functional programs (see his The Essence of Functional Programming). So one might say that it was his doing that brought monads to Haskell proper. From what I've read Wadler was clearly the guy who thought of using monads in Haskell, but he explicitly credits Moggi for coming up with the general idea. Moggi just as clearly knew he was on to something powerful and useful (e.g. something that could lead to the introduction of higher order modules in programming languages like ADA or ML). What I would be interested in knowing is whether it was Wadler or Moggi who first realized monads (and CT) could be encoded directly in a target language, not just in a semantic metalanguage. Plus there were other people working in the same area; I just don't know the detailed history. Might be a good subject for a blog post for somebody who does. FYI I made a few corrections to my original post. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] evaluation semantics of bind
I think I've just about got monads figured out, but there's one detail that still escapes me. As I understand it, a monad is a kind of programming trick the uses data dependency to force evaluation order. x = f means apply f to x; since the value of f x depends on the value of x, the evaluator must evaluate x before f x. However, consider: getChar = \x - getChar An optimizer can see that the result of the first getChar is discarded and replace the entire expression with one getChar without changing the formal semantics. But that would change the behavior, so to get the desired behavior, there must be some principle that prevents this from happening, ensuring that x = f always evaluates f x. I can see that the monad laws ensure this But I haven't found anything that states this. Am I missing something? Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] evaluation semantics of bind
On Thu, Feb 5, 2009 at 9:27 AM, Bulat Ziganshin bulat.zigans...@gmail.comwrote: Hello Gregg, Thursday, February 5, 2009, 6:20:06 PM, you wrote: An optimizer can see that the result of the first getChar is discarded and replace the entire expression with one getChar without changing the formal semantics. this is prohibited by using pseudo-value of type RealWorld which is passed through entire action stream. actually, order of execution is controlled by dependencies on this values http://haskell.org/haskellwiki/IO_inside Thanks. I actually read that a few weeks ago and forgot all about it. So the gist is that type IO has special magic semantics. Formal, but hidden. Which means monad semantics are built in to the language, at least for that type. The Haskell Report doesn't seem to say anything about this, which seems odd. But then for non-IO monads, the optimization would be allowed, no? Of course; only the IO monad has external world behavior. Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad explanation
On Wed, Feb 4, 2009 at 8:18 PM, Richard O'Keefe o...@cs.otago.ac.nz wrote: On 5 Feb 2009, at 10:20 am, Gregg Reynolds wrote: That's a fairly common representation, seems to work for lots of people, but it caused me no end of trouble. Values are mathematical objects; how, I asked myself, can they possibly /be/ programs that do IO (or actions, or computations, or your metaphor here)? It doesn't make sense, says I, without reference to the rest of your message, of course values can /be/ programs. Not programs, but programs that do IO. The point of the idiom is that there's an external side effect involved. What sticks in my craw is that a mathematical value with a non-mathematical side effect is, well, non-mathematical and possibly nonsensical. I know it works for some (most?) people, but for me it lacks Geometry and Theology. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluation semantics of bind
On Thu, Feb 5, 2009 at 9:53 AM, Gleb Alexeyev gleb.alex...@gmail.comwrote:
Let's imagine that IO datatype is defined thus:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}
import Prelude(Monad, Char)
data IO a where
GetChar :: IO Char
Bind :: IO a - (a - IO b) - IO b
getChar = GetChar
(=) = Bind
It is perfectly possible to construct IO actions as values of this data
type and execute them by some function evalIO :: IO - Prelude.IO with the
obvious definition. Now the question arises: do you think
getChar = \x - getChar would be optimized to getChar by compiler?
I must be misunderstanding something. I don't know if it would be optimized
out, but I see no reason why it couldn't be. There's no data dependency,
right?
-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] evaluation semantics of bind
On Thu, Feb 5, 2009 at 10:00 AM, Lennart Augustsson lenn...@augustsson.net wrote: There's nothing magic about IO when it comes to monad semantics. If you take ghc's implementation of IO, it's a state monad. Doesn't that mean the semantics are defined by the implementation? My problem is that I'm not seeing how correct eval sequencing can be forced unless a magic token is passed around, which means that /some/ such hidden semantics must be part of the formal semantics of IO. In other words, it's not enough for it to be a monad, since = by itself cannot guarantee data dependency. If it doesn't pass around the World token, we don't get sequencing. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluation semantics of bind
On Thu, Feb 5, 2009 at 10:26 AM, m...@justinbogner.com wrote: x = f does not mean apply f to x, it means do x, and then do f with the result of x. Bind is a sequencing operator rather than an application operator. Sequencing is a side effect of data dependency. What I should have said is x = f means evaluate x and f (in any order), /then/ apply f to x. In a non-IO monad, x can be discarded if f does not depend on it. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluation semantics of bind
On Thu, Feb 5, 2009 at 10:49 AM, Gleb Alexeyev gleb.alex...@gmail.com wrote: Gregg Reynolds wrote: I must be misunderstanding something. I don't know if it would be optimized out, but I see no reason why it couldn't be. There's no data dependency, right? Of course there is data dependency. In my example, where IO is defined as a (generalized) algebraic datatype, the value of getChar is GetChar. The value of 'getChar = \x - getChar' is 'Bind GetChar (\x - GetChar'. 'x' is not used anywhere, but this doesn't change the fact that these are totally different values, no sane compiler would prove them equal. Are you saying that using equations to add a level of indirection prevents optimization? I still don't see it - discarding x doesn't change the semantics, so a good compiler /should/ do this. How is this different from optimizing out application of a constant function? -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluation semantics of bind
On Thu, Feb 5, 2009 at 11:12 AM, Andrew Wagner wagner.and...@gmail.com wrote: Are you saying that using equations to add a level of indirection prevents optimization? I still don't see it - discarding x doesn't change the semantics, so a good compiler /should/ do this. How is this different from optimizing out application of a constant function? No, no compiler should change getChar = \x - getChar to just getChar, because it's just wrong. The first will try to read in two values of type Char, the second will only try to read one. Side effects aren't THAT hated! Right, but that's only because the compiler either somehow knows about side effects or there is some other mechanism - e.g. an implicit World token that gets passed around - that prevents optiimization. As far as the formal semantics of the language are concerned, there's no essential difference between getChar = \x - getChar and Foo 3 = \x - Foo 7 for some data constructor Foo. I should think the latter would be optimized; if so, why not the former? The presence of some hidden (from me, anyway) semantics is inescapable. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluation semantics of bind
On Thu, Feb 5, 2009 at 11:22 AM, Gleb Alexeyev gleb.alex...@gmail.com wrote: Gregg Reynolds wrote: Are you saying that using equations to add a level of indirection prevents optimization? I still don't see it - discarding x doesn't change the semantics, so a good compiler /should/ do this. How is this different from optimizing out application of a constant function? Perhaps my example doesn't work, so I'll try another example. As you know, (=) is just an (overloaded) higher-order function. Let's consider another higher-order function, map. The expression map (\x - 42) [1..3] evaluates to [42, 42, 42]. As you can see, the function (\x - 42) passed to map ignores its first argument. Would you expect the compiler to discard the call to map? No, but I might expect it to discard the function application and just replace each element of the list with 42. Which it may do at compile time. Plus, it will only be evaluated once, no matter how many times the expression occurs, since lazy evaluation memoizes results. Can you see the analogy? The shapes of the two expressions, map (\x - 42) [1..3] and (=) getChar (\x - getChar) are similar. (=) is a combinator just like map, you cannot optimize it away in general. Ok, I see what you're getting at, but I have to think about it some more. Here's a restatement that might make my puzzlement more clear. Suppose we have f = \x - 42 Then I would expect the compiler to replace each expression of the form f x with 42, for all x. Now suppose we write 7 = \x - 42. It seems to me that a compiler could examine that expression, conclude that it is constant, and replace it with the expression 42. So far as I know, there's nothing in the semantics of Haskell to forbid this, so why not do it? There are no side effects, and an optimizer can always substitute equals for equals, no? (Let's disregard the fact that such optimizations may be hard or expensive.) This is different from map, because unlike map it doesn't need to perform a computation (i.e. execute the function) to arrive at the final value; it only has to analyze the function (which is computation but not computation of the function itself.) Now getChar is a value of type IO Char, by definition. That means mathematical value - an action that does some IO won't cut it in a formal semantics, since there is no way to express does some IO formally. Values is values; they don't do anything. So we should be able to replace 7 and 42 above by getChar, and do the same optimization. Do you see why this is problematic for me? In any case, you're responses (and the others) have been quite useful and have helped me work through some problems with a rather radical idea I have to address this that I hope to write up this weekend. Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad explanation
On Thu, Feb 5, 2009 at 1:46 PM, Lennart Augustsson lenn...@augustsson.net wrote: You are absolutely right. The statement The values of the IO monad are programs that do IO. is somewhat nonsensical. Values don't do anything, they just are. Whew! So I'm not crazy. I was starting to wonder. But values of the IO monad *describe* how to do IO; they can be seen as a recipe for doing IO. A recipe doesn't cook a dish, but when the recipe is executed by a cook they creates a dish. An IO values doesn't do IO, but when it is executed by the runtime system IO happens. This is one way of interpreting what the IO type means. (Another one is to say that Haskell is just an imperative programming language, but any imperative actions show up in the type.) Thanks very much to you and everybody who contributed on the thread. It's amazing how much one can learn on this list. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluation semantics of bind
On Thu, Feb 5, 2009 at 7:19 PM, wren ng thornton w...@freegeek.org wrote: Gregg Reynolds wrote: as the formal semantics of the language are concerned, there's no essential difference between getChar = \x - getChar and Foo 3 = \x - Foo 7 for some data constructor Foo. I should think the latter would be optimized; if so, why not the former? The presence of some hidden (from me, anyway) semantics is inescapable. There's no reason to assume the latter would be optimized either. Consider: data NotIO a = NotIO String a instance Monad NotIO where return x = NotIO x (NotIO s x) = f = (\(NotIO z y) - NotIO (s++z) y) (f x) notGetChar = NotIO foo 'a' Let's consider your example: notGetChar = \x - notGetChar == (NotIO foo 'a') = (\x - NotIO foo 'a') == (\(NotIO z y) - NotIO (foo++z) y) ((\x - NotIO foo 'a') 'a') == (\(NotIO z y) - NotIO (foo++z) y) (NotIO foo 'a') == NotIO (foo++foo) 'a' You've defined = in such a way that it carries additional semantic weight. My example doesn't do that. Bind can be thought of as an augmented application operator: x = f applies f to x, but it may fiddle with x first. If it doesn't then it amounts to ordinary function application, which can be optimized out. That's the point of my example: data constructors don't munge their arguments, and getChar is essentially a data constructor. NotIO has a Chars for side effects. IO is a perfectly fine mathematical object, the only difference is that it is appending sequences of an abstract Gotcha! appending sequences is not something mathematical values are inclined to do. They neither spin nor toil, let alone append. The dominant idiom - IO values are actions just doesn't work if you want formal semantics, no matter how useful it may be pedagogically. The only way we can optimize away one of the calls to notGetChar (or any other monadic function) is if we can guarantee that no other computation will use either the monoidal values or the contained values associated with it. IO is defined with a bind operator that's strict in the monoidal value, which means we can never remove things (unless, perhaps, we can Ok; but where does it say that in the language definition? I understand how it all works, but that comes from the many informal narrative expositions; my point is that if you tried to write a formal semantics for Haskell, a la ML, you couldn't do it without coming up with a different story for IO. -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] morphisms in IO
I'm working on a radically different way of looking at IO. Before I post it and make a fool of myself, I'd appreciate a reality check on the following points: a) Can IO be thought of as a category? I think the answer is yes. b) If it is a category, what are its morphisms? I think the answer is: it has no morphisms. The morphisms available are natural transformations or functors, and thus not /in/ the category. Alternatively: we have no means of directly naming its values, so the only way we can operate on its values is to use morphisms from the outside (operating on construction expressions qua morphisms.) c) All categories with no morphisms (bereft categories?) are isomorphic (to each other). I think yes. Thanks, gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] morphisms in IO
On Thu, Feb 5, 2009 at 10:32 PM, Dan Weston weston...@imageworks.com wrote: I truly have no idea what you are saying (and probably not even what I am saying), but I suspect: a) You are calling IO the target category of applying the functor IO [taking a to IO a and (a-b) to (IO a - IO b)] to Hask. b) This category is hardly bereft, nor discrete. Its morphisms are IO a - IO b. Well, that's a function in Haskell, yes; but does it represent a morphism /in/ the category? It looks more like a Functor morphism to me. c) What you are calling a bereft category is an empty category. Without (identity) morphisms, there can be no objects. There is only one such Right, I meant other than Id morphisms. I guess discrete is the correct term. category (the empty category), so naturally any two such are isomorphic (for what it's worth, which I suspect is not much). Thanks, g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad explanation
On Wed, Feb 4, 2009 at 11:41 AM, Tim Newsham news...@lava.net wrote: I put up a small Monad explanation (I wouldn't quite call it a tutorial): http://www.thenewsh.com/~newsham/haskell/monad.htmlhttp://www.thenewsh.com/%7Enewsham/haskell/monad.html The values of the IO monad are programs that do IO. That's a fairly common representation, seems to work for lots of people, but it caused me no end of trouble. Values are mathematical objects; how, I asked myself, can they possibly /be/ programs that do IO (or actions, or computations, or your metaphor here)? It doesn't make sense, says I, so I must be misunderstanding something about values; better spend hours and hours researching and trying to figure this out. But it turns out the answer is simple: they can't. They're not actions, or IO procedures, or anything else other than plain old mathematical values, no different than '2' or Int - Char. They happen to correspond in some way to the external physical behavior of the program, but that correspondence is an implementation detail beyond the scope of the formal (mathematical) semantics of the language. You don't even need monads for this part; they only enter the picture in order to provide ordered evaluation. In fact there really aren't any monadic values, since a monad is pure morphism; the values at issue are functoric values if anything. It's (the implementation of) getChar the does the IO, not IO Char. So you could say that the monad itself is a purely mathematical structure that has the felicitous if accidental side effect of imposing temporal sequence on the physical interpretation (events) associated with the program. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type and data constructors in CT
On Mon, Feb 2, 2009 at 3:27 PM, David Menendez d...@zednenem.com wrote: Does that help at all? I think it does. But ... it gives me crazy ideas. Like: a functor is a kind of magic non-computing function! That's why they didn't call it a function? We know it maps A to FA, but we don't know how (maybe we don't care): there's no algorithm, just a functorific magic carpet that transports us across the border to FA. We couldn't compute FA even if we wanted to - different categories are like alternate universes, it would be like producing a widget in an alternate physical universe, we have no way of even thinking of how to do that. Ditto for data constructors as natural transformations: they don't compute, they just do magic. They're the CT surgeon's devious way of working on the guts of a categorical object without getting his hands dirty with mundane functions - getting from value A to (an?) image value of A under the functor F, which we cannot do directly by algorithm or computation. We do not - can not - have an actual function that computes A's image. We have to work indirectly, using non-computing magic carpets - first Id takes us to Id A, then we follow the nat trans to FA. Ok, that probably triggers the gag reflex for a real mathematician, but it sure sounds like a good story to me (remember, I'm taking notes for a guide/tutorial for newbies that may or may not ever get written.) Thanks very much for the help, -gregg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type metaphysics
Hi, The concept of type seems to be a little like porno: I know it when I see it, but I can't define it (apologies to Justice Stewart). I've picked through lots of documents that discuss types in various ways, but I have yet to find one that actually says what a type really is. For example, definitions of the typed lambda calculus usually define some type symbols and rules like a : T means a is of type T, and then reasoning ensues without discussion of what type means. The only discussion I've found that addresses this is at the Stanford Encyclopedia of Philosophy, article Types and Tokens [1]. It's all very philosophical, but there is one point there that I think has relevance to Haskell. It's in section 4.1, discussing the distinction between types and sets: Another closely related problem also stems from the fact that sets, or classes, are defined extensionally, in terms of their members. The set of natural numbers without the number 17 is a distinct set from the set of natural numbers. One way to put this is that classes have their members essentially. Not so the species homo sapiens, the word 'the', nor Beethoven's Symphony No. 9. The set of specimens of homo sapiens without George W. Bush is a different set from the set of specimens of homo sapiens with him, but the species would be the same even if George W. Bush did not exist. That is, it is false that had George W. Bush never existed, the species homo sapiens would not have existed. The same species might have had different members; it does not depend for its existence on the existence of all its members as sets do. So it appears that one can think of a type as a predicate; any token (value?) that satisfies the predicate is a token (member?) of that type. This gives a very interesting way of looking at Haskell type constructors: a value of (say) Tcon Int is anything that satisfies isA Tcon Int. The tokens/values of Tcon Int may or may not constitute a set, but even if they, we have no way of describing the set's extension. My hunch is that it /cannot/ be a set, although I'm not mathematician enough to prove it. My reasoning is that we can define an infinite number of data constructors for it, including at least all possible polynomials (by which I mean data constructors of any arity taking args of any type). To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. In any case, Tcon Int does not depend on any particular constructor, just as homo sapiens does not depend on any particular man. So it can't be a set because it doesn't have its members essentially. (I suspect this leads to DeepThink about classical v. constructivist mathematics, but that's a subject for a different discussion.) I'm not sure that works technically, but it seems kinda cool. My question for the list: is the collection of e.g. Tcon Int values a set, or not? If it is, how big is it? Thanks, gregg [1] http://plato.stanford.edu/entries/types-tokens/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Hi Martijn, On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen mart...@van.steenbergen.nl wrote: There are many answers to the question what is a type?, depending on one's view. One that has been helpful to me when learning Haskell is a type is a set of values. That's the way I've always thought of types, never having had a good reason to think otherwise. But it seems it doesn't work - type theory goes beyond set theory. I've even found an online book[1] that uses type theory to construct set theory! At least I think that's what it does (not that I understand it.) This gives a very interesting way of looking at Haskell type constructors: a value of (say) Tcon Int is anything that satisfies isA Tcon Int. The tokens/values of Tcon Int may or may not constitute a set, but even if they, we have no way of describing the set's extension. Int has 2^32 values, just like in Java. You can verify this in GHCi: Ok, but that's an implementation detail. My question is what is the theoretical basis of types. Notice that the semantics of Haskell's built-in types are a matter of social convention. The symbols used - Int, 0, 1, 2, ... - are well-known, and we agree not to add data constructors. But we could if we wanted to. Say, Foo :: Int - Int. Then Foo 3 is an Int, distinct from all other Ints; in particular it is not equal to 3. I suspect a full definition of type would have to say something about operations. To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. Here you're probably thinking about the distinction between countable and uncountable sets. See also: It could be that values of a constructed type form an uncountably large set, rather than something too big to be a set at all. I'm afraid I don't know how to work with such critters. In any case, the more interesting thing (to me) is the notion that sets contain their members essentially, but data types don't, as far as I can see. Thanks much, gregg [1] http://www.cs.chalmers.se/Cs/Research/Logic/book/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Hi and thanks for the response,
On Mon, Feb 2, 2009 at 10:32 AM, Lennart Augustsson
lenn...@augustsson.netwrote:
Thinking of types as sets is not a bad approximation. You need to add
_|_ to your set of values, though.
So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}
I'm afraid I haven't yet wrapped my head around _|_ qua member of a set. In
any case, I take it that sets being a reasonable /approximation/ of types
means there is a difference.
Back to metaphysics: you pointed out that the function space is countable,
and Christopher noted that there are countably many strings that could be
used to represent a function. So that answers my question about the size of
e.g. Tcon Int. But then again, that's only if we're working under the
assumption that the members of Tcon Int are those we can express with data
constructors and no others. If we drop that assumption,then it seems we
can't say much of anything about its size.
FWIW, what started me on this is the observation that we don't really know
anything about constructed types and values except that they are
constructed. I.e. we know that Foo 3 is the image of 3 under Foo, and
that's all we know. Any thing else (like operations) we must construct out
of stuff we do know (like Ints or Strings.) This might seem trivial, but to
me it seems pretty fundamental, since it leads to the realization that we
can use one thing (e.g. Ints) to talk about something we know nothing about,
which seems to be what category theory is about. (Amateur speaking here.)
Thanks,
gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 11:51 AM, Lennart Augustsson
lenn...@augustsson.netwrote:
If we're talking Haskell types here I think it's reasonable to talk
about the values of a type as those that we can actually express in
the Haskell program, any other values are really besides the point.
Well, if you have a more philosophical view of types then I guess
there is a point, but I thought you wanted to know about Haskell
types?
The metaphysics thereof. ;) I want to situate them in the larger
intellectual context to get a more precise answer to what is a type,
really?
There's nothing mysterious about _|_ being a member of a set. Say
that you have a function (Int-Bool). What are the possible results
when you run this function? You can get False, you can get True, and
the function can fail to terminate (I'll include any kind of runtime
error in this).
So now we want to turn this bit of computing into mathematics, so we
say that the result must belong to the set {False,True,_|_} where
we've picked the name _|_ for the computation that doesn't terminate.
Note that is is mathematics, there's no notion of non-termination
here. The function simply maps to one of three values.
I like that, thanks.
-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 12:39 PM, Ketil Malde ke...@malde.org wrote: Gregg Reynolds d...@mobileink.com writes: This gives a very interesting way of looking at Haskell type constructors: a value of (say) Tcon Int is anything that satisfies isA Tcon Int. Reminiscent of arguments between dynamic and static typing camps - as far as I understand, a dynamic type is just a predicate. So division by zero is a type error, since the domain of division is the type of all numbers except zero. In contrast, I've always thought of (static) types as disjoint sets of values. My reasoning is that we can define an infinite number of data constructors for it, including at least all possible polynomials (by which I mean data constructors of any arity taking args of any type). I guess I don't quite understand what you mean by Tcon Int above. Could you give a concrete example of such a type? Just shorthand for something like data Tcon a = Dcon a, applied to Int. Any data constructor expression using an Int will yield a value of type Tcon Int. To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. I suspect that since types and values are separate domains, you avoid the complications caused by self reference. In any case, Tcon Int does not depend on any particular constructor, just as homo sapiens does not depend on any particular man. So it can't be a set because it doesn't have its members essentially. I don't follow this argument. Are you saying you can remove a data constructor from a type, and still have the same type? And because of this, the values of the type do not constitute a set? Yep. Well, that is /if/ you start from the Open-World Assumption - see http://en.wikipedia.org/wiki/Open_World_Assumption (very important in ontologies e.g. OWL and Description Logics). Just because we know that e.g. expressions like Dcon 3 yield values of type Tcon Int does not mean that we know that those are the only such expressions. So we can't really say anything about how big it can be. Who knows, it might actually be a useful distinction for an OWL reasoner in Haskell. I guess it boils down to how Tcon Int does not depend on any particular constructor. That seems like a good way of putting it. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 10:05 AM, Andrew Butterfield andrew.butterfi...@cs.tcd.ie wrote: Martijn van Steenbergen wrote: To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. Here you're probably thinking about the distinction between countable and uncountable sets. See also: http://en.wikipedia.org/wiki/Countable_set No - it's even bigger than those ! He is thinking of proper classes, not sets. http://en.wikipedia.org/wiki/Class_(set_theory) Yes, that's my hypothesis: type constructors take us outside of set theory (ZF set theory, at least). I just can't prove it. Thanks, g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
