[Redirect] polymorphism and existential types
Redirected to haskell-cafe@haskell.org, the right list. -- Don ----- Forwarded message from Louis-Julien Guillemette <guillelj@iro.umontreal.ca> ----- Date: Mon, 27 Nov 2006 16:15:26 -0500 (EST) From: Louis-Julien Guillemette Subject: [Haskell] polymorphism and existential types 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' {- Test.hs:18:17: Inferred type is less polymorphic than expected Quantified type variable `a' is mentioned in the environment: e' :: ExpT a t (bound at Test.hs:18:11) In the first argument of `f', namely `e'' In the expression: f e' In a case alternative: Exp e' -> f e' Failed, modules loaded: none. -} In particular, the solution of pushing the forall inside doesn't work for me (it breaks other parts of my code...) : data Exp' = forall t . Exp' (forall a . ExpT a t) g' :: (forall a . ExpT a t) -> () g' e = let e1 :: Exp' e1 = Exp' e in case e1 of Exp' e' -> f e' Any help welcome! Louis-Julien _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
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.
participants (2)
-
dons@cse.unsw.edu.au -
Roberto Zunino