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.