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

Generics.MRSOP.AG

Contents

Description

Attribute grammars over mutual recursive datatypes

Synopsis

# Annotated Fixpoints

Annotated fixpoints are a very useful construction. Suppose the generic algorithm at hand frequently requires the height of the tree being processed. Instead of recomputing the height of the trees everytime we need them, we can annotate the whole tree with its height at each given point.

Given an algebra that computes height at one point, assuming the recursive positions have been substituted with their own heights,

heightAlgebra :: Rep ki (Const Int) xs -> Const Int iy
heightAlgebra = Const . (1+) . elimRep (const 0) getConst (maximum . (0:))

We can annotate each node with their height with the synthesize function.

synthesize heightAlgebra :: Fix ki codes ix -> AnnFix ki codes (Const Int) ix

Note how using just cata would simply count the number of nodes, forgetting the intermediate values.

cata heightAlgebra :: Fix ki codes ix -> Const Int ix

data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat) Source #

Annotated version of Fix. This is basically the Cofree datatype, but for n-ary functors.

Constructors

 AnnFix (phi n) (Rep ki (AnnFix ki codes phi) (Lkup n codes))

getAnn :: AnnFix ki codes ann ix -> ann ix Source #

Retrieves the top annotation at the current value.

Arguments

 :: IsNat ix => (forall iy. IsNat iy => chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -> AnnFix ki codes chi ix -> phi ix

forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix Source #

Forgetful natural transformation back into Fix

Arguments

 :: IsNat ix => (forall iy. chi iy -> phi iy) -> AnnFix ki codes chi ix -> AnnFix ki codes phi ix

Maps over the annotations within an annotated fixpoint

Arguments

 :: IsNat ix => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -> Fix ki codes ix -> AnnFix ki codes phi ix

Annotates a tree at every node with the result of the catamorphism with the supplied algebra called at each node.

Arguments

 :: (Monad m, IsNat ix) => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) -> Fix ki codes ix -> m (AnnFix ki codes phi ix)

Monadic variant of synthesize

Arguments

 :: IsNat ix => (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -> AnnFix ki codes chi ix -> AnnFix ki codes phi ix