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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
