Version 3 (modified by john@…, 10 years ago) (diff)

Existential Quantifier

this means supporting the 'exists' quantifier as creating existential types much the same way 'forall' can be used in ghc. An example would be

type Any = exists a . Typeable a => a

sameType :: Any -> Any -> Bool
sameType x y = typeOf x == typeOf y

When existentials appear in the contravarient position such as above, they can be desugared into rank-n types with foralls. if existentials are allowed in the covarient position, then support for FirstClassExistentials? is needed.


Jhc currently supports the existential syntax anywhere a type is accepted, but will report an error if one is used in a covariant position with the exception of when it is a component of a data type.