[Haskell-cafe] lambda calculus and equational logic

[Ben Lippmeier]

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.