Le Wed, 4 Jan 2012 16:22:31 +0100,
Yves Parès
Oleg explained why those work in his last post. It's the exact same logic for each one.
f :: a -> a f x = x :: a
We explained that too: it's converted (alpha-converted, but I don't exactly know what 'alpha' refers to. I guess it's phase the type inferer goes through) to:
f :: forall a. a -> a f x = x :: forall a1. a1
On one side, x has type a, on the other, it has type a1. Those are different polymorphic types, yet it's the same variable x hence the incompatibility. So it doesn't type-check.
Have you ever asked what βreduction refers to? I guess that αconversion and βreduction are the two properties on the λcalculus. (γcorrection is not a λcalculus property, is just some settings for your screens.) αcorrection: λa.t = λb.t[all free occurences of a are replaced by b] if b doesn't appear in t βreduction: (λa.t)b = t[all free occurences of a are replaced by b] even if b appear in t There are also some greekletterproperty names which are common in functionnal languages: ηexpansion/contraction: λa.(f a) = f and I know that in Coq we have δ to unfold the definitions, ι for case reduction (case True of {True -> a ; False -> b} = a) and ζ for unrolling one time a fixpoint ((fix f n := match n with O => a | S n => b (f n) end) = (fun n => match n with O => a | S n => b ((fix f ... end) n) end)).