The Exists type, for encoding existential types.
spago install exists
The type Exists f is isomorphic to the existential type exists a. f a.
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)The mkExists and runExists functions then enable packing and unpacking of SteamF into/out of Stream.
Module documentation is published on Pursuit.