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
