Data.Exists

data Exists :: (Type -> Type) -> Type

This type constructor can be used to existentially quantify over a type of kind Type.

Specifically, the type Exists f is isomorphic to the existential type exists a. f a.

Existential types can be encoded using universal types (forall) for endofunctors in more general categories. The benefit of this library is that, by using the FFI, we can create an efficient representation of the existential by simply hiding type information.

For example, consider the type exists s. Tuple s (s -> Tuple s a) which represents infinite streams of elements of type a.

This type can be constructed by creating a type constructor StreamF as follows:

data StreamF a s = StreamF s (s -> Tuple s a)

We can then define the type of streams using Exists:

type Stream a = Exists (StreamF a)

mkExists :: forall a f. f a -> Exists f

The mkExists function is used to introduce a value of type Exists f, by providing a value of type f a, for some type a which will be hidden in the existentially-quantified type.

For example, to create a value of type Stream Number, we might use mkExists as follows:

nats :: Stream Number
nats = mkExists $ StreamF 0 (\n -> Tuple (n + 1) n)

runExists :: forall r f. (forall a. f a -> r) -> Exists f -> r

The runExists function is used to eliminate a value of type Exists f. The rank 2 type ensures that the existentially-quantified type does not escape its scope. Since the function is required to work for any type a, it will work for the existentially-quantified type.

For example, we can write a function to obtain the head of a stream by using runExists as follows:

head :: forall a. Stream a -> a
head = runExists head'
  where
  head' :: forall s. StreamF a s -> a
  head' (StreamF s f) = snd (f s)