[Haskell-cafe] Tutorial: Curry-Howard Correspondence
Jonathan Cast
jonathanccast at fastmail.fm
Thu Oct 18 18:41:38 EDT 2007
On Fri, 2007-10-19 at 00:02 +0200, jerzy.karczmarczuk at 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
More information about the Haskell-Cafe
mailing list