Higher order types via the Curry-Howard correspondence

Gaal Yahas

10 May 2007 10 May '07

3:47 a.m.

What do higher-order types like lists mean when viewed through the Curry-Howard correspondence? I've been wondering about this for a while. The tutorials ask me to consider id :: forall a. a -> a (.) :: forall a b c. (b -> c) -> (a -> b) -> (a -> c) These represent theorems in a logical calculus, with the variables a, b, c denoting propositions. In the case of the composition function, the proposition (a -> c) may be deduced if (b -> c) and (a -> b) obtain, and so on. (I've obviously skimmed some details.) We know the function e :: a -> b diverges because there is no way to deduce b from a with no other premises; the only value that satisfies this is bottom -- and so on. But what does the following mean? map :: (a -> b) -> [a] -> [b] Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead: data Stream a = SHead a (Stream a) sMap :: (a -> b) -> Stream a -> Stream b What is the object "Stream a" in logic? What inference rules may be applied to it? How is "data Stream" introduced, and what about variant constructors? -- Gaal Yahas http://gaal.livejournal.com/

Show replies by date

DavidA

11 May 11 May

3:04 p.m.

New subject: Higher order types via the Curry-Howard correspondence

Gaal Yahas writes:

...

What do higher-order types like lists mean when viewed through the Curry-Howard correspondence?

Okay well I don't know the complete answer, but since no one else has answered I'll have a go. Suppose we define our own version of list as data List a = Nil | Cons a (List a) This is the traditional "sum of products" Haskell data type. In Curry-Howard, it corresponds to a disjunction of conjunctions. For example, if we had data X a b c d = Y a b | Z c d then the right-hand side corresponds to a&b | c&d. In the case of List a, the first conjunction (Nil) is empty, which in Curry- Howard corresponds to T (truth). So the right-hand side corresponds to T | a&(List a). The tricky bit is how to handle that recursive mention of List a. There is an explanation in Chapter 20 of Pierce, Types and Programming Languages, but it involves introducing new machinery.

Benja Fallenstein

3:58 p.m.

Adding some thoughts to what David said (although I don't understand the issues deeply enough to be sure that these ideas don't lead to ugly things like paradoxes)-- 2007/5/10, Gaal Yahas :

...

Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead:

data Stream a = SHead a (Stream a) sMap :: (a -> b) -> Stream a -> Stream b

What is the object "Stream a" in logic?

It's not that much more interesting than "list." The 'data' declaration can be read as, "To prove the proposition (Stream a), you must prove the proposition 'a' and the proposition 'Stream a.'" In ordinary logic this would mean that you couldn't prove (Stream a), of course, but that just corresponds to strict languages in which you couldn't construct an object of type Stream a (because it would have to be infinite). To make sense of this, we need to assume a logic in which we can have similar 'infinite proofs.' (This is the part where I'm not sure it's really possible to do. I haven't read the Pierce chapter David refers to.) With that reading, (Stream a) is basically the same proposition as (a) -- as evidenced by f x = SHead x (f x) -- f :: a -> Stream a g (SHead x) = x -- g :: Stream a -> a We can find more interesting propositions, though. Here's an example (perhaps not useful, but I find it interesting :-)): data Foo a b = A a | Fn (Foo a b -> b) We can prove this proposition if we can prove one of these propositions: a a -> b (a -> b) -> b ((a -> b) -> b) -> b ... Each of these is weaker than the previous one; if x is a proof of proposition n, then (\f -> f x) is a proof of proposition n+1. The fourth one is a tautology in classical logic, but not in intuitionistic logic. - Benja

Derek Elkins

6:19 p.m.

New subject: Higher order types via the Curry-Howard correspondence

Benja Fallenstein wrote:

...

Adding some thoughts to what David said (although I don't understand the issues deeply enough to be sure that these ideas don't lead to ugly things like paradoxes)--

2007/5/10, Gaal Yahas :

...
Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead:

data Stream a = SHead a (Stream a) sMap :: (a -> b) -> Stream a -> Stream b

What is the object "Stream a" in logic?

A coinductive type. Lookup things like codata and coalgebra. List and algebraic data types are inductive. In Haskell codata and data coincide, but if you want consistency, that cannot be the case.

Benja Fallenstein

13 May 13 May

2:52 p.m.

2007/5/12, Derek Elkins :

...

In Haskell codata and data coincide, but if you want consistency, that cannot be the case.

For fun and to see what you have to avoid, here's the proof of Curry's paradox, using weird infinite data types. We'll construct an expression that inhabits any type a. (Of course, you could just write (let x=x in x). If you want consistency, you have to outlaw that one, too. :-)) I'll follow the proof on Wikipedia: http://en.wikipedia.org/wiki/Curry's_paradox data Curry a = Curry { unCurry :: Curry a -> a } id :: Curry a -> Curry a f :: Curry a -> (Curry a -> a) f = unCurry . id g :: Curry a -> a g x = f x x c :: Curry a c = Curry g paradox :: a paradox = g c Modulo the constructor and destructor invocation, this is just the familiar non-terminating ((\x -> x x) (\x -> x x)), of course. - Benja

Benja Fallenstein

3:23 p.m.

2007/5/13, Benja Fallenstein :

...

Modulo the constructor and destructor invocation, this is just the familiar non-terminating ((\x -> x x) (\x -> x x)), of course.

The same technique also gives us data Y a = Y (Y a -> a) y :: (a -> a) -> a y f = (\(Y x) -> f $ x $ Y x) $ Y $ (\(Y x) -> f $ x $ Y x) or y :: (a -> a) -> a y f = g (Y g) where g (Y x) = f $ x $ Y x as well as these formulations, which make GHC loop forever on my system: y :: (a -> a) -> a y f = (\(Y x) -> f (x (Y x))) (Y (\(Y x) -> f (x (Y x)))) y :: (a -> a) -> a y f = g (Y g) where g (Y x) = f (x (Y x)) (Aaah, the power of the almighty dollar. Even type inference isn't safe from it.) - Benja

Scott Turner

15 May 15 May

10:28 p.m.

On 2007 May 13 Sunday 14:52, Benja Fallenstein wrote:

...

2007/5/12, Derek Elkins :

...
In Haskell codata and data coincide, but if you want consistency, that cannot be the case.

For fun and to see what you have to avoid, here's the proof of Curry's paradox, using weird infinite data types.

I've had some fun with it, but need to be led by the nose to know what to avoid. Which line or lines of the below Haskell code go beyond what can be done in a language with just data? And which line or lines violate what can be done with codata?

...

We'll construct an expression that inhabits any type a. (Of course, you could just write (let x=x in x). If you want consistency, you have to outlaw that one, too. :-))

I'll follow the proof on Wikipedia: http://en.wikipedia.org/wiki/Curry's_paradox

data Curry a = Curry { unCurry :: Curry a -> a }

id :: Curry a -> Curry a

f :: Curry a -> (Curry a -> a) f = unCurry . id

g :: Curry a -> a g x = f x x

c :: Curry a c = Curry g

paradox :: a paradox = g c

Stefan O'Rear

10:44 p.m.

On Tue, May 15, 2007 at 10:28:08PM -0400, Scott Turner wrote:

...

On 2007 May 13 Sunday 14:52, Benja Fallenstein wrote:

...
2007/5/12, Derek Elkins :

...
In Haskell codata and data coincide, but if you want consistency, that cannot be the case.

For fun and to see what you have to avoid, here's the proof of Curry's paradox, using weird infinite data types.

I've had some fun with it, but need to be led by the nose to know what to avoid. Which line or lines of the below Haskell code go beyond what can be done in a language with just data? And which line or lines violate what can be done with codata?

There is nothing wrong with having both codata and data in a consistent language. For instance, in System Fω, you can have both []: λ(el : *). ∀(res : *). (el → res → res) → res → res and co-[]: λ(el : *). ∀(res : *). (∀(seed : *). seed → (seed → el) → (seed → seed) → res) � The trouble comes when they can be freely mixed. Stefan

Stefan O'Rear

10:46 p.m.

On Tue, May 15, 2007 at 07:44:25PM -0700, Stefan O'Rear wrote:

...

λ(el : *). ∀(res : *). (∀(seed : *). seed → (seed → el) → (seed → seed) → res)

that little decoding error at the end should have been -> res. I need a better unicode editing solution :) Stefan

Josef Svenningsson

13 May 13 May

2:24 p.m.

I think both Benja's and David's answers are terrific. Let me just add a reference. The person who's given these issues most thought is probably Per Martin-Löf. If you want to know more about the meaning of local connectives you should read his "On the Meanings of the Logical Constants and the Justifications of the Logical Laws" [1]. It consists of three lectures which I think are quite readable although I can recommend skipping the first lecture, at least on a first read-through since it's pretty heavy going. In the beginning of the third lecture you will find the classic quote: "the meaning of a proposition is determined by what it is to verify it, or what counts as a verification of it" This is essentially what both Benja and David said. hth, Josef [1] http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.html On 5/11/07, Benja Fallenstein wrote:

...

Adding some thoughts to what David said (although I don't understand the issues deeply enough to be sure that these ideas don't lead to ugly things like paradoxes)--

2007/5/10, Gaal Yahas :

...
Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead:

data Stream a = SHead a (Stream a) sMap :: (a -> b) -> Stream a -> Stream b

What is the object "Stream a" in logic?

It's not that much more interesting than "list." The 'data' declaration can be read as,

"To prove the proposition (Stream a), you must prove the proposition 'a' and the proposition 'Stream a.'"

In ordinary logic this would mean that you couldn't prove (Stream a), of course, but that just corresponds to strict languages in which you couldn't construct an object of type Stream a (because it would have to be infinite). To make sense of this, we need to assume a logic in which we can have similar 'infinite proofs.' (This is the part where I'm not sure it's really possible to do. I haven't read the Pierce chapter David refers to.)

With that reading, (Stream a) is basically the same proposition as (a) -- as evidenced by

f x = SHead x (f x) -- f :: a -> Stream a g (SHead x) = x -- g :: Stream a -> a

We can find more interesting propositions, though. Here's an example (perhaps not useful, but I find it interesting :-)):

data Foo a b = A a | Fn (Foo a b -> b)

We can prove this proposition if we can prove one of these propositions:

a a -> b (a -> b) -> b ((a -> b) -> b) -> b ...

Each of these is weaker than the previous one; if x is a proof of proposition n, then (\f -> f x) is a proof of proposition n+1. The fourth one is a tautology in classical logic, but not in intuitionistic logic.

- Benja _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Gaal Yahas

4:26 p.m.

On 5/13/07, Josef Svenningsson wrote:

...

I think both Benja's and David's answers are terrific. Let me just add a reference.

Yes, this entire thread has been quite illuminating. Thanks all!

...

The person who's given these issues most thought is probably Per Martin-Löf. [...] In the beginning of the third lecture you will find the classic quote: "the meaning of a proposition is determined by what it is to verify it, or what counts as a verification of it"

I like how this is reminiscent of Quine's ideas in "On What There Is". Another reference to add is Simon Thompson, _Type Theory and Functional Programming_, which I stumbled upon online here: http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ . -- Gaal Yahas http://gaal.livejournal.com/

apfelmus

12 May 12 May

6:20 a.m.

Gaal Yahas wrote:

...

What do higher-order types like lists mean when viewed through the Curry-Howard correspondence? I've been wondering about this for a while. The tutorials ask me to consider [...] But what does the following mean?

map :: (a -> b) -> [a] -> [b]

Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead:

data Stream a = SHead a (Stream a) sMap :: (a -> b) -> Stream a -> Stream b

What is the object "Stream a" in logic? What inference rules may be applied to it? How is "data Stream" introduced, and what about variant constructors?

There are many Curry-Howards correspondences depending on the logic you start with. With intuitionistic propositional logic, you have types like (a,b) -- logical conjunction Either a b -- logical disjunction with the silent agreement that a and b are variables denoting propositions. Types like () or Int do not have a logical counterpart in propositional logic, although they can be viewed as a constant denoting truth. In other words, they may be thought of as being short-hand for the type expression (a,a) (where a is a fresh variable). System F is closest to Haskell and corresponds to a second order intuitionistic propositional logic (?). Here, many recursive data types can be formulated in the logic. For instance, the proposition ∀X.(a -> X -> X) -> X -> X can be used as the list type [a]. The type 'Stream a' would correspond to ∀X.(a -> X -> X) -> X but this proposition is wrong because it can be used to prove everything: assume a term/proof 'f :: ∀X.(a -> X -> X) -> X', then f (uncurry snd) :: ∀X.X is a proof for everything. (For simplicity, we omitted the application of type variables). In the end, there more computationally interesting than logically interesting propositions. The type system corresponding to intuitionistic predicate calculus is already far more powerful than Haskell's type system and also known as "dependent types". In my eyes, this is the ultimate style of programming and and at some point, languages like Epigram or Omega will take over the Haskell mailing list ;) But there is still lots of research to do for that. Regards, apfelmus

Stefan Holdermans

13 May 13 May

2:53 a.m.

Apfelmus,

...

Types like () or Int do not have a logical counterpart in propositional logic, although they can be viewed as a constant denoting truth. In other words, they may be thought of as being short-hand for the type expression (a,a) (where a is a fresh variable).

Could you explain this? I can see () corresponding to True; but you're not suggesting that True <=> (a, a), are you?

...

System F is closest to Haskell and corresponds to a second order intuitionistic propositional logic (?).

Not propositional of course, but second-order indeed. Cheers, Stefan

Stefan Holdermans

2:58 a.m.

Apfelmus,

...

...
System F is closest to Haskell and corresponds to a second order intuitionistic propositional logic (?).

Not propositional of course, but second-order indeed.

Not sure, what I meant there :-S. Please ignore it. You're right of course: second-order intuitionistic propositional logic it is :-). (Sorry for adding confusion.) Cheers, Stefan

apfelmus

4:45 a.m.

Stefan Holdermans wrote:

...

Apfelmus,

...
Types like () or Int do not have a logical counterpart in propositional logic, although they can be viewed as a constant denoting truth. In other words, they may be thought of as being short-hand for the type expression (a,a) (where a is a fresh variable).

Could you explain this? I can see () corresponding to True; but you're not suggesting that True <=> (a, a), are you?

Oh, what a mistake .. >< . Of course, a /\ a = a /= True. But there are real tautologies like (a -> a) that can be used instead. I just wanted to avoid introducing a primitive constant ⊤ denoting truth when it already can be expressed in the logic. From now on, let's say ⊤ := (a->a). What I wanted to say is that the Curry-Howards correspondence of first order propositional logic does not assign a meaning to types like () or Int that are not built from type variables and the logical connectives. But I think it can be adapted to assign them the proposition ⊤. The translation of lambda-terms to proofs would then replace every primitive constant like 1 or 2 or () with the proof (id :: ⊤) and eradicate pattern matches and conditionals. From a computational point of view, this correspondence is not very interesting then. Regards, apfelmus

6584

Age (days ago)

6590

Last active (days ago)

List overview

Download

14 comments

9 participants

participants (9)

apfelmus
Benja Fallenstein
DavidA
Derek Elkins
Gaal Yahas
Josef Svenningsson
Scott Turner
Stefan Holdermans
Stefan O'Rear