[Haskell-cafe] [Redirect] polymorphism and existential types

[Roberto Zunino]

Donald Bruce Stewart wrote:
> Supposing a polymorphic value (of type, say, forall a . ExpT a t) is
> stored inside an existential package (of type, say, forall a . Exp a),
> I wonder how to recover a polymorphic value when eliminating the
> existential.  The ``natural way'' to write this doesn't work:
> 
> {-# OPTIONS -fglasgow-exts #-}
> 
> data ExpT a t
> data Exp a = forall t . Exp (ExpT a t)
> 
> f :: (forall a . ExpT a t) -> ()
> f e = ()
> 
> g :: (forall a . ExpT a t) -> ()
> g e =
>   let e1 :: forall a . Exp a
>       e1 = Exp e
>   in case e1 of
>        Exp e' -> f e'

IIUC, this is not possible. I believe that the type given for e1 is 
strictly weaker than the type of e, so that recovering the type of e 
from that of e1 can not be done. This is because (up-to iso)

e :: exists t . forall a . ExpT a t
e1:: forall a . exists t . ExpT a t

Clearly, the first one (where t is fixed) is stronger than the second, 
(where t might depend on a).

Regards,
Roberto Zunino.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 249 bytes
Desc: OpenPGP digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20061130/355995fe/signature.bin