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. 1) In general, the lambda calculus is seen as foundational conceptual basis for functional programming: Haskell has anonymous lambda expressions, higher-order functions, and currying, all of which come directly from the lambda calculus. More specifically, GHC's core language is based on a variant of System F omega, which is a fancy version of the simply-typed lambda calculus with polymorphism and type constructors. If you were to print out the core language code generated by GHC for some Haskell program, you would essentially see a bunch of lambda calculus expressions. 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. 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. I am not sure what to say about their relationship. Perhaps my above answers have already shed some light on that. -Brent