generics-mrsop-2.3.0: Generic Programming with Mutually Recursive Sums of Products.

Generics.MRSOP.Base.Combinators

Contents

Description

A collection of combinators for operating over sums of products.

Synopsis
• 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 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) 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 #

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