[Haskell-cafe] lambda calculus and equational logic

[Ben Lippmeier]

On 14/07/2010, at 6:26 , Patrick Browne wrote:

> Thanks for your clear and helpful responses.
> I am aware that this question can lead to into very deep water.
> I am comparing Haskell with languages based on equational logic (EL)
> (e.g. Maude/CafeOBJ, lets call them ELLs).  I need to identify the
> fundamental distinction between the semantics of ELLs and Haskell. The
> focus of my original question was just the purely functional, side
> effect free, part of Haskell.

If you ignore anything to do with the IO monad (or ST), then all of Haskell can be desugared to (untyped) call-by-name/need lambda calculus. If you stick with Haskell98 then you can desugar it to the rank-2 fragment of System-F + algebraic data types + case expressions + appropriate constants and primops. This is generally regarded as the "Haskell Kernel Language", which is mentioned but explicitly not defined in the language standard.


> The relationship between the denotational and the proof theoretic
> semantic is important for soundness and completeness. Which was sort of
> behind my original question.
> 
> Would it be fair to say
> 1) Lambda calculus provides the operational semantics for Haskell

Notionally yes, but practically no. AFAIC there isn't a formal semantics for Haskell, but there is for fragments of it, and for intermediate representations like System-Fc (on which GHC is based). There are also multiple lambda calculi, depending on which evaluation mechanism you use.

The point I was trying to make in the previous message is what while "Haskell" includes the IO monad, people insist on calling the whole language "purely functional" and "side effect free", which is murky territory. Sabry's "What is a Purely Functional Language" shows that unrestricted beta-reduction is not sound in a simple monadic language using a pass-the-world implementation -- though Wouter's paper gives a cleaner one. Another paper that might help is Sondergaard and Sestoft's highly readable "Referential Transparency, Definiteness and Unfoldability".


> 2) Maybe equational logic provides the denotational semantics.
> 3)I am not sure of proof theoretic semantic for Haskell.
>  The Curry-Howard correspondence is a proof theoretic view but only at
>  type level.
> 
> Obviously, the last three points are represent my efforts to address
> this question. Hopefully the café can comment on the accuracy of these
> points.

My (limited) understanding of Maude is that rewrites can happen at any point in the term being reduced. This is different from, say, the semantics of call-by-name lambda calculus which has a specific evaluation order. In Haskell it's no problem to pass a diverging expression to some function, which might store it in a data structure, but then discard it later. However, when rewrites can happen at any point in the term being reduced, if any part of it diverges then the whole thing does. This is just from skimming slides for Maude talks though...

Ben.