Just for fun

Anton Moscal writes:

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:

[...]

main = print (map eval [mk_app (\x->x) 239, mk_app Char.ord '1'])

import Char(ord) main = print (tail [error "I'm too lazy to be explicitly existential.", (\x->x) 239, ord '1']) {- Regards, Tom :-}