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.

In Haskell what roles are played by 1)lambda calculus and 2) equational logic? Are these roles related?

Hi, 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. Semantics can be understood under three headings: *Denotational Semantics; is a model theoretical approach which describes a program in terms of precise mathematical objects (e.g. sets and functions) which provide meaning to a program text. *Operational semantics: provides a technique for computing a result, ELs use term rewriting systems for their operational semantics. *Proof theoretic semantic: syntactically derivable proofs, can use the rules of a logic 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 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. Thanks, Pat This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie

Patrick Browne wrote:

...

In Haskell what roles are played by 1)lambda calculus and 2) equational logic? Are these roles related?

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.

Semantics can be understood under three headings: *Denotational Semantics; is a model theoretical approach which describes a program in terms of precise mathematical objects (e.g. sets and functions) which provide meaning to a program text. *Operational semantics: provides a technique for computing a result, ELs use term rewriting systems for their operational semantics. *Proof theoretic semantic: syntactically derivable proofs, can use the rules of a logic

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

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.

Lambda calculus is the basis for all three types of semantics: 1) Call-by-need (usually, implementations of Haskell are free to choose other evaluation strategies as long as the denotational semantics match) 2) The denotational semantics of a lambda calculus with general recursion, see also http://en.wikibooks.org/wiki/Haskell/Denotational_semantics 3) Not sure what you mean by proof theoretic semantics. Apparently, the trace of any program execution like, say product [1..5] -> 1 * product [2..5] -> .. -> 120 is a proof that the initial and the final expression denote the same value. The Curry-Howards correspondence is about the type system, viewing types as logical propositions and programs as their proofs. Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com

Patrick Browne wrote:

Heinrich Apfelmus wrote:

...

3) Not sure what you mean by proof theoretic semantics. Apparently, the trace of any program execution like, say

product [1..5] -> 1 * product [2..5] -> .. -> 120

is a proof that the initial and the final expression denote the same value.

The Curry-Howards correspondence is about the type system, viewing types as logical propositions and programs as their proofs.

This seems to address the first point (the role of lambda calculus. But what of the second point, the role equational logic. I assume (perhaps incorrectly) that lambda calculus is not *a logic*. See: http://lambda-the-ultimate.org/node/3719

That depends a lot on what you think "logic" means. Certainly we should be willing to call Haskell's type system a logic, with the term-level serving as proofs of the types/propositions (by Curry/Howard). It's a woefully inconsistent logic[1], sure, but a logic nevertheless. Whether we would want to call the term-level a logic is a different matter. And this is where we get into terminological disputes; e.g., to what extent are algebraic systems different/similar to logical systems? (and to what extent are computational systems similar/different to algebraic systems?) This isn't just an issue of terminology: it throws a spotlight on elephants hiding in the room, elephants such as whether all mathematics can be reduced to logic, what the relationship is between logic and language, etc. Mathematicians, logicians, philosophers, theoretical linguists, and computer scientists all have a stake in those arguments--- a stake which is, at best, tangential to the actual question, and therefore makes it hard to get a decent answer/discussion. Equational logic is used heavily for reasoning about programs in Haskell (and pure functional languages generally). It shows up in the safety proofs for the type system, correctness proofs for compilers, strictness analysis, optimizations, etc. However, as you mention in that LtU post, equational reasoning doesn't really show up *in* Haskell, only in reasoning *about* Haskell. Without dependent types or a more developed formal language for reasoning with RULES and proving their correctness, it does not seem possible to support equational reasoning within Haskell (except in the most trivial sense that defining functions is defining a system of equations). It's not clear to me whether you're asking about equational reasoning for theory or metatheory. Also, because the type system is inconsistent, that raises the question of what it could mean to reason in such a logic. Logicians throw up their hands whenever a logic is inconsistent, but computer scientists have been reasoning with inconsistency for years. In discussing a constructive LEM, Oleg highlights some interesting connections between the idea of monads-as-computation and well-known results about how the boundary of computability separates the space of Classical and Intuitionistic theorems. Issues of inconsistency also show up in reasoning about language-based security systems where sometimes we may wish to allow inconsistent states during computation so long as there is a formal guarantee that consistency is restored soon. But overall, the question of what it means to reason formally and correctly in the face of an inconsistent system is still an open question. [1] Because of bottom, as well as many other reasons: http://okmij.org/ftp/Haskell/types.html#fix [2] http://okmij.org/ftp/Computation/lem.html -- Live well, ~wren

On Jul 14, 2010, at 1:51 AM, Ben Lippmeier wrote:

Replacing equals by equals usually doesn't change anything.

What kind of equality do you use for getChar :: IO Char ?

The usual one: getChar = getChar. It's a pure value. If I find [getChar,getChar] in a program, I can safely replace it by let g = getChar in [g,g].