removing explicit recursion by replacing catamorphism-CodePudding

I have this AST data structure

data AST = Integer Int
         | Let String AST AST
         | Plus AST AST
         | Minus AST AST
         | Times AST AST
         | Variable String
         | Boolean Bool
         | If AST AST AST
         | Lambda String AST Type Type
         | Application AST AST
         | And AST AST
         | Or AST AST
         | Quot AST AST
         | Rem AST AST
         | Negate AST
         | Eq AST AST
         | Leq AST AST
         | Geq AST AST
         | Neq AST AST
         | Lt AST AST
         | Gt AST AST

and this evaluation code:

eval :: AST -> AST
eval = cata go where
    go :: ASTF (AST) -> AST
    go (LetF var e e') = eval $ substVar (var, e) e'
    go (PlusF (Integer n) (Integer m)) = Integer (n   m)
    go (MinusF (Integer n) (Integer m)) = Integer (n - m)
    go (TimesF (Integer n) (Integer m)) = Integer (n * m)
    go (QuotF (Integer n) (Integer m)) = Integer (quot n m)
    go (RemF (Integer n) (Integer m)) = Integer (rem n m)
    go (IfF (Boolean b) e e') = if b then e else e'
    go (ApplicationF (Lambda var e _ _) e') = eval $ substVar (var, e') e
    go (AndF (Boolean b) (Boolean b')) = Boolean (b && b')
    go (OrF (Boolean b) (Boolean b')) = Boolean (b || b')
    go (NegateF (Boolean b)) = Boolean (not b)
    go (EqF e e') = Boolean (e == e')
    go (NeqF e e') = Boolean (e /= e')
    go (LeqF (Integer n) (Integer m)) = Boolean (n <= m)
    go (GeqF (Integer n) (Integer m)) = Boolean (n >= m)
    go (LtF (Integer n) (Integer m)) = Boolean (n < m)
    go (GtF (Integer n) (Integer m)) = Boolean (n > m)
    go astf = embed astf

I feel like there should be away to remove the explicit recursion for 'let' and application, but I'm not sure exactly which recursion scheme I should reach for. Which recursion scheme(s) can be used to remove recursion in this case and similar cases and do you have any good ways of identifying situations where said recursion scheme is applicable?

CodePudding user response：

eval isn't directly expressible as a catamorphism because eval (Let x e e') applies eval to subst (x, eval e) e', which is not a subterm of Let x e e' (e or e'). Instead, consider the composition of eval and substitution. If you generalize substitution subst to substitute many variables at once with substs, then you can get the following equation:

(eval . substs s) (Let x e e')
= eval (Let x (substs s e) (substs s e'))
= (eval . subst (x, (eval . substs s) e) . substs s) e'

-- by (subst xe . substs s) = substs (xe : s)

= (eval . substs ((x, (eval . substs s) e) : s)) e'

where we do have a function of the form (eval . substs _) applied to both subterms e and e'. In order to account for the parameter of substs, you can use cata with an F-algebra where the carrier is a function ASTF (Sub -> AST) -> Sub -> AST, then you get to pass a different substitution Sub to each subterm.

{-# LANGUAGE TemplateHaskell, TypeFamilies #-}

import Data.Functor.Foldable (cata)
import Data.Functor.Foldable.TH (makeBaseFunctor)
import Data.Maybe (fromJust)

type Id = String
data AST
  = Let Id AST AST
  | Var Id
  | Int Int
  | Plus AST AST

type Sub = [(Id, AST)]

makeBaseFunctor ''AST

evalSubsts :: AST -> Sub -> AST
evalSubsts = cata go where
  go (LetF x e e') s = e' ((x, e s) : s)
  go (VarF x) s = fromJust (lookup x s)
  go (IntF n) _ = Int n
  go (PlusF e e') s =
    let (Int n, Int m) = (e s, e' s) in
    Int (n   m)
  -- Or this:
  -- go (PlusF e e') = liftA2 plus e e'
  --   where plus (Int n) (Int m) = Int (n   m)

eval :: AST -> AST
eval e = evalSubsts e []

Another way to think of evalSubsts is as an evaluator using an environment, mapping variables to values. Then to bind a variable, rather than to do a substitution, is just to insert its value in the environment, which gets looked up once you reach a Var node.

CodePudding user response：

Continuing on the evalSubsts approach from @li-yao-xia, let's try to add lambdas and applications to our language. We start by extending AST:

data AST
  ...
  | Lam Id AST
  | App AST AST

But, how do we write our LamF case in evalSubst?

  go (LamF x e) s = ???

We want our lambdas to be statically (lexically) scoped, so we need to keep around the environment s, but we also can't possibly apply an environment to e yet because we don't know what the value for x should be. We're in a bind!

The solution here is to recognize that, while AST is a great representation for our input, it is not a great representation for the output. Indeed, it's a bit of a coincidence that input Ints and output Ints both happen to share the same structure, and for lambdas, perhaps they shouldn't. So, we can make a new output representation:

data Val
  = IntV Int
  | LamV (Val -> Val)

type Sub = [(Id, Val)]

The key here is that LamV is a function, not simply some data. With this, we can finish our definition of evalSubsts:

evalSubsts :: AST -> Sub -> Val
evalSubsts = cata go where
  go (LetF x e e') s = e' ((x, e s) : s)
  go (VarF x) s = fromJust (lookup x s)
  go (IntF n) _ = IntV n
  go (LamF x e) s = LamV $ \xVal -> e ((x, xVal) : s)
  go (AppF lam e) s =
    let (LamV f) = lam s in f (e s)
  go (PlusF e e') s =
    let (IntV n, IntV m) = (e s, e' s) in
    IntV (n   m)