Idris2Doc : Multiplate

Multiplate

(source)
Multiplate allows for traversals over mutually recursive data types,
while removing a lot of the boilerplate.

After writting some initial boilerplate, you can write much shorter
and clearer transformations, as you don't need to manually recurse on each subterm.

Definitions

0Projector : ((Type->Type) ->Type) ->Type->Type
  A projector represents a field of a plate

Totality: total
Visibility: public export
interfaceMultiplate : ((Type->Type) ->Type) ->Type
  A plate is represents a set of applicative transforms over a type
where each transform can be applied to sub-nodes of the type.

Additionally new plates can be built from a function
which is generic over the type of nodes.

This works fine with indexed data types -
see `tests/Multiplate/Tests/DeBruijn.idr` for an expression using De Bruijn indexes.
You may need to beta-expand in the definition of `mkPlate` (ie change `build expr` to `build (\p => expr p)`)

@ p a plate parametised by an applicative functor

Parameters: p
Methods:
multiplate : Applicativef=>pf->pf
  Take a plate and return a new plate,
which applies each transform in the old plate
to the direct children of each node.
mkPlate : Applicativef=> (Projectorpa->a->fa) ->pf
  Create a plate using a generic projector function

Implementation: 
HasProjectionpa->Multiplatep
multiplate : Multiplatep=>Applicativef=>pf->pf
  Take a plate and return a new plate,
which applies each transform in the old plate
to the direct children of each node.

Totality: total
Visibility: public export
mkPlate : Multiplatep=>Applicativef=> (Projectorpa->a->fa) ->pf
  Create a plate using a generic projector function

Totality: total
Visibility: public export
purePlate : Multiplatep=>Applicativef=>pf
  A plate which 'does nothing' ie applies `pure` to each node.

Totality: total
Visibility: public export
applyNaturalTransform : Multiplatep=>Applicativeg=> (fa->ga) ->pf->pg
  Apply a natural transform to a plate

Totality: total
Visibility: public export
fromIdentity : Multiplatep=>Applicativef=>pIdentity->pf
Totality: total
Visibility: public export
andThenM : Monadm=>Multiplatep=> Lazy (pm) -> Lazy (pm) ->pm
  Compose 2 plates, by applying them from left to right.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5
andThenId : Multiplatep=>Applicativem=> Lazy (pm) -> Lazy (pIdentity) ->pm
  Compose 2 plates, where the second is based on the identity functor

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5
idAndThen : Multiplatep=>Applicativem=> Lazy (pIdentity) -> Lazy (pm) ->pm
  Compose 2 plates, where the first is based on the identity functor

Totality: total
Visibility: public export
orElse : Alternativem=>Multiplatep=> Lazy (pm) -> Lazy (pm) ->pm
  Compose 2 plates, by trying the first and then the second

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
postorderMap : Multiplatep=>Monadm=>pm->pm
  Apply a transformation to the whole family of a node.
This happens in a post-order, ie children are mapped before parents.

Visibility: public export
preorderMap : Multiplatep=>Monadm=>pm->pm
  Apply a transformation to the whole family of a node.
This happens in a pre-order, ie parents are mapped before children.

Visibility: public export
append : Multiplatep=>Monoido=> Lazy (p (Consto)) -> Lazy (p (Consto)) ->p (Consto)
  Append the result of 2 plates which each return `Const`

Totality: total
Visibility: public export
preorderFold : Multiplatep=>Monoido=>p (Consto) ->p (Consto)
  Apply a fold to the whole family of a node.
This applies to the parent node, followed by children.

The result, when applied to `x` looks like:
```
x
<+> children x
<+> grandchildren x
...
```

Visibility: public export
postorderFold : Multiplatep=>Monoido=>p (Consto) ->p (Consto)
  Apply a fold to the whole family of a node.
This applies to the children, followed by the parent node.

The result when applied to `x` looks like:
```
...
<+> grandchildren x
<+> children x
<+> x

Visibility: public export
catchWith : Multiplatep=>Applicativef=>pMaybe->pf->pf
  Remove a `Maybe` from a transformation by providing a plate which generates a default value.

Totality: total
Visibility: public export
catch : Multiplatep=>Applicativef=>pMaybe->pf
  Remove a `Maybe` from a transformation by returning the original value unaltered.

This is equivalent to `catchWith purePlate`

Totality: total
Visibility: public export
interfaceHasProjection : ((Type->Type) ->Type) ->Type->Type
  Plates tend to consist of a fixed set of fields.
This interface allows for projecting the transform of @ a.

@ p the plate
@ a the field

Parameters: p, a
Constraints: Multiplate p
Methods:
project : Projectorpa
  Project a transform of a specific field out of a plate.

Implementation: 
HasFieldpa->HasProjectionpa
project : HasProjectionpa=>Projectorpa
  Project a transform of a specific field out of a plate.

Totality: total
Visibility: public export
traverseFor : HasProjectionpa=>pIdentity->a->a
  Run a transformation in the identity monad.

To run transforms in a different Monad use `project`

Totality: total
Visibility: public export
foldFor : HasProjectionpa=>p (Consto) ->a->o
  Run a fold

Totality: total
Visibility: public export
interfaceHasField : ((Type->Type) ->Type) ->Type->Type
  Plates tend to consist of a fixed set of fields.
In addition to being able to project a field,
this interface allows for creating a plate from a transform.

This is seperate from `HasProjection` as it is typically not
possible to implement for plates with indexed data types.

@ p the plate
@ a the field

Parameters: p, a
Constraints: HasProjection p a
Methods:
inject : Applicativef=> (a->fa) ->pf
  Inject a transform to create a new plate,
by filling in other transforms with `pure`.
update : (a->fa) ->pf->pf
  Update the transform of a given field,
by replacing it with a new transform.
inject : HasFieldpa=>Applicativef=> (a->fa) ->pf
  Inject a transform to create a new plate,
by filling in other transforms with `pure`.

Totality: total
Visibility: public export
update : HasFieldpa=> (a->fa) ->pf->pf
  Update the transform of a given field,
by replacing it with a new transform.

Totality: total
Visibility: public export
injectPure : HasFieldpa=>Applicativef=> (a->a) ->pf
  Inject a pure transformation into a plate.

Totality: total
Visibility: public export