From d17685a92140e192e263230468ffaf88f7e18a75 Mon Sep 17 00:00:00 2001 From: Paul Chiusano Date: Tue, 24 Feb 2015 20:00:31 -0500 Subject: [PATCH] Node code compiling with debruijn-indexed terms --- node/src/Main.hs | 8 +- node/src/Unison/Edit/Term.hs | 94 ++++++------- node/src/Unison/Edit/Term/Eval/Interpreter.hs | 2 +- node/src/Unison/Edit/Term/Path.hs | 58 ++++---- node/src/Unison/Syntax/Term.hs | 124 +++++++++--------- node/src/Unison/Type/Context.hs | 6 +- 6 files changed, 153 insertions(+), 139 deletions(-) diff --git a/node/src/Main.hs b/node/src/Main.hs index 44eacd10d..cd197ee61 100644 --- a/node/src/Main.hs +++ b/node/src/Main.hs @@ -8,15 +8,13 @@ import Unison.Note as N import Unison.Syntax.Var as V identity :: E.Term -identity = E.lam1 $ \x -> x - -(@) = E.App +identity = E.unscope (E.lam E.var) constant :: E.Term -constant = E.lam2 $ \x y -> x +constant = E.unscope (E.lam (E.lam (E.weaken E.var))) apply :: E.Term -apply = E.lam2 $ \f x -> f `E.App` x +apply = E.unscope (E.lam (E.lam (E.weaken E.var `E.app` E.var))) -- type Any = forall r . (forall a . a -> r) -> r anyT :: Type diff --git a/node/src/Unison/Edit/Term.hs b/node/src/Unison/Edit/Term.hs index d408da3c1..13da61ee3 100644 --- a/node/src/Unison/Edit/Term.hs +++ b/node/src/Unison/Edit/Term.hs @@ -39,8 +39,7 @@ invalid loc ctx = "invalid path " ++ show loc ++ " in:\n" ++ show ctx -- todo: if the location references any free variables, make these -- function parameters of the abstract :: Applicative f => P.Path -> E.Term -> Noted f E.Term -abstract loc ctx = - N.liftMaybe (invalid loc ctx) $ E.lam1 <$> P.set' loc ctx +abstract loc ctx = N.failure "todo: Edit.Term.abstract" -- | Compute the allowed type of a replacement for a given subterm. -- Example, in @\g -> map g [1,2,3]@, @g@ has an admissible type of @@ -55,11 +54,10 @@ admissibleTypeOf :: Applicative f -> P.Path -> E.Term -> Noted f T.Type -admissibleTypeOf synthLit loc ctx = case P.at' loc ctx of +admissibleTypeOf synthLit loc ctx = case P.introduceAt1' loc E.app ctx of Nothing -> N.failure $ invalid loc ctx - Just (sub,replace) -> - let ctx = E.lam1 $ \f -> replace (f `E.App` sub) - go (T.Arrow (T.Arrow _ tsub) _) = tsub + Just ctx -> + let go (T.Arrow (T.Arrow _ tsub) _) = tsub go (T.Forall n t) = T.Forall n (go t) go _ = error "impossible, f had better be a function" in (T.gc . go) <$> synthesize synthLit ctx @@ -96,31 +94,34 @@ eta loc ctx = -- This function returns a path to the floated subexpression (@42@ and @f x@ in -- the above examples.) letFloat :: Applicative f => P.Path -> E.Term -> Noted f (E.Term, P.Path) -letFloat loc ctx = case P.at loc ctx of - Nothing -> N.failure $ invalid loc ctx - Just sub -> - let - free = E.freeVars sub - minVar = if S.null free then Nothing else Just (S.findMin free) - trimmedPath = P.trimToV minVar loc - remainderPath = P.Path $ drop (length . P.elements $ trimmedPath) (P.elements loc) - letBody = do - body <- P.at trimmedPath ctx - E.lam1 <$> P.set' remainderPath body - in - N.liftMaybe (invalid loc ctx) $ do - body <- letBody - ctx' <- P.set trimmedPath (body `E.App` sub) ctx - loc' <- pure $ P.extend P.Arg trimmedPath - pure (ctx', loc') +letFloat loc ctx = N.failure "Term.letFloat todo" + +--case P.at loc ctx of +-- Nothing -> N.failure $ invalid loc ctx +-- Just sub -> +-- let +-- free = E.freeVars sub +-- minVar = if S.null free then Nothing else Just (S.findMin free) +-- trimmedPath = P.trimToV minVar loc +-- remainderPath = P.Path $ drop (length . P.elements $ trimmedPath) (P.elements loc) +-- letBody = do +-- body <- P.at trimmedPath ctx +-- E.lam1 <$> P.set' remainderPath body +-- in +-- N.liftMaybe (invalid loc ctx) $ do +-- body <- letBody +-- ctx' <- P.set trimmedPath (body `E.App` sub) ctx +-- loc' <- pure $ P.extend P.Arg trimmedPath +-- pure (ctx', loc') -- | Return the type of all local variables in scope at the given location locals :: Applicative f => T.Env f -> P.Path -> E.Term -> Noted f [(V.Var, T.Type)] locals synthLit path ctx | E.isClosed ctx = - N.scoped ("locals@"++show path ++ " " ++ show ctx) (filterInScope . pushDown <$> lambdaTypes) + N.scoped ("locals@"++show path ++ " " ++ show ctx) + (filterInScope . label . pushDown <$> lambdaTypes) where pointsToLambda path = case P.at path ctx of - Just (E.Lam _ _) -> True + Just (E.Lam _) -> True _ -> False lambdas :: [P.Path] @@ -133,12 +134,16 @@ locals synthLit path ctx | E.isClosed ctx = -- not sure about this impl, or if it matters -- we prefer type information obtained higher in the syntax tree - pushDown :: [[(V.Var, T.Type)]] -> [(V.Var, T.Type)] + pushDown :: [[T.Type]] -> [T.Type] pushDown [] = [] pushDown (env0 : tl) = env0 ++ pushDown (drop (length env0) tl) - extract :: E.Term -> T.Type -> [(V.Var, T.Type)] - extract (E.Lam n body) (T.Arrow i o) = (n, i) : extract body o + -- todo, not sure this is correct + label :: [T.Type] -> [(V.Var,T.Type)] + label ts = iterate V.succ V.bound1 `zip` reverse ts + + extract :: E.Term -> T.Type -> [T.Type] + extract (E.Lam body) (T.Arrow i o) = i : extract body o extract ctx (T.Forall _ t) = extract ctx t extract _ _ = [] @@ -146,7 +151,7 @@ locals synthLit path ctx | E.isClosed ctx = filterInScope locals = filter (\(v,_) -> S.member v inScope) locals where inScope = S.fromList (P.inScopeAt path ctx) locals _ _ ctx = - N.failure $ "Term.locals: term contains free variables - " ++ show (E.freeVars ctx) + N.failure $ "Term.locals: term contains free variables - " ++ show ctx -- | Produce `e`, `e _`, `e _ _`, `e _ _ _` and so on, -- until the result is no longer a function type @@ -163,20 +168,19 @@ applications e t = e : go e t -- and @map@ will have a type of @forall a b . (a -> b) -> [a] -> [b]@. typeOf :: Applicative f => T.Env f -> P.Path -> E.Term -> Noted f T.Type typeOf synthLit (P.Path []) ctx = N.scoped ("typeOf: " ++ show ctx) $ synthesize synthLit ctx -typeOf synthLit loc ctx = N.scoped ("typeOf@"++show loc ++ " " ++ show ctx) $ case P.at' loc ctx of - Nothing -> N.failure $ invalid loc ctx - Just (sub,replace) -> - let sub' = sub - ctx = E.lam1 $ \f -> replace (ksub f) - -- we annotate `f` as returning `Number` so as not to introduce - -- any new quantified variables in the inferred type - -- copy the subtree so type is unconstrained by local usage - -- problem is that sub may contain variables that need freshening - ksub f = E.lam2 (\x _ -> x) `E.App` sub' `E.App` (f `E.App` sub `E.Ann` T.Unit T.Number) - go (T.Arrow (T.Arrow tsub _) _) = tsub - go (T.Forall n t) = T.Forall n (go t) - go _ = error "impossible, f had better be a function" - in (T.gc . go) <$> synthesize synthLit ctx +typeOf synthLit loc ctx = N.scoped ("typeOf@"++show loc ++ " " ++ show ctx) $ + case P.introduceAt1' loc replace ctx of + Nothing -> N.failure $ invalid loc ctx + Just ctx -> T.gc . extract <$> synthesize synthLit ctx + where + extract (T.Arrow (T.Arrow tsub _) _) = tsub + extract (T.Forall n t) = T.Forall n (extract t) + extract _ = error "impossible, f had better be a function" + k = E.lam (E.lam (E.weaken E.var)) -- `\x y -> x`, in debruijn notation + replace f focus = + -- annotate `f` as returning `Number` just so no new quantifiers are + -- introduced in the inferred type + k `E.app` focus `E.app` (f `E.app` focus `E.ann` T.Unit T.Number) -- | Evaluate the given location to weak head normal form. -- If the location contains any free variables, this noops. @@ -188,5 +192,5 @@ whnf :: Applicative f -> Noted f E.Term whnf eval readTerm loc ctx = case P.at' loc ctx of Nothing -> N.failure $ invalid loc ctx - Just (sub,replace) | S.null (E.freeVars sub) -> replace <$> Eval.whnf eval readTerm sub - Just _ | otherwise -> pure ctx + Just (sub,replace) | E.isClosed sub -> replace <$> Eval.whnf eval readTerm sub + Just _ | otherwise -> pure ctx diff --git a/node/src/Unison/Edit/Term/Eval/Interpreter.hs b/node/src/Unison/Edit/Term/Eval/Interpreter.hs index 6cbe38c63..b26703656 100644 --- a/node/src/Unison/Edit/Term/Eval/Interpreter.hs +++ b/node/src/Unison/Edit/Term/Eval/Interpreter.hs @@ -20,7 +20,7 @@ data Primop f = eval :: (Applicative f, Monad f) => Map R.Reference (Primop f) -> Eval f eval env = Eval step whnf where - reduce e@(E.App (E.Lam _ _) _) args = + reduce e@(E.App (E.Lam _) _) args = return $ Just (foldl E.App (E.betaReduce e) args) reduce (E.App (E.Ref h) x) args = case M.lookup h env of Nothing -> return Nothing diff --git a/node/src/Unison/Edit/Term/Path.hs b/node/src/Unison/Edit/Term/Path.hs index 71f0cbced..a58262498 100644 --- a/node/src/Unison/Edit/Term/Path.hs +++ b/node/src/Unison/Edit/Term/Path.hs @@ -1,5 +1,6 @@ -{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TemplateHaskell #-} module Unison.Edit.Term.Path where @@ -46,7 +47,7 @@ at (Path (h:t)) e = go h e where go Fn (E.App f _) = at (Path t) f go Arg (E.App _ x) = at (Path t) x go _ (E.Ann e' _) = at (Path (h:t)) e' - go Body (E.Lam _ body) = at (Path t) body + go Body (E.Lam body) = at (Path t) body go _ _ = Nothing along :: Path -> E.Term -> [E.Term] @@ -54,29 +55,13 @@ along (Path path) e = go path e where go [] e = [e] go (Fn:path) e@(E.App f _) = e : go path f go (Arg:path) e@(E.App _ arg) = e : go path arg - go (Body:path) e@(E.Lam _ body) = e : go path body + go (Body:path) e@(E.Lam body) = e : go path body go (Index i:path) e@(E.Vector xs) = e : maybe [] (go path) (xs !? i) go _ _ = [] valid :: Path -> E.Term -> Bool valid p e = maybe False (const True) (at p e) --- | If the given @Path@ points to a valid subterm, we replace --- that subterm @e@ with @v e@ and sequence the @Applicative@ effects --- visit :: Path -> Traversal' E.Term E.Term -visit :: Applicative f => Path -> (E.Term -> f E.Term) -> E.Term -> f E.Term -visit (Path []) v e = v e -visit (Path (h:t)) v e = go h e where - go Fn (E.App f arg) = E.App <$> visit (Path t) v f <*> pure arg - go Arg (E.App f arg) = E.App <$> pure f <*> visit (Path t) v arg - go _ (E.Ann e' typ) = E.Ann <$> visit (Path (h:t)) v e' <*> pure typ - go (Index i) e@(E.Vector xs) = let replace xi = E.Vector (xs // [(i,xi)]) - sub = xs !? i - in maybe (pure e) (\sub -> replace <$> visit (Path t) v sub) sub - go Body (E.Lam n body) = fn <$> visit (Path t) v body - where fn body = E.lam1 $ \x -> E.betaReduce (E.Lam n body `E.App` x) - go _ e = pure e - -- | Like 'at', but returns a function which may be used to modify the focus at' :: Path -> E.Term -> Maybe (E.Term, E.Term -> E.Term) at' loc ctx = case at loc ctx of @@ -87,9 +72,10 @@ at' loc ctx = case at loc ctx of inScopeAt :: Path -> E.Term -> [V.Var] inScopeAt p e = let vars = map f (along p e) - f (E.Lam n _) = Just n + f (E.Lam _) = Just () f _ = Nothing - in drop 1 (reverse vars) >>= toList + n = length (drop 1 (reverse vars) >>= toList) + in take n (iterate V.succ V.bound1) set :: Path -> E.Term -> E.Term -> Maybe E.Term set path focus ctx = impl path ctx where @@ -102,7 +88,7 @@ set path focus ctx = impl path ctx where go Fn (E.App f arg) = E.App <$> impl (Path t) f <*> pure arg go Arg (E.App f arg) = E.App f <$> impl (Path t) arg go _ (E.Ann x _) = impl (Path (h:t)) x - go Body (E.Lam n body) = E.Lam n <$> impl (Path t) body + go Body (E.Lam body) = E.Lam <$> impl (Path t) body go _ _ = Nothing -- | Like 'set', but accepts the new focus within the returned @Maybe@. @@ -114,6 +100,34 @@ modify loc f ctx = do x <- at loc ctx set loc (f x) ctx +freeAt :: Path -> V.Var +freeAt path = + let used = length [ Body | Body <- elements path ] + vars = iterate V.succ V.bound1 + in head (drop used vars) + +-- | @introduceAt1 path (\var focus -> ...) ctx@ introduces a +-- new free variable at the given path and makes some edit to +-- the focus using this variable and the current focus. +introduceAt1 :: Path + -> (forall e . E.Scoped e -> E.Scoped e -> E.Scoped e) + -> E.Scoped a + -> Maybe (E.Scoped (Maybe a)) +introduceAt1 path f ctx = do + focus <- E.Scoped <$> at path (E.unscope ctx) + focus' <- pure (f (E.Scoped (E.Var (freeAt path))) focus) + E.Scoped <$> set path (E.unscope focus') (E.unscope ctx) + +-- | Like @introduceAt1@, but takes raw terms, and returns a lambda term +introduceAt1' :: Path + -> (forall e . E.Scoped e -> E.Scoped e -> E.Scoped e) + -> E.Term + -> Maybe E.Term +introduceAt1' path f ctx = do + ctx' <- E.scoped ctx + body <- introduceAt1 path f ctx' + pure (E.unscope (E.lam body)) + -- | Drop from the right of this 'Path' until reaching the given element trimToR :: E -> Path -> Path trimToR e (Path p) = Path . reverse . dropWhile (/= e) . reverse $ p diff --git a/node/src/Unison/Syntax/Term.hs b/node/src/Unison/Syntax/Term.hs index b2b6cd032..542f1f4b1 100644 --- a/node/src/Unison/Syntax/Term.hs +++ b/node/src/Unison/Syntax/Term.hs @@ -7,12 +7,9 @@ module Unison.Syntax.Term where import qualified Data.Foldable as Foldable -import Data.Maybe import Data.Traversable -import Data.List as List import Control.Applicative import Control.Lens.TH -import Control.Monad import Control.Monad.Writer import Data.Aeson.TH import qualified Data.Aeson.Encode as JE @@ -42,7 +39,7 @@ data Term | App Term Term | Ann Term T.Type | Vector (V.Vector Term) - | Lam V.Var Term + | Lam Term deriving (Eq,Ord) instance Show Term where @@ -54,37 +51,12 @@ instance Show Term where show (App f x@(App _ _)) = show f ++ " (" ++ show x ++ ")" show (App f x) = show f ++ " " ++ show x show (Ann x t) = "(" ++ show x ++ " : " ++ show t ++ ")" - show lam@(Lam _ _) = "(" ++ List.intercalate " " (map show vs) ++ " → " ++ show inner ++ ")" + show lam@(Lam _) = "(λ. " ++ show inner ++ ")" where - (vs,inner) = go lam + inner = go lam go v = case v of - Lam n body -> let (vs,inner) = go body in (Var n : vs, inner) - _ -> ([], v) - -maxV :: Term -> V.Var -maxV (App f x) = maxV f `max` maxV x -maxV (Ann x _) = maxV x -maxV (Lam n _) = n -maxV (Vector v) | not (V.null v) = Foldable.foldl max (V.decr V.bound1) (fmap maxV v) -maxV _ = V.decr V.bound1 - -lam1M :: Monad f => (Term -> f Term) -> f Term -lam1M f = return Lam `ap` n `ap` body - where - n = liftM (V.succ . maxV) body - body = f =<< (liftM Var n) - -lam1 :: (Term -> Term) -> Term -lam1 f = Lam n body - where - n = V.succ (maxV body) - body = f (Var n) - -lam2 :: (Term -> Term -> Term) -> Term -lam2 f = lam1 $ \x -> lam1 $ \y -> f x y - -lam3 :: (Term -> Term -> Term -> Term) -> Term -lam3 f = lam1 $ \x -> lam1 $ \y -> lam1 $ \z -> f x y z + Lam body -> go body + _ -> v -- | Convert all 'Ref' constructors to the corresponding term link :: (Applicative f, Monad f) => (H.Hash -> f Term) -> Term -> f Term @@ -97,8 +69,7 @@ link env e = case e of e | otherwise -> link env e App fn arg -> App <$> link env fn <*> link env arg Vector vs -> Vector <$> traverse (link env) vs - Lam n body -> go <$> link env body - where go body = lam1 $ \x -> betaReduce (Lam n body `App` x) + Lam body -> Lam <$> link env body _ -> pure e dependencies :: Term -> S.Set H.Hash @@ -111,8 +82,22 @@ dependencies e = case e of App fn arg -> dependencies fn `S.union` dependencies arg Ann e _ -> dependencies e Vector vs -> Foldable.foldMap dependencies vs - Lam _ body -> dependencies body + Lam body -> dependencies body +isClosed :: Term -> Bool +isClosed e = go V.bound1 e + where + go depth e = case e of + Lit _ -> True + Ref _ -> True + Blank -> True + Var v -> v < depth + App f arg -> go depth f && go depth arg + Ann e _ -> go depth e + Vector vs -> Foldable.all (go depth) vs + Lam body -> go (V.succ depth) body + +{- freeVars :: Term -> S.Set V.Var freeVars e = case e of Var v -> S.singleton v @@ -121,22 +106,38 @@ freeVars e = case e of Lam n body -> S.delete n (freeVars body) Vector vs -> Foldable.foldMap freeVars vs _ -> S.empty +-} -substitute :: (V.Var -> Maybe Term) -> Term -> Term -substitute env e = go S.empty e where - go bound e = case e of - Var v -> if S.member v bound then e else fromMaybe e (env v) - App fn arg -> App (go bound fn) (go bound arg) - Vector vs -> Vector (fmap (go bound) vs) - Lam n body -> Lam n (go (S.insert n bound) body) - _ -> e +newtype Scoped a = Scoped { unscope :: Term } -weaken :: V.Var -> Term -> Term -weaken v e = substitute (\v' -> Just (Var (V.nest v v'))) e +scoped :: Term -> Maybe (Scoped a) +scoped e | isClosed e = Just (Scoped e) +scoped _ = Nothing -isClosed :: Term -> Bool -isClosed e | S.null (freeVars e) = True -isClosed _ = False +lam :: Scoped (Maybe a) -> Scoped a +lam (Scoped body) = Scoped (Lam body) + +var :: Scoped (Maybe a) +var = Scoped (Var V.bound1) + +app :: Scoped a -> Scoped a -> Scoped a +app (Scoped f) (Scoped arg) = Scoped (f `App` arg) + +ann :: Scoped a -> T.Type -> Scoped a +ann (Scoped e) t = Scoped (e `Ann` t) + +weaken :: Scoped a -> Scoped (Maybe a) +weaken (Scoped s) = Scoped (go V.bound1 s) + where + go depth e = case e of + Lit _ -> e + Ref _ -> e + Blank -> e + Var v -> if v >= depth then Var (V.succ v) else e + App f arg -> App (go depth f) (go depth arg) + Ann e t -> Ann (go depth e) t + Vector vs -> Vector (fmap (go depth) vs) + Lam body -> Lam (go (V.succ depth) body) stripAnn :: Term -> (Term, Term -> Term) stripAnn (Ann e t) = (e, \e' -> Ann e' t) @@ -150,27 +151,25 @@ arguments _ = [] -- | If the outermost term is a function application, -- perform substitution of the argument into the body betaReduce :: Term -> Term -betaReduce (App (Lam var f) arg) = go f where - go :: Term -> Term - go body = case body of - App f x -> App (go f) (go x) - Vector vs -> Vector (fmap go vs) - Ann body t -> Ann (go body) t - Lam n body | n == var -> Lam n body -- this lambda shadows var; avoid substituting - | otherwise -> Lam n (go body) - Var v | v == var -> arg +betaReduce (App (Lam f) arg) = go V.bound1 f where + go depth body = case body of + App f x -> App (go depth f) (go depth x) + Vector vs -> Vector (fmap (go depth) vs) + Ann body t -> Ann (go depth body) t + Lam body -> Lam (go (V.succ depth) body) + Var v | v == depth -> arg _ -> body betaReduce e = e -- | If the outermost term is a lambda of the form @\x -> f x@, -- reduce this to @f@. etaReduce :: Term -> Term -etaReduce (Lam n (App f n')) | Var n == n' = f +etaReduce (Lam (App f (Var v))) | v == V.bound1 = f etaReduce e = e --- | Repeatedly apply eta reduction until reaching fixed point +-- | Repeatedly apply @etaReduce@ until reaching fixed point. etaNormalForm :: Term -> Term -etaNormalForm (Lam n (App f n')) | Var n == n' = etaNormalForm f +etaNormalForm (Lam (App f (Var v))) | v == V.bound1 = etaNormalForm f etaNormalForm e = e applyN :: Term -> [Term] -> Term @@ -219,8 +218,7 @@ hashCons e = let (e', hs) = runWriter (go e) in finalize e' hs r@(Ref _) -> pure r v@(Var _) -> pure v Blank -> pure Blank - Lam n body -> go body >>= - \body -> save (lam1 $ \x -> betaReduce (Lam n body `App` x)) + Lam body -> go body >>= (\body -> save (Lam body)) Ann e t -> save =<< (Ann <$> go e <*> pure t) App f x -> save =<< (App <$> go f <*> go x) Vector vs -> save =<< (Vector <$> traverse go vs) diff --git a/node/src/Unison/Type/Context.hs b/node/src/Unison/Type/Context.hs index dec62e8e7..3ae47d1fb 100644 --- a/node/src/Unison/Type/Context.hs +++ b/node/src/Unison/Type/Context.hs @@ -279,7 +279,7 @@ check ctx e t | wellformedType ctx t = scope (show e ++ " : " ++ show t) $ go e let (x', ctx') = extendUniversal ctx in check ctx' e (T.subst body x (T.Universal x')) >>= retract (E.Universal x') - go fn@(Term.Lam _ _) (T.Arrow i o) = -- =>I + go fn@(Term.Lam _) (T.Arrow i o) = -- =>I let x' = fresh ctx v = Term.Var x' ctx' = extend (E.Ann x' i) ctx @@ -314,7 +314,7 @@ synthesize ctx e = scope ("infer: " ++ show e) $ go e where go (Term.App f arg) = do -- ->E (ft, ctx') <- synthesize ctx f synthesizeApp ctx' (apply ctx' ft) arg - go fn@(Term.Lam _ _) = -- ->I=> (Full Damas Milner rule) + go fn@(Term.Lam _) = -- ->I=> (Full Damas Milner rule) let (arg, i, o) = fresh3 ctx ctxTl = context [E.Marker i, E.Existential i, E.Existential o, E.Ann arg (T.Existential i)] @@ -363,6 +363,6 @@ synthesizeClosed synthRef term = Noted $ synth <$> N.unnote (annotate term) Term.Ref h -> Term.Ann (Term.Ref h) <$> synthRef h Term.App f arg -> Term.App <$> annotate f <*> annotate arg Term.Ann body t -> Term.Ann <$> annotate body <*> pure t - Term.Lam n body -> Term.Lam n <$> annotate body + Term.Lam body -> Term.Lam <$> annotate body Term.Vector terms -> Term.Vector <$> traverse annotate terms _ -> pure term'