Deriving.Foldable


   0 | ||| Deriving foldable instances using reflection
   1 | ||| You can for instance define:
   2 | ||| ```
   3 | ||| data Tree a = Leaf a | Node (Tree a) (Tree a)
   4 | ||| treeFoldable : Foldable Tree
   5 | ||| treeFoldable = %runElab derive
   6 | ||| ```
   7 | 
   8 | module Deriving.Foldable
   9 | 
  10 | import public Control.Monad.Either
  11 | import public Control.Monad.State
  12 | import public Data.List1
  13 | import public Data.Maybe
  14 | import public Data.Morphisms
  15 | import public Decidable.Equality
  16 | import public Language.Reflection
  17 | 
  18 | import public Deriving.Common
  19 | 
  20 | %language ElabReflection
  21 | %default total
  22 | 
  23 | public export
  24 | fromFoldMap :
  25 |   (0 f : Type -> Type) ->
  26 |   (forall a, b. Monoid b => (a -> b) -> f a -> b) ->
  27 |   Foldable f
  28 | fromFoldMap f fm = MkFoldable
  29 |   foldr
  30 |   foldl
  31 |   (foldr (\_, _ => False) True)
  32 |   (\ cons => foldl (\ acc, x => acc >>= flip cons x) . pure)
  33 |   (foldr (::) [])
  34 |   fm
  35 | 
  36 |   where
  37 | 
  38 |     foldr : forall a, b. (a -> b -> b) -> b -> f a -> b
  39 |     foldr cons base t = applyEndo (fm (Endo . cons) t) base
  40 | 
  41 |     foldl : forall a, b. (b -> a -> b) -> b -> f a -> b
  42 |     foldl cons base t = foldr (flip (.) . flip cons) id t base
  43 | 
  44 | ------------------------------------------------------------------------------
  45 | -- Errors
  46 | 
  47 | ||| Possible errors for the functor-deriving machinery.
  48 | public export
  49 | data Error : Type where
  50 |   NotFreeOf : Name -> TTImp -> Error
  51 |   NotAnApplication : TTImp -> Error
  52 |   NotAFoldable : TTImp -> Error
  53 |   NotABifoldable : TTImp -> Error
  54 |   NotFoldableInItsLastArg : TTImp -> Error
  55 |   UnsupportedType : TTImp -> Error
  56 |   NotAFiniteStructure : Error
  57 |   NotAnUnconstrainedValue : Count -> Error
  58 |   InvalidGoal : Error
  59 |   ConfusingReturnType : Error
  60 |   -- Contextual information
  61 |   WhenCheckingConstructor : Name -> Error -> Error
  62 |   WhenCheckingArg : TTImp -> Error -> Error
  63 | 
  64 | export
  65 | Show Error where
  66 |   show = joinBy "\n" . go [<] where
  67 | 
  68 |     go : SnocList String -> Error -> List String
  69 |     go acc (NotFreeOf x ty) = acc <>> ["The term \{show ty} is not free of \{show x}"]
  70 |     go acc (NotAnApplication s) = acc <>> ["The type \{show s} is not an application"]
  71 |     go acc (NotAFoldable s) = acc <>> ["Couldn't find a `Foldable' instance for the type constructor \{show s}"]
  72 |     go acc (NotABifoldable s) = acc <>> ["Couldn't find a `Bifoldable' instance for the type constructor \{show s}"]
  73 |     go acc (NotFoldableInItsLastArg s) = acc <>> ["Not foldable in its last argument \{show s}"]
  74 |     go acc (UnsupportedType s) = acc <>> ["Unsupported type \{show s}"]
  75 |     go acc NotAFiniteStructure = acc <>> ["Cannot fold over an infinite structure"]
  76 |     go acc (NotAnUnconstrainedValue rig) = acc <>> ["Cannot fold over a \{enunciate rig} value"]
  77 |     go acc InvalidGoal = acc <>> ["Expected a goal of the form `Foldable f`"]
  78 |     go acc ConfusingReturnType = acc <>> ["Confusing telescope"]
  79 |     go acc (WhenCheckingConstructor nm err) = go (acc :< "When checking constructor \{show nm}") err
  80 |     go acc (WhenCheckingArg s err) = go (acc :< "When checking argument of type \{show s}") err
  81 | 
  82 | record Parameters where
  83 |   constructor MkParameters
  84 |   asFoldables : List Nat
  85 |   asBifoldables : List Nat
  86 | 
  87 | initParameters : Parameters
  88 | initParameters = MkParameters [] []
  89 | 
  90 | paramConstraints : Parameters -> Nat -> Maybe TTImp
  91 | paramConstraints params pos
  92 |     = IVar emptyFC `{Prelude.Interfaces.Foldable}   <$ guard (pos `elem` params.asFoldables)
  93 |   <|> IVar emptyFC `{Prelude.Interfaces.Bifoldable} <$ guard (pos `elem` params.asBifoldables)
  94 | 
  95 | ------------------------------------------------------------------------------
  96 | -- Core machinery: being foldable
  97 | 
  98 | -- Not meant to be re-exported as it's using the internal notion of error
  99 | isFreeOf' :
 100 |   {0 m : Type -> Type} ->
 101 |   {auto elab : Elaboration m} ->
 102 |   {auto error : MonadError Error m} ->
 103 |   (x : Name) -> (ty : TTImp) -> m (IsFreeOf x ty)
 104 | isFreeOf' x ty = case isFreeOf x ty of
 105 |   Nothing => throwError (NotFreeOf x ty)
 106 |   Just prf => pure prf
 107 | 
 108 | ||| IsFoldableIn is parametrised by
 109 | ||| @ t  the name of the data type whose constructors are being analysed
 110 | ||| @ x  the name of the type variable that the foldable action will act on
 111 | ||| @ ty the type being analysed
 112 | ||| The inductive type delivers a proof that x can be folded over in ty,
 113 | ||| assuming that t also is foldable.
 114 | public export
 115 | data IsFoldableIn : (t, x : Name) -> (ty : TTImp) -> Type where
 116 |   ||| The type variable x occurs alone
 117 |   FIVar : IsFoldableIn t x (IVar fc x)
 118 |   ||| There is a recursive subtree of type (t a1 ... an u) and u is Foldable in x.
 119 |   ||| We do not insist that u is exactly x so that we can deal with nested types
 120 |   ||| like the following:
 121 |   |||   data Full a = Leaf a | Node (Full (a, a))
 122 |   |||   data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))
 123 |   FIRec : (0 _ : IsAppView (_, t) _ f) -> IsFoldableIn t x arg ->
 124 |           IsFoldableIn t x (IApp fc f arg)
 125 |   ||| The subterm is delayed (Lazy only, we can't fold over infinite structures)
 126 |   FIDelayed : IsFoldableIn t x ty -> IsFoldableIn t x (IDelayed fc LLazy ty)
 127 |   ||| There are nested subtrees somewhere inside a 3rd party type constructor
 128 |   ||| which satisfies the Bifoldable interface
 129 |   FIBifold : IsFreeOf x sp -> HasImplementation Bifoldable sp ->
 130 |              IsFoldableIn t x arg1 -> Either (IsFoldableIn t x arg2) (IsFreeOf x arg2) ->
 131 |              IsFoldableIn t x (IApp fc1 (IApp fc2 sp arg1) arg2)
 132 |   ||| There are nested subtrees somewhere inside a 3rd party type constructor
 133 |   ||| which satisfies the Foldable interface
 134 |   FIFold : IsFreeOf x sp -> HasImplementation Foldable sp ->
 135 |            IsFoldableIn t x arg -> IsFoldableIn t x (IApp fc sp arg)
 136 |   ||| A type free of x is trivially Foldable in it
 137 |   FIFree : IsFreeOf x a -> IsFoldableIn t x a
 138 | 
 139 | parameters
 140 |   {0 m : Type -> Type}
 141 |   {auto elab : Elaboration m}
 142 |   {auto error : MonadError Error m}
 143 |   {auto cs : MonadState Parameters m}
 144 |   (t : Name)
 145 |   (ps : List (Name, Nat))
 146 |   (x : Name)
 147 | 
 148 |   ||| When analysing the type of a constructor for the type family t,
 149 |   ||| we hope to observe
 150 |   |||   1. either that it is foldable in x
 151 |   |||   2. or that it is free of x
 152 |   ||| If it is not the case, we will use the `MonadError Error` constraint
 153 |   ||| to fail with an informative message.
 154 |   public export
 155 |   TypeView : TTImp -> Type
 156 |   TypeView ty = Either (IsFoldableIn t x ty) (IsFreeOf x ty)
 157 | 
 158 |   export
 159 |   fromTypeView : TypeView ty -> IsFoldableIn t x ty
 160 |   fromTypeView (Left prf) = prf
 161 |   fromTypeView (Right fo) = FIFree fo
 162 | 
 163 |   ||| Hoping to observe that ty is foldable
 164 |   export
 165 |   typeView : (ty : TTImp) -> m (TypeView ty)
 166 | 
 167 |   ||| To avoid code duplication in typeView, we have an auxiliary function
 168 |   ||| specifically to handle the application case
 169 |   typeAppView :
 170 |     {fc : FC} ->
 171 |     {f : TTImp} -> IsFreeOf x f ->
 172 |     (arg : TTImp) ->
 173 |     m (TypeView (IApp fc f arg))
 174 | 
 175 |   typeAppView {fc, f} isFO arg = do
 176 |     chka <- typeView arg
 177 |     case chka of
 178 |       -- if x is present in the argument then the function better be:
 179 |       -- 1. free of x
 180 |       -- 2. either an occurrence of t i.e. a subterm
 181 |       --    or a type constructor already known to be functorial
 182 |       Left sp => do
 183 |         let Just (MkAppView (_, hd) ts prf) = appView f
 184 |            | _ => throwError (NotAnApplication f)
 185 |         case decEq t hd of
 186 |           Yes Refl => pure $ Left (FIRec prf sp)
 187 |           No diff => case !(hasImplementation Foldable f) of
 188 |             Just prf => pure (Left (FIFold isFO prf sp))
 189 |             Nothing => case lookup hd ps of
 190 |               Just n => do
 191 |                 -- record that the nth parameter should be functorial
 192 |                 ns <- gets asFoldables
 193 |                 let ns = ifThenElse (n `elem` ns) ns (n :: ns)
 194 |                 modify { asFoldables := ns }
 195 |                 -- and happily succeed
 196 |                 logMsg "derive.foldable.assumption" 10 $
 197 |                   "I am assuming that the parameter \{show hd} is a Foldable"
 198 |                 pure (Left (FIFold isFO assert_hasImplementation sp))
 199 |               Nothing => throwError (NotAFoldable f)
 200 |       -- Otherwise it better be the case that f is also free of x so that
 201 |       -- we can mark the whole type as being x-free.
 202 |       Right fo => do
 203 |         Right _ <- typeView f
 204 |           | _ => throwError $ NotFoldableInItsLastArg (IApp fc f arg)
 205 |         pure (Right assert_IsFreeOf)
 206 | 
 207 |   typeView tm@(IVar fc y) = case decEq x y of
 208 |     Yes Refl => pure (Left FIVar)
 209 |     No _ => pure (Right assert_IsFreeOf)
 210 |   typeView fab@(IApp _ (IApp fc1 f arg1) arg2) = do
 211 |     chka1 <- typeView arg1
 212 |     case chka1 of
 213 |       Right _ => do isFO <- isFreeOf' x (IApp _ f arg1)
 214 |                     typeAppView {f = assert_smaller fab (IApp _ f arg1)} isFO arg2
 215 |       Left sp => do
 216 |         isFO <- isFreeOf' x f
 217 |         case !(hasImplementation Bifoldable f) of
 218 |           Just prf => pure (Left (FIBifold isFO prf sp !(typeView arg2)))
 219 |           Nothing => do
 220 |             let Just (MkAppView (_, hd) ts prf) = appView f
 221 |                | _ => throwError (NotAnApplication f)
 222 |             case lookup hd ps of
 223 |               Just n => do
 224 |                 -- record that the nth parameter should be bifoldable
 225 |                 ns <- gets asBifoldables
 226 |                 let ns = ifThenElse (n `elem` ns) ns (n :: ns)
 227 |                 modify { asBifoldables := ns }
 228 |                 -- and happily succeed
 229 |                 logMsg "derive.foldable.assumption" 10 $
 230 |                     "I am assuming that the parameter \{show hd} is a Bifoldable"
 231 |                 pure (Left (FIBifold isFO assert_hasImplementation sp !(typeView arg2)))
 232 |               Nothing => throwError (NotABifoldable f)
 233 |   typeView (IApp _ f arg) = do
 234 |     isFO <- isFreeOf' x f
 235 |     typeAppView isFO arg
 236 |   typeView (IDelayed _ lz f) = case !(typeView f) of
 237 |     Left sp => case lz of
 238 |       LLazy => pure (Left (FIDelayed sp))
 239 |       _ => throwError NotAFiniteStructure
 240 |     Right _ => pure (Right assert_IsFreeOf)
 241 |   typeView (IPrimVal _ _) = pure (Right assert_IsFreeOf)
 242 |   typeView (IType _) = pure (Right assert_IsFreeOf)
 243 |   typeView ty = case isFreeOf x ty of
 244 |     Nothing => throwError (UnsupportedType ty)
 245 |     Just prf => pure (Right prf)
 246 | 
 247 | ------------------------------------------------------------------------------
 248 | -- Core machinery: building the foldMap function from an IsFoldableIn proof
 249 | 
 250 | parameters (fc : FC) (mutualWith : List Name)
 251 | 
 252 |   ||| foldMapFun takes
 253 |   ||| @ mutualWith a list of mutually defined type constructors. Calls to their
 254 |   ||| respective mapping functions typically need an assert_total because the
 255 |   ||| termination checker is not doing enough inlining to see that things are
 256 |   ||| terminating
 257 |   ||| @ assert records whether we should mark recursive calls as total because
 258 |   ||| we are currently constructing the argument to a higher order function
 259 |   ||| which will obscure the termination argument. Starts as `Nothing`, becomes
 260 |   ||| `Just False` if an `assert_total` has already been inserted.
 261 |   ||| @ ty the type being transformed by the mapping function
 262 |   ||| @ rec the name of the mapping function being defined (used for recursive calls)
 263 |   ||| @ f the name of the function we're mapping
 264 |   ||| @ arg the (optional) name of the argument being mapped over. This lets us use
 265 |   ||| Nothing when generating arguments to higher order functions so that we generate
 266 |   ||| the eta contracted `map (mapTree f)` instead of `map (\ ts => mapTree f ts)`.
 267 |   foldMapFun : (assert : Maybe Bool) -> {ty : TTImp} -> IsFoldableIn t x ty ->
 268 |                (rec, f : Name) -> (arg : Maybe TTImp) -> TTImp
 269 |   foldMapFun assert FIVar rec f t = apply fc (IVar fc f) (toList t)
 270 |   foldMapFun assert (FIRec y sp) rec f t
 271 |     -- only add assert_total if it is declared to be needed
 272 |     = ifThenElse (fromMaybe False assert) (IApp fc (IVar fc (UN $ Basic "assert_total"))) id
 273 |     $ apply fc (IVar fc rec) (foldMapFun (Just False) sp rec f Nothing :: toList t)
 274 |   foldMapFun assert (FIDelayed sp) rec f Nothing
 275 |     -- here we need to eta-expand to avoid "Lazy t does not unify with t" errors
 276 |     = let nm = UN $ Basic "eta" in
 277 |       ILam fc MW ExplicitArg (Just nm) (IDelayed fc LLazy (Implicit fc False))
 278 |     $ foldMapFun assert sp rec f (Just (IVar fc nm))
 279 |   foldMapFun assert (FIDelayed sp) rec f (Just t)
 280 |     = foldMapFun assert sp rec f (Just t)
 281 |   foldMapFun assert {ty = IApp _ ty _} (FIFold _ _ sp) rec f t
 282 |     -- only add assert_total if we are calling a mutually defined Foldable implementation.
 283 |     = let isMutual = fromMaybe False (appView ty >>= \ v => pure (snd v.head `elem` mutualWith)) in
 284 |       ifThenElse isMutual (IApp fc (IVar fc (UN $ Basic "assert_total"))) id
 285 |     $ apply fc (IVar fc (UN $ Basic "foldMap"))
 286 |       (foldMapFun ((False <$ guard isMutual) <|> assert <|> Just True) sp rec f Nothing
 287 |        :: toList t)
 288 |   foldMapFun assert (FIBifold _ _ sp1 (Left sp2)) rec f t
 289 |     = apply fc (IVar fc (UN $ Basic "bifoldMap"))
 290 |       (foldMapFun (assert <|> Just True) sp1 rec f Nothing
 291 |       :: foldMapFun (assert <|> Just True) sp2 rec f Nothing
 292 |       :: toList t)
 293 |   foldMapFun assert (FIBifold _ _ sp (Right _)) rec f t
 294 |     = apply fc (IVar fc (UN $ Basic "bifoldMapFst"))
 295 |       (foldMapFun (assert <|> Just True) sp rec f Nothing
 296 |       :: toList t)
 297 |   foldMapFun assert (FIFree y) rec f t = `(mempty)
 298 | 
 299 | ------------------------------------------------------------------------------
 300 | -- User-facing: Foldable deriving
 301 | 
 302 | namespace Foldable
 303 | 
 304 |   derive' : (Elaboration m, MonadError Error m) =>
 305 |             {default Private vis : Visibility} ->
 306 |             {default Total treq : TotalReq} ->
 307 |             {default [] mutualWith : List Name} ->
 308 |             m (Foldable f)
 309 |   derive' = do
 310 | 
 311 |     -- expand the mutualwith names to have the internal, fully qualified, names
 312 |     mutualWith <- map concat $ for mutualWith $ \ nm => do
 313 |                     ntys <- getType nm
 314 |                     pure (fst <$> ntys)
 315 | 
 316 |     -- The goal should have the shape (Foldable t)
 317 |     Just (IApp _ (IVar _ foldable) t) <- goal
 318 |       | _ => throwError InvalidGoal
 319 |     when (`{Prelude.Interfaces.Foldable} /= foldable) $
 320 |       logMsg "derive.foldable" 1 "Expected to derive Foldable but got \{show foldable}"
 321 | 
 322 |     -- t should be a type constructor
 323 |     logMsg "derive.foldable" 1 "Deriving Foldable for \{showPrec App $ mapTTImp cleanup t}"
 324 |     MkIsType f params cs <- isType t
 325 |     logMsg "derive.foldable.constructors" 1 $
 326 |       joinBy "\n" $ "" :: map (\ (n, ty) => "  \{showPrefix True $ dropNS n} : \{show $ mapTTImp cleanup ty}") cs
 327 | 
 328 |     -- Generate a clause for each data constructor
 329 |     let fc = emptyFC
 330 |     let un = UN . Basic
 331 |     let foldMapName = un ("foldMap" ++ show (dropNS f))
 332 |     let funName = un "f"
 333 |     let fun  = IVar fc funName
 334 |     (ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
 335 |       withError (WhenCheckingConstructor cName) $ do
 336 |         -- Grab the types of the constructor's explicit arguments
 337 |         let Just (MkConstructorView (paraz :< (para, _)) args) = constructorView ty
 338 |               | _ => throwError ConfusingReturnType
 339 |         let paras = paraz <>> []
 340 |         logMsg "derive.foldable.clauses" 10 $
 341 |           "\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
 342 |         let vars = map (map (IVar fc . un . ("x" ++) . show . (`minus` 1)))
 343 |                  $ zipWith (<$) [1..length args] (map snd args)
 344 |         recs <- for (zip vars args) $ \ (v, (rig, arg)) => do
 345 |                   res <- withError (WhenCheckingArg (mapTTImp cleanup (unArg arg))) $ do
 346 |                            res <- typeView f paras para (unArg arg)
 347 |                            case res of
 348 |                              Left _ => case rig of
 349 |                                MW => pure ()
 350 |                                _ => throwError (NotAnUnconstrainedValue rig)
 351 |                              _ => pure ()
 352 |                            pure res
 353 |                   pure $ case res of
 354 |                     Left sp => -- do not bother with assert_total if you're generating
 355 |                                -- a covering/partial definition
 356 |                                let useTot = False <$ guard (treq /= Total) in
 357 |                                Just (v, Just (foldMapFun fc mutualWith useTot sp foldMapName funName (Just $ unArg v)))
 358 |                     Right free => do ignore $ isExplicit v
 359 |                                      Just (v, Nothing)
 360 |         let (vars, recs) = unzip (catMaybes recs)
 361 |         pure $ PatClause fc
 362 |           (apply fc (IVar fc foldMapName) [ fun, apply (IVar fc cName) vars])
 363 |           (case catMaybes recs of
 364 |              [] => `(neutral)
 365 |              (x :: xs) => foldr1 (\v, vs => `(~(v) <+> ~(vs))) (x ::: xs))
 366 | 
 367 |     -- Generate the type of the mapping function
 368 |     let paramNames = unArg . fst <$> params
 369 |     let a = un $ freshName paramNames "a"
 370 |     let b = un $ freshName paramNames "b"
 371 |     let va = IVar fc a
 372 |     let vb = IVar fc b
 373 |     let ty = MkTy fc (NoFC foldMapName) $ withParams fc (paramConstraints ns) params
 374 |            $ IPi fc M0 ImplicitArg (Just a) (IType fc)
 375 |            $ IPi fc M0 ImplicitArg (Just b) (IType fc)
 376 |            $ `(Monoid ~(vb) => (~(va) -> ~(vb)) -> ~(t) ~(va) -> ~(vb))
 377 |     logMsg "derive.foldable.clauses" 1 $
 378 |       joinBy "\n" ("" :: ("  " ++ show (mapITy cleanup ty))
 379 |                       :: map (("  " ++) . showClause InDecl . mapClause cleanup) cls)
 380 | 
 381 |     -- Define the instance
 382 |     check $ ILocal fc
 383 |       [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
 384 |       , IDef fc foldMapName cls
 385 |       ] `(fromFoldMap ~(t) ~(IVar fc foldMapName))
 386 | 
 387 |   ||| Derive an implementation of Foldable for a type constructor.
 388 |   ||| This can be used like so:
 389 |   ||| ```
 390 |   ||| data Tree a = Leaf a | Node (Tree a) (Tree a)
 391 |   ||| treeFoldable : Foldable Tree
 392 |   ||| treeFoldable = %runElab derive
 393 |   ||| ```
 394 |   export
 395 |   derive : {default Private vis : Visibility} ->
 396 |            {default Total treq : TotalReq} ->
 397 |            {default [] mutualWith : List Name} ->
 398 |            Elab (Foldable f)
 399 |   derive = do
 400 |     res <- runEitherT {e = Error, m = Elab} (derive' {vis, treq, mutualWith})
 401 |     case res of
 402 |       Left err => fail (show err)
 403 |       Right prf => pure prf
 404 |