[Haskell-cafe] Non-existant existential?

[Bruno Oliveira]

Hello,

>Consider the following:

>data SimpExist a = SimpExist (forall x . x -> a)
>f :: SimpExist Bool
>f = SimpExist (const True)
>g = SimpExist id

>What is the type of g? In a similar example, GHC tells me it is of
>type SimpExist c. Yet, I can't unify it with any other SimpExist c'.

Have you tried to type check this example (the "g")?

It does not type check in my GHC. There are not many functions with 
the type "forall x . x -> a" when "a" is also polymorphic --- it is the type of 
 unsafeCoerce.

>It seems to me that this is something like exists x . SimpExist x, and
>is similar to:

>data ExistWrap = forall a . ExistWrap (forall x . x -> a)

Sure, you should read a "forall" on the left side of a constructor as 
"exists". 

Look at section 7.4.1.4.1 of:

http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html

The design decision here was to avoid introducing a new "exist" construct. I believe 
that the justification for this option is that in Logic a "forall" in a contravariant position 
has the same effect as an existential.

Cheers,

Bruno