Deriving.Functor


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