[Haskell-cafe] Solved but strange error in type inference
AUGER Cédric
sedrikov at gmail.com
Fri Jan 6 16:32:51 CET 2012
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
More information about the Haskell-Cafe
mailing list