Version 5 (modified by ross@…, 10 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

Existential quantification hides a type variable within a data constructor.
The current syntax uses a `forall` before the data constructor, as in the following example , which packs a value together with operations on that value:

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

When a value of this type is constructed, `s` will be instantiated to some concrete type. When such a value is analysed, `s` is abstract.

The `forall` hints at the polymorphic type of the data constructor:

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

but see below for alternatives.

## References

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

## Syntax of existentials

Several possibilities have been proposed:

implicit quantification::

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

As the type variable

sdoes not appear on the left hand side, it is considered to be existentially quantified. The main counterargument is that one can easily introduce an existential type by forgetting an argument to the data type. Error messages might confuse the novice programmer.

`forall` before the constructor::

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

This is the currently implemented syntax, motivated by the type of the data constructor, but it can be confused with PolymorphicComponents.

`exists` before the constructor::

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

which reinforces the connection to existential types. When analysing such a value, you know only that there exists some type

ssuch that the arguments have these types.

Reserves an extra word.

GADT syntax::

data Accum :: * -> * where MkAccum :: s -> (a -> s -> s) -> (s -> a) -> Accum a

Existentials are subsumed by GADTs.

## 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.