[Haskell-cafe] lambda calculus and equational logic

[Brent Yorgey]

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