[Haskell-cafe] Solved but strange error in type inference

AUGER Cédric sedrikov at gmail.com
Wed Jan 4 18:22:57 CET 2012

Le Wed, 4 Jan 2012 16:22:31 +0100,
Yves Parès <limestrael at 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.)


λa.t = λb.t[all free occurences of a are replaced by b]
 if b doesn't appear in t


(λ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:

λ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)).

More information about the Haskell-Cafe mailing list