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

[AUGER Cédric]

Le Fri, 6 Jan 2012 10:59:29 +0100,
Yves Parès <limestrael at gmail.com> a écrit :

> 2012/1/6 AUGER Cédric <sedrikov at gmail.com>
> 
> > when you write "forall a. exists b. a -> b -> a", then you allow the
> > caller to have access to b to produce a (didn't you write
> > "a->b->a"?)
> >
> 
> Yes, sorry, I always assumed independence between the type variables.
> Like in:
> f :: forall a. a -> (forall b. b -> a)
> being the same than:
> f :: forall a b. a -> b -> a
> I should have specified: "*if* a doesn't depend on b in the latter."
> Of course the latter allows that, whereas the first does not (since
> its what prevents STRefs from escaping runST, by forbidding the
> return type of runST to depend on the phantom type 's' of the ST
> action).

You misunderstood me.

> f :: forall a. a -> (forall b. b -> a)

is equal to:
> f :: forall a. a -> forall b. b -> a
(parenthesis are uneeded here)

which is equivalent to:
> f :: forall a b. a -> b -> a

(assuming what you said of course, but with only type variables it is
the case)

Although GHC may complain if it gets one type instead of the other;
(but in that case, just replacing "f" with "(\x y -> f x y)" should do
the trick as this is an eta expansion which accepts both signatures).

It is not the case with existential variables:
in mathematics, you cannot change order of different quantifications;
it is the same in type theory:

"∀ a. ∃ b. p a b" is not the same as "∃ b. ∀ a. p a b"

Think of "∀ a. ∃ b. b = a+1" and "∃ b. ∀ a. b = a+1"

(but of course you can swap 2 existential quantifications as well as
you can swap 2 universal quantifications)

To understand how to eliminate "exist p. t[p]", to have only forall
expressions, you must consider elimination principle of the "∃" rule;
but it will change the type.

It is the same thing for datatypes:

data Bool = True
          | False

can be eliminated in the types:

Bool "=" forall a. a -> a -> a
True "=" \x y -> x
False "=" \x y -> y

So now a function like:

f :: Bool -> SomeType
f b = if b then someTerm1 else someTerm2

can be rewritten as:

f2 :: (forall a. a -> a -> a) -> SomeType
f2 b = b someTerm1 someTerm2

(note that "a" is existentially quantified in the type of "f2")

For the existential types, it is the same thing; the easiest way to
understand them is as inductive types, so that the type is "stored"
somewhere. But elimination of an inductive type completely changes the
signature!

exists b. t[b] as a syntactic sugar of:
Exists (t::*->*) is isomorphic to:
forall a. (forall b. (t[b]) -> a) -> a