wiki:ExistentialQuantification

Version 4 (modified by loeh@…, 8 years ago) (diff)

added crossref

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

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.

Cons