[Haskell-cafe] Rigid type-var unification failure in existentials
used with parametrically polymorphic functions
Pablo Nogueira
pirelo at googlemail.com
Fri Nov 30 07:20:16 EST 2007
A question about existential quantification:
Given the existential type:
data Box = forall a. B a
in other words:
-- data Box = B (exists a.a)
-- B :: (exists a.a) -> Box
I cannot type-check the function:
mapBox :: forall a b. (a -> b) -> Box -> Box
-- :: forall a b. (a -> b) -> (exists a.a) -> (exists a.a)
mapBox f (B x) = B (f x)
Nor can I type check:
mapBox :: forall a. (a -> a) -> Box -> Box
-- :: forall a. (a -> a) -> (exists a.a) -> (exists a.a)
mapBox f (B x) = B (f x)
The compiler tells me that in both functions, when it encounters the
expression |B (f x)|, it cannot unify the universally quantified |a|
(which generates a rigid type var) with the existentially quatified
|a| (which generates a different rigid type var) -- or so I interpret
the error message.
However, at first sight |f| is polymorphic so it could be applied to
any value, included the value hidden in |Box|.
Of course, this works:
mapBox :: (forall a b. a -> b) -> Box -> Box
mapBox f (B x) = B (f x)
Because it's a tautology: given a proof of a -> b for any a or b I can
prove Box -> Box. However the only value of type forall a b. a -> b is
bottom.
This also type-checks:
mapBox :: (forall a. a -> a) -> Box -> Box
mapBox f (B x) = B (f x)
When trying to give an explanation about why one works and the other
doesn't, I see that, logically, we have:
forall a. P(a) => Q implies (forall a. P(a)) => Q when a does not
occur in Q.
The proof in our scenario is trivial:
p :: (forall a. (a -> a) -> (Box -> Box)) -> (forall a. a -> a) -> Box -> Box
p mapBox f b = mapBox f b
However, the converse is not true.
Yet, could somebody tell me the logical reason for the type-checking
error? In other words, how does the unification failure translate
logically. Should the first mapBox actually type-check?
Isn't the code for mapBox :: forall a. (a -> a) -> Box -> Box
encoding the proof:
Assume forall a. a -> a
Assume exists a.a
unpack the existential, x :: a = T for some T
apply f to x, we get (f x) :: a
pack into existential, B (f x) :: exists a.a
Discharge first assumption
Discharge second assumption
The error must be in step 3. Sorry if this is obvious, it's not to me right now.
More information about the Haskell-Cafe
mailing list