|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
# 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/type-extensions.html#existential-quantification)
|
|
|
|
- distinguish from [PolymorphicComponents](polymorphic-components)
|
|
|
|
|
|
|
|
## 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](polymorphic-components).
|
|
|
|
</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](gad-ts) syntax</th>
|
|
|
|
<td>
|
|
|
|
|
|
|
|
```wiki
|
|
|
|
data Accum :: * -> * where
|
|
|
|
MkAccum :: s -> (a -> s -> s) -> (s -> a) -> Accum a
|
|
|
|
```
|
|
|
|
|
|
|
|
Existentials are subsumed by [GADTs](gad-ts).
|
|
|
|
</td></tr></table>
|
|
|
|
|
|
|
|
|
|
|
|
<table><tr><th>use [ExistentialQuantifier](existential-quantifier)</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/haskell-cafe/2005-June/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.
|
|
|
|
|
|
|
|
|