Rigid type-var unification failure in existentials used with parametrically polymorphic functions
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.
Stupid of me:
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.
The proof outlined is that of (forall a. a -> a) -> Box -> Box, my apologies. We have to prove a universally quantified formula and that requires forall-introduction. If someone has the proof in the tip of their fingers, I'm grateful if you could let me know.
On Nov 30, 2007 12:20 PM, Pablo Nogueira
A question about existential quantification:
Given the existential type:
data Box = forall a. B a
[...]
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)
However, at first sight |f| is polymorphic so it could be applied to any value, included the value hidden in |Box|.
f is not polymorphic here; mapBox is.
Of course, this works:
mapBox :: (forall a b. a -> b) -> Box -> Box mapBox f (B x) = B (f x)
Here f is polymorphic.
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.
Yes, but that is only because your Box type is trivial. It can contain any value, so you can never extract any information from it. Let's detrivialize your box and see where that leads us: data Box = forall a. (Num a) => B a Then: mapBox :: (forall a b. (Num a) => a -> a) -> Box -> Box Should work fine, and there are functions which you can give to mapBox which are not bottom. Luke
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)
However, at first sight |f| is polymorphic so it could be applied to any value, included the value hidden in |Box|.
f is not polymorphic here; mapBox is.
I see, it's a case of not paying proper attention. I presume this will reflect in the imposibility of introducing the forall when trying to "prove" the type.
Yes, but that is only because your Box type is trivial. It can contain any value, so you can never extract any information from it.
Indeed, I was just trying to play with unconstrained existentials.
It seems you've already figured this out, but here's a quick counterexample:
{-# LANGUAGE ExistentialQuantification, RankNTypes #-} module Box where data Box = forall a. B a
--mapBox :: forall a b. (a -> b) -> Box -> Box -- incorrect type mapBox f (B x) = B (f x)
then:
boxedInt :: Box boxedInt = B (1 :: Int)
f :: [Int] -> Int f = sum
mf :: Box -> Box mapBox f -- this is well-typed according to the specified type of "mapBox" But, mf boxedInt :: Box mf boxedInt = mapBox f boxedInt = mapBox sum (B (1 :: Int)) = B (sum (1 :: Int)) which is not well-typed. The least specific type for MapBox is
mapBox :: forall b. (forall a. (a -> b)) -> Box -> Box
There are non-bottom functions of this type, for example: const (1 :: Int) :: forall a. a -> Int With this type,
ok :: Box ok = mapBox (const 1) (B "hello")
is well-typed.
-- ryan
On 11/30/07, Pablo Nogueira
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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Luke Palmer -
Pablo Nogueira -
Ryan Ingram