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

Language | Haskell2010 |

A collection of combinators for operating over sums of products.

- geq :: forall ki fam codes ix. Family ki fam codes => (forall k. ki k -> ki k -> Bool) -> El fam ix -> El fam ix -> Bool
- composM :: forall ki fam codes ix m. (Monad m, Family ki fam codes, IsNat ix) => (forall iy. IsNat iy => SNat iy -> El fam iy -> m (El fam iy)) -> El fam ix -> m (El fam ix)
- compos :: forall ki fam codes ix. (Family ki fam codes, IsNat ix) => (forall iy. IsNat iy => SNat iy -> El fam iy -> El fam iy) -> El fam ix -> El fam ix
- crushM :: forall ki fam codes ix r m. (Monad m, Family ki fam codes) => (forall k. ki k -> m r) -> ([r] -> m r) -> El fam ix -> m r
- crush :: forall ki fam codes ix r. Family ki fam codes => (forall k. ki k -> r) -> ([r] -> r) -> El fam ix -> r

# Equality

Compares two elements for equality.

geq :: forall ki fam codes ix. Family ki fam codes => (forall k. ki k -> ki k -> Bool) -> El fam ix -> El fam ix -> Bool Source #

Given a way to compare the constant types within two values, compare the outer values for syntatical equality.

# Compos

Applies a morphism everywhere in a structure.

Conceptually one can think of `compos`

as
having type `(b -> b) -> a -> a`

. The semantics
is applying the morphism over `b`

s wherever possible
inside a value of type `a`

.

For our case, we need `a`

and `b`

to be elements of
the same family.

composM :: forall ki fam codes ix m. (Monad m, Family ki fam codes, IsNat ix) => (forall iy. IsNat iy => SNat iy -> El fam iy -> m (El fam iy)) -> El fam ix -> m (El fam ix) Source #

Given a morphism for the `iy`

element of the family,
applies it everywhere in another element of
the family.

compos :: forall ki fam codes ix. (Family ki fam codes, IsNat ix) => (forall iy. IsNat iy => SNat iy -> El fam iy -> El fam iy) -> El fam ix -> El fam ix Source #

Non monadic version from above.

# Crush

Crush will collapse an entire value given only an action to perform on the leaves and a way of combining results.