[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.)
α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)).
More information about the Haskell-Cafe
mailing list