










# Existential Quantification









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









```wiki



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



```









Constraints are also allowed.












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:









```wiki



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



```









but see below for alternatives.












When pattern matching, the type variable `s` is instantiated to a *Skolem variable*, which cannot be unified with any other type and cannot escape the scope of the match.









## References









 [ Polymorphic Type Inference and Abstract Data Types](http://www.cs.luc.edu/users/laufer/papers/toplas94.pdf) by K. Läufer and M. Odersky, in TOPLAS, Sep 1994.



 [ GHC documentation](http://www.haskell.org/ghc/docs/latest/html/users_guide/typeextensions.html#existentialquantification)



 distinguish from [PolymorphicComponents](polymorphiccomponents)






## Tickets












<table><tr><th>[\#26](https://gitlab.haskell.org//haskell/prime/issues/26)</th>



<td>add ExistentialQuantification</td></tr></table>












## Syntax of existentials












Several possibilities have been proposed:









<table><tr><th>implicit quantification</th>



<td>






```wiki



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



```






As the type variable `s` does 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.



</td></tr></table>









<table><tr><th>`forall` before the constructor</th>



<td>






```wiki



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](polymorphiccomponents).



</td></tr></table>









<table><tr><th>`exists` before the constructor</th>



<td>






```wiki



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 `s` such that the arguments have these types.



This syntax is used by [ Tim Sheard](http://www.cs.pdx.edu/~sheard/)'s Omega language, which is based on Haskell.



</td></tr></table>









>



>



> Reserves an extra word.



>



>






<table><tr><th>[GADT](gadts) syntax</th>



<td>






```wiki



data Accum :: * > * where



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



```






Existentials are subsumed by [GADTs](gadts).



</td></tr></table>









<table><tr><th>use [ExistentialQuantifier](existentialquantifier)</th>



<td>



</td></tr></table>









>



>



> if exists quantifiers are allowed in any type, existential data types are



>



>









simply a special case of this.









```wiki



data Foo = Foo (exists a . a > a)



```






>



>



> and they may be declared via type synonym as well



>



>






```wiki



type Any = exists a . Num a => a



data Foo = Foo Any



```






>



>



> if you with the quantifier to scope over multiple components of a data type,



>



>









you pull it in front of the constructor:









```wiki



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



```






>



>



> Note that this is the same syntax one would use when using existential



>



>









quantifiers in type signatures with the exists coming before the constructor:









```wiki



foo :: Int > (exists a . Either (a > Char) a) > Char



foo = ...



```






>



>



> This is the syntax supported by jhc.



>



>






## Variations









 Hugs allows existential quantification for newtype declarations, as long as there are no class constraints.






```wiki



newtype T = forall a. C a



```






GHC and Nhc98 do not and jhc can not.






 Hugs and Nhc98 allow matching on an existentially quantified constructor in a pattern binding declaration, except at the top level.






```wiki



data T = forall a. C (a > Int) a



foo t = let C f x = t in f x



```






GHC does not allow such matching.



More generally, GHC does not allow matching of existentially quantified constructors inside irrefutable patterns (of which `let` pattern bindings are a special case).



It is said that the translation to GHC's intermediate language is problematic.






 None of the implementations can derive instances for existentially quantified types, but this could be relaxed, e.g






```wiki



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.






```wiki



data T = forall a. C { f1 :: a, f2 :: Int }



```






## Pros









 offered by GHC, Hugs and Nhc98 for years, HBC even longer.



 typing rules well understood.



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






## Cons









 tricky to implement on implementations without a common runtime representation of values such as jhc. (however, John Meacham believes any trickiness is worth it due to the value of this extension, at least for jhc)






# Extension: better syntactic support












Discussion on the list in late January focussed on a [ proposal from Johannes Waldmann](http://www.haskell.org//pipermail/haskellcafe/2005June/010516.html) to add syntactic support for the use of existential types.









## Background example












The status quo is illustrated by the concrete example of geometrical figures, each of which is an instance of an interface given by the Haskell class









```wiki



class Figure f ...



```









with instances `Circle r` and `Rectangle h w`, say. The existential built on the `Figure` class is given by









```wiki



data EFigure = exists f . Figure f => EFigure f



```









Elements of this type have the form `EFigure (Circle r)` and so the values of the existential type are explicitly 'boxed' by the `EFigure` constructor when they are built and need to be unboxed when they are used. Unboxing can be achieved by an additional instance declaration:









```wiki



instance Figure EFigure ...



```









but boxing needs to be explicit.









## First proposal












The extension proposed here is to hide the existence of the data type and constructor `EFigure`, just referring to `Figure` instead. The issue becomes one of conversion between the figure types `Circle` and `Rectangle` and the type `Figure`. A concrete example is given by









```wiki



f :: Integer > Circle



g :: Figure > Blah



```









in order for the expression `g . f` to be well typed, a conversion needs to be inserted thus: `g . EFigure . f`. Conversions become more complicated in case that









```wiki



f :: Integer > [Circle]



g :: [Figure] > Blah



```









for instance.









## an existential for each single parameter class












A proposal based on the discussion is automatically to introduce an existential type for each single parameter type class. The type and class would have the same name, as in









```wiki



class Figure f ...



data Figure = exists f . Figure f => Figure f



instance Figure Figure ...



```









Discussion focussed on whether there should or should not be automatic conversion from figure types into `Figure`; it was agreed that the `Figure` constructor could be used to do this, with the `Figure` instance providing the unboxing required.












This is a signifigantly more difficult problem than this proposal makes it seem.






