I was bothered by him equating closures and thunks. While they are kind of similar (a thunk is almost like a closure with no arguments), they aren't really the same thing.
I read the article as saying almost exactly that: thunks are sort of like closures, but not entirely. I have the advantage of having a good understanding of both thunks and closures already, but I don't think most reasonable readers would think he's drawing an exact equivalence. Rather he's pointing out a similar concept (code that is run sometime later) that readers may have encountered elsewhere.
"Local color so you can sound like you know what you’re talking about: in Haskell-land, a closure is called a “thunk”."
Which just isn't true. A closure is called a closure and a thunk is called a thunk (as it is in Scheme and any number of other languages; there is nothing special about Haskell). For most of that article he should just replace the word 'closure' with 'thunk' and the issue would disappear.
they really are the same thing semantically, a thunk is a just closure that will be evaluated once (being applied to a unit/trivial value), and then GHC will have its runtime mark a bit that indicated that its been evaluated and redirect the thunk pointer to a value. This is simply a difference of efficiency between normal order evaluation vs lazy evaluation, with a special sort of common subexpression elimination built into the language
A closure is a function + environment, i.e., the values of its free variables at the time of creation.
A thunk is a suspended computation together with an environment. That is, a thunk is a special type of closure, where the function takes no arguments. Additionally, a thunk is updated with its result.
In GHC's execution model, the Spineless Tagless G-machine (STG), every heap object is actually a closure. That is, every heap object has a code pointer that can be called to return the object's value. For evaluated objects (including functions) that is essentially the identity function, for thunks this will evaluate as much as necessary, return, and possibly update it's heap object with its new value. Of course, there are several optimisations going on, but that's the basic idea.
Pretty good article! I read the first few paragraphs and was a little scared, but the author redeemed himself with the line, "A simpler way to think about monads is as a hack to turn function composition into a way of forcing the sequencing of function calls, or the functional-programming equivalent of a shell pipeline." After that, I would agree with pretty much everything he says! (A first for an "I looked at Haskell today" article :)
A few nit-picks that come to mind; thunks and closures are related but different, every other language with thunks also calls them thunks.
Lisp is not really "based on lambda calculus" any more than any other imperative programming language; "(loop for i from 1 to 10 collect (+ i 42))" is not so different from a loop in assembler.
And finally, monads are not really a hack for making function application look like a sequence, that's already what function application does. Monads just let you run some extra code between function applications. But given that most people write stuff like, "monads are like nuclear-waste burritos inside of spacesuits" (er...), I am not going to complain about this explanation too loudly :)
Well... if you consider IO to be the nuclear waste of functional programming, the IO monad is a way of wrapping up that nuclear waste so tightly that it can't escape until the functional program has logically completed executing. The high-level result (of some IO type) is logically an imperative program that the functional program built using functional composition with placeholders where the IO was supposed to happen.
But while I have to stretch to make this analogy, monads are sufficiently abstract that they could probably be made to fit many strained analogies...
To summarize: everyone, once they learn Haskell, comes up with their own analogy for "what monads are"... and the analogy, while it makes perfect sense to the person that came up with it, never helps anyone else because everyone gets to monads via a different route.
I have the perfect explanation for Monads: Monads are like everything that satisfies the three monad laws. (Of course this only helps mathematicians, if at all. Not mere mortals.)
Yeah. My mental picture is "thing with return/pure -> thing with fmap -> thing with join". The second is a pointed functor, the third is monad. Not sure what the first is, probably because it is nearly useless :)
You may have it backward. The mathematicians use "thing with fmap (functor) -> thing with return/pure (pointed functor) -> thing with join (monad)", as far as I know.
Arrows are another generalization of Monads that goes in a direction different from functors.
As I always say, I disagree about this. "Monad" is a property, the "is a" in "is a monad" does not mean the same thing as "is a pencil" or "is an airplane". It means the same thing as "red" does in "red apple" or "red cup" or "red piece of paper". If you look at one of those, and say "red is like an apple", you're just wrong... that's why nobody gets what you're talking about. As soon as you realize that "monad" is a property of types like "red" is a property of things in the physical world, then you have the understanding you need to be able to make "monads" make sense to you.
I'm not sure what I said that you are disagreeing with, but it's not clear to me that "monad" is strictly an adjective like "red".
My understanding is that a monad is a data type paired with a properly implemented bind and return (proper in the sense of obeying the monadic laws)... much like a monoid is a tuple with a binary operation and an identity element, a monad is a triple of bind, return, and the data structure.
In a practical sense, I find myself saying "this behaves like a monad" rather than "this is a monad" or "this is monadic" (although that last one is an adjective like you say). Once you recognize the that something behaves monadically, you are free to write the plumbing (bind and return) and use the abstraction if you wish.
Then again, I'm not a mathematician by any stretch of the imagination, and it's entirely possible I just completely missed the point you were trying to make. Just throwing out my thoughts.
I think we are saying the same thing. A monad is not a "nuclear waste container" or a "spacesuit". Nuclear waste containers and spacesuits could be monads. But "a implies b" does not mean "b implies a", and that's where people get confused.
Anyway, I think what I am trying to say is that the problem is a grammar issue, rather than a programming issue or a mathematical issue. Monads are easy to grasp in terms of math or programming. They are apparently quite difficult to explain, however.
A list (for instance) is not a monad. A list plus appropriately defined unit_list and bind_list together form a tuple which is a monad. That's the 'is a' sense of monads.
When you refer to a list itself, it's easier to think of it as having the adjective "monaded" since unit and bind are defined even if you don't usually carry them around with you. A list is a monad/has the properties of a monad because the appropriate definitions of unit and bind both can exist and are written.
1. n. Originally, a quick job that produces what is needed, but not well.
2. n. An incredibly good, and perhaps very time-consuming, piece of work that produces exactly what is needed.
They're also precisely the foundations of different notions of computation -- what we mean by ';' in an imperative language. So if math is a hack, then yeah. http://portal.acm.org/citation.cfm?id=116984
To the best of my knowledge, no. If memory serves me, Coq actually isn't even Turing-complete, being a typed lambda calculus with no general fixpoint operator (specifically, a variant on the Calculus of Constructions). Any "program" that "type checks" in Coq is thus provably terminating.
Note that, in Haskell terms, the simplest general fixpoint operator is:
y :: (t -> t) -> t
y f = f (y f)
...which, interpreting "->" as logical implication, is a theorem stating that a proposition implying its own truth implies its own truth. Given that (t -> t) is clearly a tautology, this suffices to prove all possible propositions, also known as the "principle of explosion". [0]
On the other hand, see http://ynot.cs.harvard.edu/ for an attempt to add side-effects and general recursion to Coq in a controlled fashion, in order to turn it into more of a programming language.
one odd thing reading through was the comment that A benefit of lazy evaluation is that you can write code like an Icon or Python generator that spins forever, returning a value on each cycle, and it will only be called for the exact number of returns that the enclosing program actually needs even if the caller is itself a generator.
that sounds to me like it's making a contrast with icon and python generators. but, as far as i understand things, that's just the same as icon + python. also, "even if..." was emphasised, and i don't understand why.
i suspect i've misread it or am missing something. would someone be kind enough to set me straight? thanks...
I believe GHC's type system is also Turing complete. As an example, you can implement BrainFuck in the GHC type system. I haven't looked over the details, but it looks promising.
Type-level computation is actually quite limited by default in GHC; it becomes quasi-Turing-complete only when using the UndecidableInstances extension, and even then it has a very shallow stack by default, though you can increase it if you want deeper recursion. If memory serves me, Oleg Kiselyov has a type-level implementation of the untyped lambda calculus, which is rather more pleasant than brainfuck.
Any reason why Haskell is so popular here? I spoke to people on Prgmr IRC and they were wondering too. I've learnt lisp in the past, but I have to wonder what benefits Haskell really offers that makes it so popular currently?
39 comments
[ 3.0 ms ] story [ 98.0 ms ] thread[1] Can anybody find the source of this quote?
I thought it was anonymous but Google tells me it is by Saki, who happens to be a terrific writer.
"Local color so you can sound like you know what you’re talking about: in Haskell-land, a closure is called a “thunk”."
Which just isn't true. A closure is called a closure and a thunk is called a thunk (as it is in Scheme and any number of other languages; there is nothing special about Haskell). For most of that article he should just replace the word 'closure' with 'thunk' and the issue would disappear.
A thunk is a suspended computation together with an environment. That is, a thunk is a special type of closure, where the function takes no arguments. Additionally, a thunk is updated with its result.
In GHC's execution model, the Spineless Tagless G-machine (STG), every heap object is actually a closure. That is, every heap object has a code pointer that can be called to return the object's value. For evaluated objects (including functions) that is essentially the identity function, for thunks this will evaluate as much as necessary, return, and possibly update it's heap object with its new value. Of course, there are several optimisations going on, but that's the basic idea.
So, I'd say a thunk is a special kind of closure.
A few nit-picks that come to mind; thunks and closures are related but different, every other language with thunks also calls them thunks.
Lisp is not really "based on lambda calculus" any more than any other imperative programming language; "(loop for i from 1 to 10 collect (+ i 42))" is not so different from a loop in assembler.
And finally, monads are not really a hack for making function application look like a sequence, that's already what function application does. Monads just let you run some extra code between function applications. But given that most people write stuff like, "monads are like nuclear-waste burritos inside of spacesuits" (er...), I am not going to complain about this explanation too loudly :)
But while I have to stretch to make this analogy, monads are sufficiently abstract that they could probably be made to fit many strained analogies...
http://byorgey.wordpress.com/2009/01/12/abstraction-intuitio...
To summarize: everyone, once they learn Haskell, comes up with their own analogy for "what monads are"... and the analogy, while it makes perfect sense to the person that came up with it, never helps anyone else because everyone gets to monads via a different route.
Arrows are another generalization of Monads that goes in a direction different from functors.
[0] http://ncatlab.org/nlab/show/monoid#examples_6
[1] http://james-iry.blogspot.com/2009/05/brief-incomplete-and-m...
That is all. :)
My understanding is that a monad is a data type paired with a properly implemented bind and return (proper in the sense of obeying the monadic laws)... much like a monoid is a tuple with a binary operation and an identity element, a monad is a triple of bind, return, and the data structure.
In a practical sense, I find myself saying "this behaves like a monad" rather than "this is a monad" or "this is monadic" (although that last one is an adjective like you say). Once you recognize the that something behaves monadically, you are free to write the plumbing (bind and return) and use the abstraction if you wish.
Then again, I'm not a mathematician by any stretch of the imagination, and it's entirely possible I just completely missed the point you were trying to make. Just throwing out my thoughts.
Anyway, I think what I am trying to say is that the problem is a grammar issue, rather than a programming issue or a mathematical issue. Monads are easy to grasp in terms of math or programming. They are apparently quite difficult to explain, however.
When you refer to a list itself, it's easier to think of it as having the adjective "monaded" since unit and bind are defined even if you don't usually carry them around with you. A list is a monad/has the properties of a monad because the appropriate definitions of unit and bind both can exist and are written.
Go read Moggi.
Depends. Monads are too linear, in a sense, to express some computations. Arrows express some things better.
I would say that Coq's type system (or some other Martin Lof type system) would be a logical limit.
(is there IO Monad in Coq?)
Again, nice article.
Indeed. Though it makes some sense as a figure of speech.
To the best of my knowledge, no. If memory serves me, Coq actually isn't even Turing-complete, being a typed lambda calculus with no general fixpoint operator (specifically, a variant on the Calculus of Constructions). Any "program" that "type checks" in Coq is thus provably terminating.
Note that, in Haskell terms, the simplest general fixpoint operator is:
...which, interpreting "->" as logical implication, is a theorem stating that a proposition implying its own truth implies its own truth. Given that (t -> t) is clearly a tautology, this suffices to prove all possible propositions, also known as the "principle of explosion". [0]On the other hand, see http://ynot.cs.harvard.edu/ for an attempt to add side-effects and general recursion to Coq in a controlled fashion, in order to turn it into more of a programming language.
[0] http://xkcd.com/704/
that sounds to me like it's making a contrast with icon and python generators. but, as far as i understand things, that's just the same as icon + python. also, "even if..." was emphasised, and i don't understand why.
i suspect i've misread it or am missing something. would someone be kind enough to set me straight? thanks...
I think that distinction should go to Qi. Derived from Common Lisp, but with a type system that's Turing-complete.
http://www.lambdassociates.org/doc.htm
http://killersmurf.blogspot.com/2009/11/typefuck.html
http://stackoverflow.com/questions/189172/c-templates-turing...