Generics.MRSOP.Base.Combinators

A collection of combinators for operating over sums of products.

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

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

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

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.

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

crushM Applies its first parameter to all leaves, combines the results with its second parameter.

crush :: forall ki fam codes ix r. Family ki fam codes => (forall k. ki k -> r) -> ([r] -> r) -> El fam ix -> r

Non-monadic version