purescript-exists

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.