Re: [Haskell-cafe] lambda calculus and equational logic
Patrick Browne wrote: Hi, In Haskell what roles are played by 1)lambda calculus and 2) equational logic? Are these roles related? I think this thread is getting a bit too theoretical, so I moved it to http://lambda-the-ultimate.org/node/4014 Thanks for putting the time and effort into your really helpful replies. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda calculus and equational logic
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda calculus and equational logic
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
Re: [Haskell-cafe] lambda calculus and equational logic
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda calculus and equational logic
Ben, comments from the peanut gallery: On 13/07/2010, at 11:51 PM, Ben Lippmeier wrote: What kind of equality do you use for getChar :: IO Char ? Surely this is easy: getChar denotes a particular IO action, which is always the same thing (i.e. self-identical and distinct from all other IO actions). 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... ... which tells you that the passing-the-world semantics is not a faithful model of I/O. In the archives of this list there are many comments on exactly this topic. A couple of quick pointers: - Wouter Swierstra wrote a paper on this. http://www.cse.chalmers.se/~wouter/repos/IOSpec/index.html - Resumptions are a better model: http://www.haskell.org/pipermail/haskell-cafe/2003-August/004892.html Intuitively the state monad used by GHC works because it only needs to track dependencies between I/O actions - there is no need for the compiler to impose a total order on everything going on in the world (taken to be all of the context that could influence the execution of the program). For interesting programs it cannot, anyway. cheers peter -- http://peteg.org/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda calculus and equational logic
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda calculus and equational logic
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]. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] lambda calculus and equational logic
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. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
