[Haskell-cafe] Non-existant existential?
bruno.oliveira at comlab.ox.ac.uk
Thu Sep 21 12:50:11 EDT 2006
>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
>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
Look at section 188.8.131.52.1 of:
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.
More information about the Haskell-Cafe