6.4.6. Existentially quantified data constructors — Glasgow Haskell Compiler 9.12.1 User's Guide (original) (raw)

ExistentialQuantification

Implies:

ExplicitForAll

Since:

6.8.1

Status:

Included in GHC2024, GHC2021

Allow existentially quantified type variables in types.

The idea of using existential quantification in data type declarations was suggested by Perry, and implemented in Hope+ (Nigel Perry, The Implementation of Practical Functional Programming Languages, PhD Thesis, University of London, 1991). It was later formalised by Laufer and Odersky (Polymorphic type inference and abstract data types, TOPLAS, 16(5), pp. 1411-1430, 1994). It’s been in Lennart Augustsson’shbc Haskell compiler for several years, and proved very useful. Here’s the idea. Consider the declaration:

data Foo = forall a. MkFoo a (a -> Bool) | Nil

The data type Foo has two constructors with types:

MkFoo :: forall a. a -> (a -> Bool) -> Foo Nil :: Foo

Notice that the type variable a in the type of MkFoo does not appear in the data type itself, which is plain Foo. For example, the following expression is fine:

[MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]

Here, (MkFoo 3 even) packages an integer with a function eventhat maps an integer to Bool; and MkFoo 'c' isUpper packages a character with a compatible function. These two things are each of type Foo and can be put in a list.

What can we do with a value of type Foo? In particular, what happens when we pattern-match on MkFoo?

Since all we know about val and fn is that they are compatible, the only (useful) thing we can do with them is to apply fn toval to get a boolean. For example:

f :: Foo -> Bool f (MkFoo val fn) = fn val

What this allows us to do is to package heterogeneous values together with a bunch of functions that manipulate them, and then treat that collection of packages in a uniform manner. You can express quite a bit of object-oriented-like programming this way.

6.4.6.1. Why existential?

What has this to do with existential quantification? Simply thatMkFoo has the (nearly) isomorphic type

MkFoo :: (exists a . (a, a -> Bool)) -> Foo

But Haskell programmers can safely think of the ordinary _universally_quantified type given above, thereby avoiding adding a new existential quantification construct.

6.4.6.2. Existentials and type classes

An easy extension is to allow arbitrary contexts before the constructor. For example:

data Baz = forall a. Eq a => Baz1 a a | forall b. Show b => Baz2 b (b -> b)

The two constructors have the types you’d expect:

Baz1 :: forall a. Eq a => a -> a -> Baz Baz2 :: forall b. Show b => b -> (b -> b) -> Baz

But when pattern matching on Baz1 the matched values can be compared for equality, and when pattern matching on Baz2 the first matched value can be converted to a string (as well as applying the function to it). So this program is legal:

f :: Baz -> String f (Baz1 p q) | p == q = "Yes" | otherwise = "No" f (Baz2 v fn) = show (fn v)

Operationally, in a dictionary-passing implementation, the constructorsBaz1 and Baz2 must store the dictionaries for Eq andShow respectively, and extract it on pattern matching.

6.4.6.3. Record Constructors

GHC allows existentials to be used with records syntax as well. For example:

data Counter a = forall self. NewCounter { _this :: self , _inc :: self -> self , _display :: self -> IO () , tag :: a }

Here tag is a public field, with a well-typed selector functiontag :: Counter a -> a. See Field selectors and TypeApplicationsfor a full description of how the types of top-level field selectors are determined.

The self type is hidden from the outside; any attempt to apply _this, _inc or _display as functions will raise a compile-time error. In other words, GHC defines a record selector function only for fields whose type does not mention the existentially-quantified variables. (This example used an underscore in the fields for which record selectors will not be defined, but that is only programming style; GHC ignores them.)

To make use of these hidden fields, we need to create some helper functions:

inc :: Counter a -> Counter a inc (NewCounter x i d t) = NewCounter { _this = i x, _inc = i, _display = d, tag = t }

display :: Counter a -> IO () display NewCounter{ _this = x, _display = d } = d x

Now we can define counters with different underlying implementations:

counterA :: Counter String counterA = NewCounter { _this = 0, _inc = (1+), _display = print, tag = "A" }

counterB :: Counter String counterB = NewCounter { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }

main = do display (inc counterA) -- prints "1" display (inc (inc counterB)) -- prints "##"

Record update syntax is supported for existentials (and GADTs):

setTag :: Counter a -> a -> Counter a setTag obj t = obj{ tag = t }

The rule for record update is this:

the types of the updated fields may mention only the universally-quantified type variables of the data constructor. For GADTs, the field may mention only types that appear as a simple type-variable argument in the constructor’s result type.

For example:

data T a b where { T1 { f1::a, f2::b, f3::(b,c) } :: T a b } -- c is existential upd1 t x = t { f1=x } -- OK: upd1 :: T a b -> a' -> T a' b upd2 t x = t { f3=x } -- BAD (f3's type mentions c, which is -- existentially quantified)

data G a b where { G1 { g1::a, g2::c } :: G a [c] } upd3 g x = g { g1=x } -- OK: upd3 :: G a b -> c -> G c b upd4 g x = g { g2=x } -- BAD (g2's type mentions c, which is not a simple -- type-variable argument in G1's result type)

6.4.6.4. Restrictions

There are several restrictions on the ways in which existentially-quantified constructors can be used.