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 "p"s and "q"s 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: kokr@jabberpl.org Mobile IRL: +353851383329, Mobile PL: +48783303040 "Simplicity is the ultimate sophistication" -- Leonardo da Vinci

Tim Newsham http://www.thenewsh.com/~newsham/

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/

Hello, On 10/17/07, Lennart Augustsson 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

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

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

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:

...

...

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'.

On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote: - 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

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/

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! jerzy.karczmarczuk@info.unicaen.fr 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

On Fri, 2007-10-19 at 00:02 +0200, jerzy.karczmarczuk@info.unicaen.fr 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

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 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

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.