Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- data Union (r :: [(* -> *) -> * -> *]) (m :: * -> *) a where
- data Yo e m a where
- liftYo :: Functor m => e m a -> Yo e m a
- type Member e r = Member' e r
- inj :: forall r e a m. (Functor m, Member e r) => e m a -> Union r m a
- weaken :: Union r m a -> Union (e ': r) m a
- weakenUnder :: Union (e1 ': r) m a -> Union (e1 ': (e2 ': r)) m a
- weakenUnder2 :: Union (e1 ': r) m a -> Union (e1 ': (e2 ': (e3 ': r))) m a
- weakenUnder3 :: Union (e1 ': r) m a -> Union (e1 ': (e2 ': (e3 ': (e4 ': r)))) m a
- decomp :: Union (e ': r) m a -> Either (Union r m a) (Yo e m a)
- prj :: forall e r a m. Member e r => Union r m a -> Maybe (Yo e m a)
- extract :: Union '[e] m a -> Yo e m a
- absurdU :: Union '[] m a -> b
- decompCoerce :: Union (e ': r) m a -> Either (Union (f ': r) m a) (Yo e m a)
- data SNat :: Nat -> * where
- data Nat

# Documentation

data Union (r :: [(* -> *) -> * -> *]) (m :: * -> *) a where Source #

An extensible, type-safe union. The `r`

type parameter is a type-level
list of effects, any one of which may be held within the `Union`

.

type Member e r = Member' e r Source #

A proof that the effect `e`

is available somewhere inside of the effect
stack `r`

.

# Building Unions

inj :: forall r e a m. (Functor m, Member e r) => e m a -> Union r m a Source #

Lift an effect `e`

into a `Union`

capable of holding it.

weaken :: Union r m a -> Union (e ': r) m a Source #

Weaken a `Union`

so it is capable of storing a new sort of effect.

weakenUnder :: Union (e1 ': r) m a -> Union (e1 ': (e2 ': r)) m a Source #

Like `weaken`

, but introduces a new effect under the top of the stack.

weakenUnder2 :: Union (e1 ': r) m a -> Union (e1 ': (e2 ': (e3 ': r))) m a Source #

Like `weaken`

, but introduces a new effect under the top of the stack.

weakenUnder3 :: Union (e1 ': r) m a -> Union (e1 ': (e2 ': (e3 ': (e4 ': r)))) m a Source #

Like `weaken`

, but introduces a new effect under the top of the stack.

# Using Unions

decomp :: Union (e ': r) m a -> Either (Union r m a) (Yo e m a) Source #

Decompose a `Union`

. Either this union contains an effect `e`

---the head
of the `r`

list---or it doesn't.

prj :: forall e r a m. Member e r => Union r m a -> Maybe (Yo e m a) Source #

Attempt to take an `e`

effect out of a `Union`

.

absurdU :: Union '[] m a -> b Source #

An empty union contains nothing, so this function is uncallable.

decompCoerce :: Union (e ': r) m a -> Either (Union (f ': r) m a) (Yo e m a) Source #

Like `decomp`

, but allows for a more efficient
`reinterpret`

function.

# Witnesses

data SNat :: Nat -> * where Source #

A singleton for `Nat`

.

## Instances

TestEquality SNat Source # | |

Defined in Polysemy.Internal.Union |