Le Wed, 4 Jan 2012 16:22:31 +0100, Yves Parès <limestr...@gmail.com> a écrit :
> 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)). _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe