18 Oct
2007
18 Oct
'07
9:09 p.m.
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