Le Fri, 6 Jan 2012 10:59:29 +0100, Yves Parès <limestr...@gmail.com> a écrit :
> 2012/1/6 AUGER Cédric <sedri...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe