On 13/07/2010, at 20:47 , Brent Yorgey wrote:
On Wed, Jul 07, 2010 at 09:56:08AM +0100, Patrick Browne wrote:
Hi, In Haskell what roles are played by 1)lambda calculus and 2) equational logic? Are these roles related?
Hopefully this question can be answered at a level suitable for this forum.
Since no one else has responded I'll take a quick stab at answering, and others can fill in more information as appropriate, or ask further questions.
2) Haskell is able to embrace equational logic because of its insistence on purity: in a Haskell program (leaving aside for the moment things like seq and unsafePerformIO) you can always "replace equals by equals" (where equality is the normal beta-equality for System F omega, plus definitional equality introduced by Haskell declarations) without changing the semantics of your program. So the story of an equational logic for System F omega and the story of evaluating Haskell programs are to a large extent the same story.
Replacing equals by equals usually doesn't change anything. What kind of equality do you use for getChar :: IO Char ?
Coming up with equational logics corresponding to most imperative languages (or even a non-pure functional language like OCaml) is massively complicated by the need to keep track of an implicit "state of the world" due to the presence of side effects.
By "massively complicated" you mean "harder than the simplest case." Haskell's do-notation makes the "state of the world" implicit, and performing the desugaring makes it explicit again -- but then that state isn't really "the state of the word"... Sorry or my heckling. You gave a fine answer, to the standard question. However, I propose mandating that all such questions asked on the haskell-beginners list are answered with "Haskell's purity solves everything" -- but on haskell-cafe they should get "Haskell's purity solves everything, but read Sabry's paper on What is a Purely Functional Language, because it's really more subtle than that." Cheers, Ben.