Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
On 2007 May 13 Sunday 14:52, Benja Fallenstein wrote:
2007/5/12, Derek Elkins [EMAIL PROTECTED]:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
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 [EMAIL PROTECTED]: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED]: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
2007/5/12, Derek Elkins [EMAIL PROTECTED]:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
2007/5/13, Benja Fallenstein [EMAIL PROTECTED]: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
On 5/13/07, Josef Svenningsson [EMAIL PROTECTED] 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 [EMAIL PROTECTED] http://gaal.livejournal.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
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 [EMAIL PROTECTED]: 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
Re: [Haskell-cafe] 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 [EMAIL PROTECTED]: 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Higher order types via the Curry-Howard correspondence
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 [EMAIL PROTECTED] http://gaal.livejournal.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
