Re: [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'

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



Regards,
Roberto Zunino.

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) Clearly, the first one (where t is fixed) is stronger than the second, (where t might depend on a).

signature.asc
Description: OpenPGP digital signature

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe