7 ms·

On Learning Haskell

74 points by karlzt 17y ago

Xichekolas 17y ago
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.
- eru 17y ago
  Careful lying may aid in explaining. [1] The author knows the difference. [1] Can anybody find the source of this quote?
  - jsyedidia 17y ago
    The author feels that this technique of deliberate lying will actually make it easier for you to learn the ideas. --- Donald E Knuth, The TeXbook
    - eru 17y ago
      Thanks! That's what I was searching for.
  - nandemo 17y ago
    "A little inaccuracy sometimes saves a ton of explanation." I thought it was anonymous but Google tells me it is by Saki, who happens to be a terrific writer.
    - eru 17y ago
      Thanks. That's close, but not what I had in mind.
- kscaldef 17y ago
  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.
  - Xichekolas 17y ago
    But he does draw direct equivalence: "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.
- carterschonwald 17y ago
  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
- nominolo 17y ago
  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. So, I'd say a thunk is a special kind of closure.
- dfranke 17y ago
  See comment #3 on the blog :-)
jrockway 17y ago
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 :)
- barrkel 17y ago
  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...
  - Xichekolas 17y ago
    When jrockway said the burrito thing, I think he was referring to the Brent Yorgey post about the "monad tutorial fallacy": http://byorgey.wordpress.com/2009/01/12/abstraction-intuition-and-the-monad-tutorial-fallacy/ 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.
stralep 17y ago
Nice article, but Haskell type system is not a logical limit. 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.
- eru 17y ago
  > Nice article, but Haskell type system is not a logical limit. Indeed. Though it makes some sense as a figure of speech.
- camccann 17y ago
  (is there IO Monad in Coq?) 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/ 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/ http://xkcd.com/704/
andrewcooke 17y ago
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...
mnemonicsloth 17y ago
Haskell pushes [static typing] to some sort of logical limit. 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://www.lambdassociates.org/doc.htm
- Periodic 17y ago
  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. http://killersmurf.blogspot.com/2009/11/typefuck.html http://killersmurf.blogspot.com/2009/11/typefuck.html
  - camccann 17y ago
    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.
- sreque 17y ago
  Isn't c++'s type system also turing complete via templates? http://stackoverflow.com/questions/189172/c-templates-turing-complete http://stackoverflow.com/questions/189172/c-templates-turing...
  - eru 17y ago
    Yes, but in the same sense that Brainfuck is..
Auzy 17y ago
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?

74 points by karlzt 17y ago

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.

eru 17y ago
Careful lying may aid in explaining. [1] The author knows the difference. [1] Can anybody find the source of this quote?
- jsyedidia 17y ago
  The author feels that this technique of deliberate lying will actually make it easier for you to learn the ideas. --- Donald E Knuth, The TeXbook
  - eru 17y ago
    Thanks! That's what I was searching for.
- nandemo 17y ago
  "A little inaccuracy sometimes saves a ton of explanation." I thought it was anonymous but Google tells me it is by Saki, who happens to be a terrific writer.
  - eru 17y ago
    Thanks. That's close, but not what I had in mind.
kscaldef 17y ago
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.
- Xichekolas 17y ago
  But he does draw direct equivalence: "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.
carterschonwald 17y ago
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
nominolo 17y ago
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. So, I'd say a thunk is a special kind of closure.
dfranke 17y ago
See comment #3 on the blog :-)

jrockway 17y ago

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 :)

barrkel 17y ago
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...
- Xichekolas 17y ago
  When jrockway said the burrito thing, I think he was referring to the Brent Yorgey post about the "monad tutorial fallacy": http://byorgey.wordpress.com/2009/01/12/abstraction-intuition-and-the-monad-tutorial-fallacy/ 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.

stralep 17y ago

Nice article, but Haskell type system is not a logical limit. 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.

eru 17y ago
> Nice article, but Haskell type system is not a logical limit. Indeed. Though it makes some sense as a figure of speech.
camccann 17y ago
(is there IO Monad in Coq?) 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/ 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/ http://xkcd.com/704/

andrewcooke 17y ago

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...

mnemonicsloth 17y ago

Haskell pushes [static typing] to some sort of logical limit. 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://www.lambdassociates.org/doc.htm

Periodic 17y ago
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. http://killersmurf.blogspot.com/2009/11/typefuck.html http://killersmurf.blogspot.com/2009/11/typefuck.html
- camccann 17y ago
  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.
sreque 17y ago
Isn't c++'s type system also turing complete via templates? http://stackoverflow.com/questions/189172/c-templates-turing-complete http://stackoverflow.com/questions/189172/c-templates-turing...
- eru 17y ago
  Yes, but in the same sense that Brainfuck is..

Auzy 17y ago

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?