0 | ||| Deriving traversable instances using reflection
1 | ||| You can for instance define:
2 | ||| ```
3 | ||| data Tree a = Leaf a | Node (Tree a) (Tree a)
4 | ||| treeFoldable : Traversable Tree
5 | ||| treeFoldable = %runElab derive
6 | ||| ```
20 | %language ElabReflection
23 | ------------------------------------------------------------------------------
24 | -- Errors
26 | ||| Possible errors for the functor-deriving machinery.
39 | -- Contextual information
43 | export
50 | go acc (NotATraversable s) = acc <>> ["Couldn't find a `Traversable' instance for the type constructor \{show s}"]
51 | go acc (NotABitraversable s) = acc <>> ["Couldn't find a `Bitraversable' instance for the type constructor \{show s}"]
52 | go acc (NotTraversableInItsLastArg s) = acc <>> ["Not traversable in its last argument \{show s}"]
58 | go acc (WhenCheckingConstructor nm err) = go (acc :< "When checking constructor \{show nm}") err
72 | <|> IVar emptyFC `{Prelude.Interfaces.Bitraversable} <$ guard (pos `elem` params.asBitraversables)
74 | ------------------------------------------------------------------------------
75 | -- Core machinery: being traversable
77 | -- Not meant to be re-exported as it's using the internal notion of error
87 | ||| IsTraversableIn is parametrised by
88 | ||| @ t the name of the data type whose constructors are being analysed
89 | ||| @ x the name of the type variable that the traversable action will act on
90 | ||| @ ty the type being analysed
91 | ||| The inductive type delivers a proof that x can be traversed over in ty,
92 | ||| assuming that t also is traversable.
95 | ||| The type variable x occurs alone
97 | ||| There is a recursive subtree of type (t a1 ... an u) and u is Traversable in x.
98 | ||| We do not insist that u is exactly x so that we can deal with nested types
99 | ||| like the following:
100 | ||| data Full a = Leaf a | Node (Full (a, a))
101 | ||| data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))
104 | ||| The subterm is delayed (Lazy only, we can't traverse infinite structures)
106 | ||| There are nested subtrees somewhere inside a 3rd party type constructor
107 | ||| which satisfies the Bitraversable interface
111 | ||| There are nested subtrees somewhere inside a 3rd party type constructor
112 | ||| which satisfies the Traversable interface
115 | ||| A type free of x is trivially Traversable in it
118 | parameters
127 | ||| When analysing the type of a constructor for the type family t,
128 | ||| we hope to observe
129 | ||| 1. either that it is traversable in x
130 | ||| 2. or that it is free of x
131 | ||| If it is not the case, we will use the `MonadError Error` constraint
132 | ||| to fail with an informative message.
137 | export
142 | ||| Hoping to observe that ty is traversable
143 | export
146 | ||| To avoid code duplication in typeView, we have an auxiliary function
147 | ||| specifically to handle the application case
157 | -- if x is present in the argument then the function better be:
158 | -- 1. free of x
159 | -- 2. either an occurrence of t i.e. a subterm
160 | -- or a type constructor already known to be functorial
170 | -- record that the nth parameter should be functorial
174 | -- and happily succeed
179 | -- Otherwise it better be the case that f is also free of x so that
180 | -- we can mark the whole type as being x-free.
203 | -- record that the nth parameter should be bitraversable
207 | -- and happily succeed
226 | ------------------------------------------------------------------------------
227 | -- Core machinery: building the traverse function from an IsTraversableIn proof
231 | ||| traverseFun takes
232 | ||| @ mutualWith a list of mutually defined type constructors. Calls to their
233 | ||| respective mapping functions typically need an assert_total because the
234 | ||| termination checker is not doing enough inlining to see that things are
235 | ||| terminating
236 | ||| @ assert records whether we should mark recursive calls as total because
237 | ||| we are currently constructing the argument to a higher order function
238 | ||| which will obscure the termination argument. Starts as `Nothing`, becomes
239 | ||| `Just False` if an `assert_total` has already been inserted.
240 | ||| @ ty the type being transformed by the mapping function
241 | ||| @ rec the name of the mapping function being defined (used for recursive calls)
242 | ||| @ f the name of the function we're mapping
243 | ||| @ arg the (optional) name of the argument being mapped over. This lets us use
244 | ||| Nothing when generating arguments to higher order functions so that we generate
245 | ||| the eta contracted `map (mapTree f)` instead of `map (\ ts => mapTree f ts)`.
250 | -- only add assert_total if it is declared to be needed
254 | -- here we need to eta-expand to avoid "Lazy t does not unify with t" errors
260 | ]
265 | ]
267 | -- only add assert_total if we are calling a mutually defined Traversable implementation.
268 | = let isMutual = fromMaybe False (appView ty >>= \ v => pure (snd v.head `elem` mutualWith)) in
284 | ------------------------------------------------------------------------------
285 | -- User-facing: Traversable deriving
293 | let eta = foldr (\ x => ILam fc MW ExplicitArg (Just x) (Implicit fc False)) (apply c args) lams in
296 | where
313 | in
335 | -- expand the mutualwith names to have the internal, fully qualified, names
340 | -- The goal should have the shape (Traversable t)
346 | -- t should be a type constructor
350 | joinBy "\n" $ "" :: map (\ (n, ty) => " \{showPrefix True $ dropNS n} : \{show $ mapTTImp cleanup ty}") cs
352 | -- Generate a clause for each data constructor
360 | -- Grab the types of the constructor's explicit arguments
365 | "\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
379 | -- a covering/partial definition
389 | -- Generate the type of the mapping function
406 | -- Define the instance
412 | ||| Derive an implementation of Traversable for a type constructor.
413 | ||| This can be used like so:
414 | ||| ```
415 | ||| data Tree a = Leaf a | Node (Tree a) (Tree a)
416 | ||| treeTraversable : Traversable Tree
417 | ||| treeTraversable = %runElab derive
418 | ||| ```
419 | export