Hello! This is well-known definition of the existential quantification through universal: (E x.P(x)) <=> A y.(A x.P (x) => y) => y I try to translate in to Haskell. The following program can be compiled by "ghc -fglasgow-exts ..." and works correctly: ---------------------------------------- import Char type E a = forall t . (forall x . a x -> t) -> t newtype Pair a b = MkPair (b, (b -> a)) newtype App a = MkApp (E (Pair a)) mk_app :: (a -> b) -> a -> App b mk_app f v = MkApp (\g -> g (MkPair (v, f))) app_s = mk_app Char.ord '1' app_id = mk_app (\x->x) 239 eval :: App a -> a eval (MkApp g) = g (\(MkPair (x, f)) -> f x) main = print (map eval [mk_app (\x->x) 239, mk_app Char.ord '1']) --------------------------------------- Regards, Anton Moscal