[Haskell-cafe] Tutorial: Curry-Howard Correspondence
Dan Weston
westondan at imageworks.com
Thu Oct 18 17:46:03 EDT 2007
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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
More information about the Haskell-Cafe
mailing list