This type constructor can be used to existentially quantify over a type of kind
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
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
type Stream a = Exists (StreamF a)
mkExists function is used to introduce a value of type
Exists f, by providing a value of
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 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)