On Fri, 2007-10-19 at 00:02 +0200, [EMAIL PROTECTED] 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
