[Haskell-cafe] Rigid type-var unification failure in existentials
used with parametrically polymorphic functions
Luke Palmer
lrpalmer at gmail.com
Fri Nov 30 07:32:05 EST 2007
On Nov 30, 2007 12:20 PM, Pablo Nogueira <pirelo at googlemail.com> 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
More information about the Haskell-Cafe
mailing list