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

[AUGER Cédric]

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

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