Version 4 (modified by loeh@…, 11 years ago) (diff) |
---|

# Existential Quantification

See ExtensionDescriptionHowto for information on how to write these extension descriptions. Please add any new extensions to the list of HaskellExtensions.

## Brief Explanation

Local existential quantification of type variables in a data constructor,
introduced with `forall` before the data constructor, e.g.

data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a)

The `forall` is justified by the type of the data constructor:

MkAccum :: s -> (a -> s -> s) -> (s -> a) -> Accum a

but some have suggested using `exists` instead to avoid confusion with PolymorphicComponents.

## References

- Polymorphic Type Inference and Abstract Data Types by K. Läufer and M. Odersky, in TOPLAS, Sep 1994.
- GHC documentation
- ExistentialsVsPolymorphicComponents?

## Variations

- Hugs allows existential quantification for newtype declarations, as long as there are no class constraints.
newtype T = forall a. C a

GHC and Nhc98 do not.

- Hugs and Nhc98 allow matching on an existentially quantified constructor in a pattern binding declaration, except at the top level.
data T = forall a. C (a -> Int) a foo t = let C f x = t in f x

GHC does not allow such matching.

- None of the implementations can derive instances for existentially quantified types, but this could be relaxed, e.g
data T = forall a. Show a => C [a] deriving Show

- GHC 6.5 allows fields with existentially quantified types, though selectors may only be used if their type does not include the quantified variable.
data T = forall a. C { f1 :: a, f2 :: Int }

## Pros

- quite handy for representations that delay composition or application, e.g. objects, various parser combinator libraries from Utrecht.