Safe Haskell | None |
---|---|

Language | Haskell2010 |

Attribute grammars over mutual recursive datatypes

## Synopsis

- data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat) = AnnFix (phi n) (Rep ki (AnnFix ki codes phi) (Lkup n codes))
- getAnn :: AnnFix ki codes ann ix -> ann ix
- annCata :: 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
- mapAnn :: IsNat ix => (forall iy. chi iy -> phi iy) -> AnnFix ki codes chi ix -> AnnFix ki codes phi ix
- synthesize :: forall ki phi codes ix. IsNat ix => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -> Fix ki codes ix -> AnnFix ki codes phi ix
- synthesizeM :: forall ki phi codes ix m. (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)
- synthesizeAnn :: forall ki codes chi phi ix. IsNat ix => (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -> AnnFix ki codes chi ix -> AnnFix ki codes phi ix

# 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.

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

Retrieves the top annotation at the current value.

:: 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 Source #

Forgetful natural transformation back into `Fix`

Maps over the annotations within an annotated fixpoint

:: 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.