Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Fri, 2007-10-19 at 00:02 +0200, [EMAIL PROTECTED] wrote: Dan Weston writes: ... now I am totally flummoxed: thm1 :: (a - a) - a thm1 f = let x = f x in x thm1 (const 1) 1 I *thought* that the theorem ((a = a) = a) is not derivable (after all, 0^(0^0) = 0^1 = 0), but it appears somehow that thm1 is a proof of its type. Help, I just unlearned everything I ever thought I new about the C-H correspondence! No, the world is not so cruel. This is not a theorem, you cannot really derive it by constructing a polymorphic function, I cheated, because your statement was negligent. (const 1) is not a function of type (a-a), the only function *really* of that type is id. So the point is that, if a is a type such that the proofs of a are in one-to-one correspondence with the type Integer, then (a = a) = a *is* a theorem. In fact, so-called well-founded recursion corresponds to those proofs of a via (a = a) = a where the proof of a = a supplied is a valid (well-founded) induction step. Ill-founded recursion corresponds to illegitimate proof via the false rule a = a |- a. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Derek and Lennart, Thank you both for your clarifications. Tutorials (and blogs) of the C-H correspondence and the naive (i.e. set-theoretic) categorical descriptions of Haskell are so eager to get to the insights you mention that they gloss too easily over the important role of _|_, a term I have been learning to give more respect to every time I (re)read about the differences between sets and CPOs. If types correspond to theorems and terms correspond to proofs, then I guess program transformations correspond to rules of inference (e.g. function application flip ($) :: p - (p - q) - q corresponding to modus ponens), and what causes the inconsistency is an extra rule of inference implied by non-strict function application when applied to bottom allowing the proof \_ - undefined :: p - q What slightly bemuses me is that I would have thought this makes the proof procedure unsound, and consequently the insights into the logic Haskell's type system corresponds to not terribly insightful when analogized to intuitionist logic unless there were some computational way of restricting the proof system to a sound subset, which is what I was trying to get at by proposing to accept only proofs that terminated. Obviously, I've got a bit more reading to do before I can really understand all this. Dan Derek Elkins wrote: On Mon, 2007-10-22 at 01:12 +0100, Lennart Augustsson wrote: There's nothing wrong with Haskell types. It's the terms that make Haskell types an inconsistent logic. Logics are what are consistent or not, so saying the logic Haskell's type system corresponds to is inconsistent is all that can be said. Somewhere there is an axiom in it that makes forall a.(a - a) - a hold. Usually, we just take that directly as the axiom (i.e. the existence of fix). But that doesn't mean that the C-H correspondence doesn't have any insight to offer. Which is certainly not what I said at all. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
I must confess that I find choosing type Prop = CProp () to be slightly dangerous, since now CProp (const ()) :: Prop p and there is nothing in that expression that suggests non-termination (~ invalid proof). I would rather choose a type admitting only _|_ as its value: type Prop = CProp (forall a. a) or even the H98 (IIRC) type Prop = CProp Void newtype Void = Void Void Using another approach, I also tried data Prop p = Prop (forall r. (p - r) - r) but I was then unable to define propCC. Maybe this is because of the presence of the definable functions iso :: Prop p - p osi :: p - Prop p and so definifing propCC amounts to proving Peirce's law. (Still not sure about this...) Regards, Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Wed, 2007-10-17 at 15:06 -0700, Dan Weston wrote: That is a great tutorial. Thanks! But in the last two sentences of the introduction you say: We just need to find any program with the given type. The existence of a program for the type will be a proof of the corresponding proposition! Maybe you should make explicit that 1) the type is inhabited undefined :: forall p . p does not prove that all propositions are true Yes it does. 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x does not prove the (false) theorem (p = p) = p Yes it does. Terms in Haskell prove the propositions that the types of Haskell correspond to. *The logic that Haskell's type systems corresponds to is inconsistent.* This is what you are missing. Haskell's type systems does not correspond to intuitionistic propositional logic. Indeed, in the actual statement of the Curry-Howard correspondence, it's a correspondence between intuitionistic propositional logic and the simply typed lambda calculus which Haskell quite certainly is not. As is well known, it (CH) can be generalized beyond that, but generally you need a strongly normalizing language (or at least prove strong normalization for your particular term and note normalization means -normal form- not weak head normal form) to actually use the programs as proofs. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
There's nothing wrong with Haskell types. It's the terms that make Haskell types an inconsistent logic. But that doesn't mean that the C-H correspondence doesn't have any insight to offer. -- Lennart On 10/21/07, Derek Elkins [EMAIL PROTECTED] wrote: On Wed, 2007-10-17 at 15:06 -0700, Dan Weston wrote: That is a great tutorial. Thanks! But in the last two sentences of the introduction you say: We just need to find any program with the given type. The existence of a program for the type will be a proof of the corresponding proposition! Maybe you should make explicit that 1) the type is inhabited undefined :: forall p . p does not prove that all propositions are true Yes it does. 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x does not prove the (false) theorem (p = p) = p Yes it does. Terms in Haskell prove the propositions that the types of Haskell correspond to. *The logic that Haskell's type systems corresponds to is inconsistent.* This is what you are missing. Haskell's type systems does not correspond to intuitionistic propositional logic. Indeed, in the actual statement of the Curry-Howard correspondence, it's a correspondence between intuitionistic propositional logic and the simply typed lambda calculus which Haskell quite certainly is not. As is well known, it (CH) can be generalized beyond that, but generally you need a strongly normalizing language (or at least prove strong normalization for your particular term and note normalization means -normal form- not weak head normal form) to actually use the programs as proofs. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Hello, On 10/17/07, Lennart Augustsson [EMAIL PROTECTED] wrote: Check Wikipedia. Peirce law, law of excluded middle, double negation, ... they are all equivalent and it can be instructive to see how one can derive one from the other. Apparently these axioms are not all equivalent (I was quite surprised to learn that :-). Here is some interesting---but perhaps a bit advanced for a tutorial on CH---reading which studies the relation between classical logic and computation: http://coq.inria.fr/~herbelin/publis/icalp-AriHer03-minimal-classical.ps.gz -- Iavor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Mon, 2007-10-22 at 01:12 +0100, Lennart Augustsson wrote: There's nothing wrong with Haskell types. It's the terms that make Haskell types an inconsistent logic. Logics are what are consistent or not, so saying the logic Haskell's type system corresponds to is inconsistent is all that can be said. Somewhere there is an axiom in it that makes forall a.(a - a) - a hold. Usually, we just take that directly as the axiom (i.e. the existence of fix). But that doesn't mean that the C-H correspondence doesn't have any insight to offer. Which is certainly not what I said at all. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Thank you for that clarification, and I hope you will have patience for a follow-up question. I am really eager to fully understand this correspondence and appreciate any help. Your strong normalization induction does deconstruct function application but seemingly not constructor application, which I guess halts in System F at weak head normalization, so a theorem (Prop p) does not prove a theorem p. You said that: foo is a valid proof of a true theorem, but does not halt for the defined argument 'fix'. I assume you mean then that it is a valid proof because it halts for *some* argument? Suppose I have: thm1 :: (a - a) - a thm1 f = let x = f x in x There is no f for which (thm1 f) halts (for the simple reason that _|_ is the only value in every type), so thm1 is not a valid theorem. Now we reify our propositions (as the tutorial does) in a constructor: data Prop a = Prop a thm2 :: (Prop a - Prop a) - Prop a thm2 f = Prop undefined fix :: (p - p) - p fix f = let x = f x in x instance Show (Prop a) where show f = (Prop something) *Prop :t thm2 thm2 :: (Prop a - Prop a) - Prop a *Prop thm2 (fix id) (Prop something) Wow! thm2 halts. Valid proof. We have a proof (thm2 (fix id)) of a theorem (((Prop a) - (Prop a)) - (Prop a)), assuming that can somehow be mapped isomorphically to ((a - a) - a), thence to intuitionist logic as ((a = a) = a). That somehow in the tutorial seems to be an implied isomorphism from Prop a to a, so that proofs about (Prop a) can be interpreted as proofs about a. I hope to have shown that unless without constructors strict in their arguments that this is not valid. My hypothesis was that data Prop a = Prop !a justified this isomorphism. Or am I still just not getting it? Dan Stefan O'Rear wrote: On Wed, Oct 17, 2007 at 06:49:24PM -0700, Dan Weston wrote: It would seem that this induction on SN requires strictness at every stage. Or am I missing something? Yes you are missing something. Whether it exists in my message is less certain. First, note that the elements of SN[a] are lambda-terms, like (\x - x) (\x - x). Second, strong normalization means that *every* reduction sequence terminates. E.g. that term is strongly normalizing, since the only possible reduction leads to \x - x, from which no further reductions apply. Third, by inhabit...when passed, I mean that if TERM1 inhabits SN[a - b], and TERM2 inhabits SN[a], then (TERM1) (TERM2) inhabits SN[b]. No mention of evaluation required. Is it clear now? Stefan Stefan O'Rear wrote: On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote: 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x consider: foo :: ((a - a) - a) - a foo x = x id foo is a valid proof of a true theorem, but does not halt for the defined argument 'fix'. - An effective approach for handling this was found long ago in the context of prooving the strong normalization of the simply typed lambda calculus. Define a category of terms SN[a] for each type a by recursion on a. SN[a], for atomic a, consists of terms that halt. SN[a - b] consists of functions that inhabit SN[b] when passed an argument in SN[a]. With that definition, prooving that every term of the STLC of type a inhabits SN[a], and thus halts, becomess a trivial induction on the syntax of terms. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
I'm fairly new to this and struggling to follow along so I might be a little off base here... I assume you mean then that it is a valid proof because it halts for *some* argument? Suppose I have: thm1 :: (a - a) - a thm1 f = let x = f x in x There is no f for which (thm1 f) halts (for the simple reason that _|_ is the only value in every type), so thm1 is not a valid theorem. Now we reify our propositions (as the tutorial does) in a constructor: data Prop a = Prop a thm2 :: (Prop a - Prop a) - Prop a thm2 f = Prop undefined fix :: (p - p) - p fix f = let x = f x in x instance Show (Prop a) where show f = (Prop something) *Prop :t thm2 thm2 :: (Prop a - Prop a) - Prop a *Prop thm2 (fix id) (Prop something) Wow! thm2 halts. Valid proof. We have a proof (thm2 (fix id)) of a theorem (((Prop a) - (Prop a)) - (Prop a)), assuming that can somehow be mapped isomorphically to ((a - a) - a), thence to intuitionist logic as ((a = a) = a). The function needs to be total. You seem to be using Haskell to execute a function to see if it terminates as a proof of totality. Is that fair? This approach might work for some simple examples, but if the function doesn't terminate immediately then what? I would assume that proof of totality would be an obligation of the person who constructed the function. Using Haskell to prove termination for some simple cases might be fair (in which case I see your point about avoiding a non-lazy constructor), but it doesn't seem to be very general anyway. If you're relying on the programmer to provide proof of totality, then I don't see the harm in using Prop a instead of a. That somehow in the tutorial seems to be an implied isomorphism from Prop a to a, so that proofs about (Prop a) can be interpreted as proofs about a. I hope to have shown that unless without constructors strict in their arguments that this is not valid. My hypothesis was that data Prop a = Prop !a justified this isomorphism. Or am I still just not getting it? That would allow you to use the dynamic property (I observed termination) to verify the static property (the function is total) in some situations, right? But the static property of totality shouldn't rely on evaluation strategy, right? Dan Tim Newsham http://www.thenewsh.com/~newsham/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
The function needs to be total. You seem to be using Haskell to execute a function to see if it terminates as a proof of totality. Is that fair? This approach might work for some simple examples, but if the function doesn't terminate immediately then what? I would assume that proof of totality would be an obligation of the person who constructed the function. thm2 :: (Prop a - Prop a) - Prop a thm2 f = Prop undefined Prop is not total, but thm2 is (if I am not mistaken) total. Every non-_|_ f results in a non-bottom result (namely, Prop _|_). My (still hesitant) assertion is that the totality must be transitive to all sub-expressions for the function to be considered a valid proof. The easiest way to get Haskell to do this work for you is to make everything strict and just evaluate the function. Tim Newsham wrote: I'm fairly new to this and struggling to follow along so I might be a little off base here... I assume you mean then that it is a valid proof because it halts for *some* argument? Suppose I have: thm1 :: (a - a) - a thm1 f = let x = f x in x There is no f for which (thm1 f) halts (for the simple reason that _|_ is the only value in every type), so thm1 is not a valid theorem. Now we reify our propositions (as the tutorial does) in a constructor: data Prop a = Prop a thm2 :: (Prop a - Prop a) - Prop a thm2 f = Prop undefined fix :: (p - p) - p fix f = let x = f x in x instance Show (Prop a) where show f = (Prop something) *Prop :t thm2 thm2 :: (Prop a - Prop a) - Prop a *Prop thm2 (fix id) (Prop something) Wow! thm2 halts. Valid proof. We have a proof (thm2 (fix id)) of a theorem (((Prop a) - (Prop a)) - (Prop a)), assuming that can somehow be mapped isomorphically to ((a - a) - a), thence to intuitionist logic as ((a = a) = a). The function needs to be total. You seem to be using Haskell to execute a function to see if it terminates as a proof of totality. Is that fair? This approach might work for some simple examples, but if the function doesn't terminate immediately then what? I would assume that proof of totality would be an obligation of the person who constructed the function. Using Haskell to prove termination for some simple cases might be fair (in which case I see your point about avoiding a non-lazy constructor), but it doesn't seem to be very general anyway. If you're relying on the programmer to provide proof of totality, then I don't see the harm in using Prop a instead of a. That somehow in the tutorial seems to be an implied isomorphism from Prop a to a, so that proofs about (Prop a) can be interpreted as proofs about a. I hope to have shown that unless without constructors strict in their arguments that this is not valid. My hypothesis was that data Prop a = Prop !a justified this isomorphism. Or am I still just not getting it? That would allow you to use the dynamic property (I observed termination) to verify the static property (the function is total) in some situations, right? But the static property of totality shouldn't rely on evaluation strategy, right? Dan Tim Newsham http://www.thenewsh.com/~newsham/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Tim Newsham quotes somebody /I didn't follow this thread!/: I assume you mean then that it is a valid proof because it halts for *some* argument? Suppose I have: thm1 :: (a - a) - a thm1 f = let x = f x in x There is no f for which (thm1 f) halts (for the simple reason that _|_ is the only value in every type), so thm1 is not a valid theorem. = Since, as I said, I didn't follow you, it would be indecent of me to try to be clever now, but the statement above (that there is no f for which thm1 halts) is false *IN HASKELL*. Try f = const 1. Unless I missed some important point elsewhere... Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
It was I that he quoted, and now I am totally flummoxed: thm1 :: (a - a) - a thm1 f = let x = f x in x thm1 (const 1) 1 I *thought* that the theorem ((a = a) = a) is not derivable (after all, 0^(0^0) = 0^1 = 0), but it appears somehow that thm1 is a proof of its type. Help, I just unlearned everything I ever thought I new about the C-H correspondence! [EMAIL PROTECTED] wrote: Tim Newsham quotes somebody /I didn't follow this thread!/: I assume you mean then that it is a valid proof because it halts for *some* argument? Suppose I have: thm1 :: (a - a) - a thm1 f = let x = f x in x There is no f for which (thm1 f) halts (for the simple reason that _|_ is the only value in every type), so thm1 is not a valid theorem. = Since, as I said, I didn't follow you, it would be indecent of me to try to be clever now, but the statement above (that there is no f for which thm1 halts) is false *IN HASKELL*. Try f = const 1. Unless I missed some important point elsewhere... Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Dan Weston writes: ... now I am totally flummoxed: thm1 :: (a - a) - a thm1 f = let x = f x in x thm1 (const 1) 1 I *thought* that the theorem ((a = a) = a) is not derivable (after all, 0^(0^0) = 0^1 = 0), but it appears somehow that thm1 is a proof of its type. Help, I just unlearned everything I ever thought I new about the C-H correspondence! No, the world is not so cruel. This is not a theorem, you cannot really derive it by constructing a polymorphic function, I cheated, because your statement was negligent. (const 1) is not a function of type (a-a), the only function *really* of that type is id. People, use Djinn! The slave of the Lamp of Alladenartson will send you to Walhalla if you ask: what ? (a-a)-a Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Tue, Oct 16, 2007 at 08:03:52PM -1000, Tim Newsham wrote: A tutorial on the Curry-Howard Correspondence in Haskell: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ Feedback appreciated. Very clear and useful for me. Thank you for sharing it. Andrea ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Tim Newsham wrote: A tutorial on the Curry-Howard Correspondence in Haskell: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ Nice! Perhaps you should add a link to this on the wiki: http://haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence Thanks, Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Tim, I have also enjoyed the article, it's well written and easy enough to follow (at least for me). Slightly offtopic - I am curious about the use of forall in some type signatures: subsume :: forall p q r. Prop (p := q) - Prop ((p :/\ q) :== p) subsume pIMPq = equivInj (impInj pq2p) (impInj p2pq) where pq2p :: Prop (p :/\ q) - Prop p pq2p assumePQ = andElimL assumePQ p2pq :: Prop p - Prop (p :/\ q) p2pq assumeP = andInj assumeP q where q = impElim assumeP pIMPq There r type variable is mentioned, but it does not occur anywhere else in the signature - what's the purpose of this construct? Regards, -- Krzysztof Kościuszkiewicz Skype: dr.vee, Gadu: 111851, Jabber: [EMAIL PROTECTED] Mobile IRL: +353851383329, Mobile PL: +48783303040 Simplicity is the ultimate sophistication -- Leonardo da Vinci ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Very clear tutorial indeed. But why isn't propCC shown as Pierce's Law? And Excluded middle is proven on such basis. Vitaliy. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Slightly offtopic - I am curious about the use of forall in some type signatures: If you specify the forall p q at the top level then the types used internally will use the same p and q. Otherwise the internal types will be new ps and qs and wont line up with the outer type declaration. subsume :: forall p q r. Prop (p := q) - Prop ((p :/\ q) :== p) subsume pIMPq = equivInj (impInj pq2p) (impInj p2pq) where pq2p :: Prop (p :/\ q) - Prop p pq2p assumePQ = andElimL assumePQ p2pq :: Prop p - Prop (p :/\ q) p2pq assumeP = andInj assumeP q where q = impElim assumeP pIMPq There r type variable is mentioned, but it does not occur anywhere else in the signature - what's the purpose of this construct? Ahh! r is a remnant of earlier iterations where I had carried around the r in every CProp from the classical propositions. Then I realized I could just pick any r (I picked ()) and avoid having to type r everywhere. So its no longer used, and I'll remove it from the code and the paper. Thank you! Krzysztof Kościuszkiewicz Skype: dr.vee, Gadu: 111851, Jabber: [EMAIL PROTECTED] Mobile IRL: +353851383329, Mobile PL: +48783303040 Simplicity is the ultimate sophistication -- Leonardo da Vinci Tim Newsham http://www.thenewsh.com/~newsham/___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Very clear tutorial indeed. But why isn't propCC shown as Pierce's Law? And Excluded middle is proven on such basis. Simply because I don't know that much about pierce's law. I've seen it mentioned a few times, but I'm not that familiar with it yet and I haven't read a good treatment of it yet. Do you have any pointers to something I could read? Vitaliy. Tim Newsham http://www.thenewsh.com/~newsham/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Check Wikipedia. Peirce law, law of excluded middle, double negation, ... they are all equivalent and it can be instructive to see how one can derive one from the other. On 10/17/07, Tim Newsham [EMAIL PROTECTED] wrote: Very clear tutorial indeed. But why isn't propCC shown as Pierce's Law? And Excluded middle is proven on such basis. Simply because I don't know that much about pierce's law. I've seen it mentioned a few times, but I'm not that familiar with it yet and I haven't read a good treatment of it yet. Do you have any pointers to something I could read? Vitaliy. Tim Newsham http://www.thenewsh.com/~newsham/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
That is a great tutorial. Thanks! But in the last two sentences of the introduction you say: We just need to find any program with the given type. The existence of a program for the type will be a proof of the corresponding proposition! Maybe you should make explicit that 1) the type is inhabited undefined :: forall p . p does not prove that all propositions are true 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x does not prove the (false) theorem (p = p) = p even though (fix id) is well-typed and id is certainly not undefined (though fix id is). Tim Newsham wrote: A tutorial on the Curry-Howard Correspondence in Haskell: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ Feedback appreciated. Tim Newsham http://www.thenewsh.com/~newsham/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Also, I was wondering if the constructor and/or function arguments should be marked strict. Otherwise, types can be inhabited by defined arguments. Since Prop is not strict in its argument, we could have the (false) theorem andAlwaysTrue :: forall p q . p :/\ q andAlwaysTrue p q = And (Prop undefined) (Prop undefined) This halts for all p and q since Prop and And are not strict. Dan Weston wrote: That is a great tutorial. Thanks! But in the last two sentences of the introduction you say: We just need to find any program with the given type. The existence of a program for the type will be a proof of the corresponding proposition! Maybe you should make explicit that 1) the type is inhabited undefined :: forall p . p does not prove that all propositions are true 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x does not prove the (false) theorem (p = p) = p even though (fix id) is well-typed and id is certainly not undefined (though fix id is). Tim Newsham wrote: A tutorial on the Curry-Howard Correspondence in Haskell: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ Feedback appreciated. Tim Newsham http://www.thenewsh.com/~newsham/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
Tim Newsham writes: A tutorial on the Curry-Howard Correspondence in Haskell: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ Feedback appreciated. Did I miss it (then I apologize), or that tutorial doesn't even mention Djinn (in which case the Author should). Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote: 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x consider: foo :: ((a - a) - a) - a foo x = x id foo is a valid proof of a true theorem, but does not halt for the defined argument 'fix'. - An effective approach for handling this was found long ago in the context of prooving the strong normalization of the simply typed lambda calculus. Define a category of terms SN[a] for each type a by recursion on a. SN[a], for atomic a, consists of terms that halt. SN[a - b] consists of functions that inhabit SN[b] when passed an argument in SN[a]. With that definition, prooving that every term of the STLC of type a inhabits SN[a], and thus halts, becomess a trivial induction on the syntax of terms. Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
_|_ does not provide a witness to a theorem in any consistent logic (otherwise everything could be proved from it), yet it inhabits every type in Haskell. If the only invalid type instance is _|_, then a necessary and sufficient test for the C-H correspondence be the existence of a type instance that halts. Non-strict constructors would seem to mess that up. From http://en.wikipedia.org/wiki/Curry%E2%80%93Howard#Types The problem of finding a ?-expression with a particular type is called the type inhabitation problem. The answer turns out to be remarkable: There is a closed ?-expression with a particular type only if the type corresponds to a theorem of logic, when the ? symbols are re-interpreted as meaning logical implication. By inhabit, they clearly mean no occurrence (recursively) in the type instance of _|_. I think the extra wrinkle you are introducing with constructors like Prop to wrap types is justified only insofar as the boxed and unboxed types are isomorphic, but they are not unless the constructor is strict in all its arguments. Just as _|_ :: a does not qualify as justifying theorem a, so in isomorphism Prop _|_ :: Prop a should also not qualify. If all constructors were strict, Prop _|_ = _|_ and all is fine. I am posting this to the haskell-cafe list because I am not at all sure that my understanding is right, and I don't want you to change your tutorial if it's not. Dan Weston Tim Newsham wrote: Also, I was wondering if the constructor and/or function arguments should be marked strict. Otherwise, types can be inhabited by defined arguments. Since Prop is not strict in its argument, we could have the (false) theorem andAlwaysTrue :: forall p q . p :/\ q andAlwaysTrue p q = And (Prop undefined) (Prop undefined) This halts for all p and q since Prop and And are not strict. Hmm.. I'm wondering to what degree this would make a difference. I'm not actually running any of these programs. I'm just compiling them and relying on the type checker to validate the types (and check the proofs). If I understand this correctly, adding ! wont affect the behavior of the type checking phase. Dan Weston wrote: That is a great tutorial. Thanks! But in the last two sentences of the introduction you say: We just need to find any program with the given type. The existence of a program for the type will be a proof of the corresponding proposition! Maybe you should make explicit that 1) the type is inhabited undefined :: forall p . p does not prove that all propositions are true 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x does not prove the (false) theorem (p = p) = p even though (fix id) is well-typed and id is certainly not undefined (though fix id is). Tim Newsham wrote: A tutorial on the Curry-Howard Correspondence in Haskell: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ Feedback appreciated. Tim Newsham http://www.thenewsh.com/~newsham/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe Tim Newsham http://www.thenewsh.com/~newsham/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
It would seem that this induction on SN requires strictness at every stage. Or am I missing something? Stefan O'Rear wrote: On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote: 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x consider: foo :: ((a - a) - a) - a foo x = x id foo is a valid proof of a true theorem, but does not halt for the defined argument 'fix'. - An effective approach for handling this was found long ago in the context of prooving the strong normalization of the simply typed lambda calculus. Define a category of terms SN[a] for each type a by recursion on a. SN[a], for atomic a, consists of terms that halt. SN[a - b] consists of functions that inhabit SN[b] when passed an argument in SN[a]. With that definition, prooving that every term of the STLC of type a inhabits SN[a], and thus halts, becomess a trivial induction on the syntax of terms. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Wed, Oct 17, 2007 at 06:45:04PM -0700, Dan Weston wrote: _|_ does not provide a witness to a theorem in any consistent logic (otherwise everything could be proved from it), yet it inhabits every type in Haskell. If the only invalid type instance is _|_, then a necessary and sufficient test for the C-H correspondence be the existence of a type instance that halts. Non-strict constructors would seem to mess that up. From http://en.wikipedia.org/wiki/Curry%E2%80%93Howard#Types The problem of finding a ?-expression with a particular type is called the type inhabitation problem. The answer turns out to be remarkable: There is a closed ?-expression with a particular type only if the type corresponds to a theorem of logic, when the ? symbols are re-interpreted as meaning logical implication. By inhabit, they clearly mean no occurrence (recursively) in the type instance of _|_. I think the extra wrinkle you are introducing with constructors like Prop to wrap types is justified only insofar as the boxed and unboxed types are isomorphic, but they are not unless the constructor is strict in all its arguments. Just as _|_ :: a does not qualify as justifying theorem a, so in isomorphism Prop _|_ :: Prop a should also not qualify. If all constructors were strict, Prop _|_ = _|_ and all is fine. I am posting this to the haskell-cafe list because I am not at all sure that my understanding is right, and I don't want you to change your tutorial if it's not. This is fine, but function types complicate the issue dramatically. In the CPO interpretation (from whence ⊥ originates), a function type is to be regarded as a product with one value of the co-domain for each value of the domain. If you force function types to be strict, you require the function to never produce ⊥, which gets you right back where you started - functions must be total. Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Wed, Oct 17, 2007 at 06:49:24PM -0700, Dan Weston wrote: It would seem that this induction on SN requires strictness at every stage. Or am I missing something? Yes you are missing something. Whether it exists in my message is less certain. First, note that the elements of SN[a] are lambda-terms, like (\x - x) (\x - x). Second, strong normalization means that *every* reduction sequence terminates. E.g. that term is strongly normalizing, since the only possible reduction leads to \x - x, from which no further reductions apply. Third, by inhabit...when passed, I mean that if TERM1 inhabits SN[a - b], and TERM2 inhabits SN[a], then (TERM1) (TERM2) inhabits SN[b]. No mention of evaluation required. Is it clear now? Stefan Stefan O'Rear wrote: On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote: 2) the function must halt for all defined arguments fix :: forall p . (p - p) - p fix f = let x = f x in x consider: foo :: ((a - a) - a) - a foo x = x id foo is a valid proof of a true theorem, but does not halt for the defined argument 'fix'. - An effective approach for handling this was found long ago in the context of prooving the strong normalization of the simply typed lambda calculus. Define a category of terms SN[a] for each type a by recursion on a. SN[a], for atomic a, consists of terms that halt. SN[a - b] consists of functions that inhabit SN[b] when passed an argument in SN[a]. With that definition, prooving that every term of the STLC of type a inhabits SN[a], and thus halts, becomess a trivial induction on the syntax of terms. Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
