How do you express calculations that recursively descend from a tree and maintain a new local state on each split?

Question

Context

The question in the title is actually the general version of the specific problem that I have. Feel free to answer a general question or this specific question below.

I am implementing some function that traverses the purely untyped AST lambda calculus and replaces variables with the De-Bruijn indices. There are two AST representations, external (with variable names) and internal (with indexes):

type Id = String data TermEx = VarE Id | LamE Id TermEx | AppE TermEx TermEx data TermIn = VarI Int | LamI TermIn | AppI TermIn TermIn 

A quick overview of how De-Bruijn indexing works on page 6 of this pdf:

http://ttic.uchicago.edu/~pl/classes/CMSC336-Winter08/lectures/lec4.pdf

Current solution

A regular recursive function that does what I want:

 encode' :: TermEx -> TermIn encode' = go [] where go en te = case te of VarE x -> case elemIndex x en of Just i -> VarI LamE xt -> LamI $ go (x:en) t AppE tt' -> AppI (go en t) (go en t') -- * see comment below 

Comment: The AppI annotation function application is a split in the AST, and each split creates a new “local” state.

Question

Ideally, I want to describe this as some kind of monadic calculation that keeps track of a new local state every time an AST breaks up, my first attempt:

 type DeBruijn = forall m. (Monad m, Functor m) => StateT [Id] m TermIn 

does not work, since all branches will share the same state, discarding the index. So, how do you describe this apparently very general calculation scheme?

Answer 1

You need a converter to read the monad :

 import Control.Monad.Trans.Reader import Control.Applicative import Data.Maybe import Data.List type DeBruijnT = ReaderT [Id] encode :: (Applicative m, Monad m) => TermEx -> DeBrujinT m TermIn encode t = case t of VarE x -> reader (maybe (error "!") VarI . elemIndex x) LamE xt -> withReaderT (x:) $ LamI <$> encode t AppE tt' -> AppI <$> encode t <*> encode t' 

Here withReaderT performs its calculation (2nd argument) in the local environment, which is the result of applying the 1st argument to the current environment, so when new bindings are introduced in the branches after separation, they will not randomly work in the same environment.

In addition, if you really want to create new environments for partitions only and save the old ones in new representations of variables, you can use the state monad transformer in this way:

 type DeBruijnT = StateT [Id] encode :: (Applicative m, Monad m) => TermEx -> DeBruijnT m TermIn encode t = case t of VarE x -> gets (maybe (error "!") VarI . elemIndex x) LamE xt -> withStateT (x:) $ LamI <$> encode t AppE tt' -> do s <- get AppI <$> lift (evalStateT (encode t ) s) <*> lift (evalStateT (encode t') s) 

Here, instead of linking subcomplexes in split mode to the current monadic stream, new monadic flows are generated and calculated with the current state.