On Nov 30, 2007 12:20 PM, Pablo Nogueira <[EMAIL PROTECTED]> wrote: > 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
