Just for fun

[Anton Moscal]

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