Data.Exists
- Package
- purescript-exists
- Repository
- purescript/purescript-exists
#Exists Source
data Exists :: forall k. (k -> Type) -> Type
data Exists t0
This type constructor can be used to existentially quantify over a 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 Source
mkExists :: forall f a. 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 Source
runExists :: forall f r. (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)
- Modules
- Data.
Exists