Le Fri, 6 Jan 2012 10:59:29 +0100, Yves Parès a écrit :

2012/1/6 AUGER Cédric

...

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