[Haskell-cafe] Tutorial: Curry-Howard Correspondence
jerzy.karczmarczuk at info.unicaen.fr
jerzy.karczmarczuk at info.unicaen.fr
Thu Oct 18 17:09:09 EDT 2007
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
More information about the Haskell-Cafe
mailing list