30 Nov
2007
30 Nov
'07
7:38 a.m.
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.