# Data.Exists

- Package
- purescript-exists
- Repository
- purescript/purescript-exists

### #Exists Source

`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 Source

`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 Source

`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)
```

- Modules
- Data.
Exists