0 | ||| Multiplate allows for traversals over mutually recursive data types,
  1 | ||| while removing a lot of the boilerplate.
  2 | |||
  3 | ||| After writting some initial boilerplate, you can write much shorter
  4 | ||| and clearer transformations, as you don't need to manually recurse on each subterm.
  5 | module Multiplate
  6 |
  7 | import Control.Monad.Identity
  8 | import Control.Applicative.Const
  9 |
 10 | %default total
 11 |
 12 | ||| A projector represents a field of a plate
 13 | public export 0
 14 | Projector : ((Type -> Type) -> Type) -> Type -> Type
 15 | Projector p a = forall f. p f -> a -> f a
 16 |
 17 | ||| A plate is represents a set of applicative transforms over a type
 18 | ||| where each transform can be applied to sub-nodes of the type.
 19 | |||
 20 | ||| Additionally new plates can be built from a function
 21 | ||| which is generic over the type of nodes.
 22 | |||
 23 | ||| This works fine with indexed data types -
 24 | ||| see `tests/Multiplate/Tests/DeBruijn.idr` for an expression using De Bruijn indexes.
 25 | ||| You may need to beta-expand in the definition of `mkPlate` (ie change `build expr` to `build (\p => expr p)`)
 26 | |||
 27 | ||| @ p a plate parametised by an applicative functor
 28 | public export
 29 | interface Multiplate (0 p : (Type -> Type) -> Type) where
 30 |     ||| Take a plate and return a new plate,
 31 |     ||| which applies each transform in the old plate
 32 |     ||| to the direct children of each node.
 33 |     total
 34 |     multiplate : Applicative f => p f -> p f
 35 |     ||| Create a plate using a generic projector function
 36 |     total
 37 |     mkPlate : Applicative f => (forall a. Projector p a -> a -> f a) -> p f
 38 |
 39 | ||| A plate which 'does nothing' ie applies `pure` to each node.
 40 | public export %inline
 41 | purePlate : Multiplate p => Applicative f => p f
 42 | purePlate = mkPlate (\_ => pure)
 43 |
 44 | ||| Apply a natural transform to a plate
 45 | public export %inline
 46 | applyNaturalTransform : Multiplate p => Applicative g => (forall a. f a -> g a) -> p f -> p g
 47 | applyNaturalTransform f p = mkPlate $ \proj, x => f $ proj p x
 48 |
 49 | public export %inline
 50 | fromIdentity : Multiplate p => Applicative f => p Identity -> p f
 51 | fromIdentity = applyNaturalTransform (pure . runIdentity)
 52 |
 53 | infixl 5 `andThenM`
 54 |
 55 | ||| Compose 2 plates, by applying them from left to right.
 56 | public export %inline
 57 | andThenM : Monad m => Multiplate p => Lazy (p m) -> Lazy (p m) -> p m
 58 | andThenM p1 p2 = mkPlate $ \proj, x => do
 59 |     x' <- proj p1 x
 60 |     proj p2 x'
 61 |
 62 | infixl 5 `andThenId`
 63 |
 64 | ||| Compose 2 plates, where the second is based on the identity functor
 65 | public export %inline
 66 | andThenId : Multiplate p => Applicative m => Lazy (p m) -> Lazy (p Identity) -> p m
 67 | andThenId p1 p2 = mkPlate $ \proj, x => proj p1 x <&> \x' => runIdentity (proj p2 x')
 68 |
 69 | infixl 5 `iAndThen`
 70 |
 71 | ||| Compose 2 plates, where the first is based on the identity functor
 72 | public export %inline
 73 | idAndThen : Multiplate p => Applicative m => Lazy (p Identity) -> Lazy (p m) -> p m
 74 | idAndThen p1 p2 = mkPlate $ \proj, x =>
 75 |     let x' = runIdentity $ proj p1 x
 76 |      in proj p2 x'
 77 |
 78 | infixr 4 `orElse`
 79 |
 80 | ||| Compose 2 plates, by trying the first and then the second
 81 | public export %inline
 82 | orElse : Alternative m => Multiplate p => Lazy (p m) -> Lazy (p m) -> p m
 83 | orElse p1 p2 = mkPlate $ \proj, x => proj p1 x <|> proj p2 x
 84 |
 85 | ||| Apply a transformation to the whole family of a node.
 86 | ||| This happens in a post-order, ie children are mapped before parents.
 87 | public export covering
 88 | postorderMap : Multiplate p => Monad m => p m -> p m
 89 | postorderMap p = multiplate (postorderMap p) `andThenM` p
 90 |
 91 | ||| Apply a transformation to the whole family of a node.
 92 | ||| This happens in a pre-order, ie parents are mapped before children.
 93 | public export covering
 94 | preorderMap : Multiplate p => Monad m => p m -> p m
 95 | preorderMap p = p `andThenM` multiplate (preorderMap p)
 96 |
 97 | ||| Append the result of 2 plates which each return `Const`
 98 | public export %inline
 99 | append : Multiplate p => Monoid o => Lazy (p (Const o)) -> Lazy (p (Const o)) -> p (Const o)
100 | append p1 p2 = mkPlate $ \proj, x => proj p1 x <+> proj p2 x
101 |
102 | ||| Apply a fold to the whole family of a node.
103 | ||| This applies to the parent node, followed by children.
104 | |||
105 | ||| The result, when applied to `x` looks like:
106 | ||| ```
107 | ||| x
108 | |||     <+> children x
109 | |||     <+> grandchildren x
110 | |||     ...
111 | ||| ```
112 | public export covering
113 | preorderFold : Multiplate p => Monoid o => p (Const o) -> p (Const o)
114 | preorderFold p = p `append` multiplate (preorderFold p)
115 |
116 | ||| Apply a fold to the whole family of a node.
117 | ||| This applies to the children, followed by the parent node.
118 | |||
119 | ||| The result when applied to `x` looks like:
120 | ||| ```
121 | ||| ...
122 | |||     <+> grandchildren x
123 | |||     <+> children x
124 | |||     <+> x
125 | public export covering
126 | postorderFold : Multiplate p => Monoid o => p (Const o) -> p (Const o)
127 | postorderFold p = multiplate (postorderFold p) `append` p 
128 |
129 | ||| Remove a `Maybe` from a transformation by providing a plate which generates a default value.
130 | public export %inline
131 | catchWith : Multiplate p => Applicative f => p Maybe -> p f -> p f
132 | catchWith p def = mkPlate $ \proj, x => case proj p x of
133 |     Just x' => pure x'
134 |     Nothing => proj def x
135 |
136 | ||| Remove a `Maybe` from a transformation by returning the original value unaltered.
137 | |||
138 | ||| This is equivalent to `catchWith purePlate`
139 | public export %inline
140 | catch : Multiplate p => Applicative f => p Maybe -> p f
141 | catch p = mkPlate $ \proj, x => case proj p x of
142 |     Just x' => pure x'
143 |     Nothing => pure x
144 |
145 | ||| Plates tend to consist of a fixed set of fields.
146 | ||| This interface allows for projecting the transform of @ a.
147 | |||
148 | ||| @ p the plate
149 | ||| @ a the field
150 | public export
151 | interface Multiplate p => HasProjection p a where
152 |     ||| Project a transform of a specific field out of a plate.
153 |     total
154 |     project : Projector p a
155 |
156 | ||| Run a transformation in the identity monad.
157 | |||
158 | ||| To run transforms in a different Monad use `project`
159 | public export %inline
160 | traverseFor : HasProjection p a => p Identity -> a -> a
161 | traverseFor p x = runIdentity $ project p x
162 |
163 | ||| Run a fold
164 | public export %inline
165 | foldFor : HasProjection p a => p (Const o) -> a -> o
166 | foldFor p x = runConst $ project p x
167 |
168 | ||| Plates tend to consist of a fixed set of fields.
169 | ||| In addition to being able to project a field,
170 | ||| this interface allows for creating a plate from a transform.
171 | |||
172 | ||| This is seperate from `HasProjection` as it is typically not
173 | ||| possible to implement for plates with indexed data types.
174 | |||
175 | ||| @ p the plate
176 | ||| @ a the field
177 | public export
178 | interface HasProjection p a => HasField p a where
179 |     ||| Inject a transform to create a new plate,
180 |     ||| by filling in other transforms with `pure`.
181 |     total
182 |     inject : Applicative f => (a -> f a) -> p f
183 |     inject f = update f purePlate
184 |     ||| Update the transform of a given field,
185 |     ||| by replacing it with a new transform.
186 |     total
187 |     update : (a -> f a) -> p f -> p f
188 |
189 | ||| Inject a pure transformation into a plate.
190 | public export %inline
191 | injectPure : HasField p a => Applicative f => (a -> a) -> p f
192 | injectPure f = inject $ pure . f
193 |