Generics.MRSOP.AG

Attribute grammars over mutual recursive datatypes

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)

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

Retrieves the top annotation at the current value.

annCata

Arguments

:: IsNat ix

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

-> AnnFix ki codes chi ix

-> phi ix

Catamorphism with access to the annotations

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

Forgetful natural transformation back into Fix

mapAnn

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

synthesize

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.

synthesizeM

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

synthesizeAnn

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

Synthesized attributes with an algebra that has access to the annotations.