[Haskell-cafe] lambda calculus and equational logic
benl at ouroborus.net
Tue Jul 13 09:51:08 EDT 2010
On 13/07/2010, at 20:47 , Brent Yorgey wrote:
> On Wed, Jul 07, 2010 at 09:56:08AM +0100, Patrick Browne wrote:
>> 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
> 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."
More information about the Haskell-Cafe