If you are writing an interpreter, odds are you will want to bind variables. If you are binding variables, there is a decent chance you will want to locally scope your variables.
For tracking your bindings, your first thought might be to reach for the State
monad. Unfortunately it will get you a global binding context and many tears.
It sure would be a shame of x
in the function f
was bound over the globally scoped x
:
let x = 0;
let f = (x) => x + 1;
f(5) > x;
Luckily there is a really neat trick using the Reader
monad to get local scoping for free.
Lets say we want to write a typechecker for a minimal Simply Typed Lambda Calculus. Our Types will look like:
data Term = Var String
| Abs String Type Term
| App Term Term
data Type = Type :-> Type | UnitT | BoolT
deriving Eq
Term
is our Term AST, Type
is our types. In this calculus all we can construct are functions that take functions as arguments.
Now for our typechecker we want to traverse the AST, collecting all our bindings and their types as we pass over Lambda terms (Abs
) and then return the type of the entire expression.
We will our save our types in the typing context which we call Context
:
type Context = [(String, Type)]
Context
is a mapping from binder to Type
.
Each time we pass through a Lambda term we must create a new local context with everything above that Lambda term plus the new local binding.
An ill typed term should terminate the typechecker and throw an error. For this we use ExceptT
.
For managing our Context
I already revealed that we will use Reader
. This may still seem like an unusual choice, but as we will see, it is in fact the ideal candidate for local state.
Our final Typechecking Monad is thus:
type Context = [(String, Type)]
data TypeErr = TypeError
deriving (Show, Eq)
newtype TypecheckM a =
TypecheckM { unTypecheckM :: ExceptT TypeErr (Reader Context) a }
deriving (Functor, Applicative, Monad, MonadReader Context, MonadError TypeErr)
In general we know that what we want to do is traverse an AST and build up the type of the expression represnted by the AST. If at any point the type of the AST (or a supexpression of the AST) violates our typing judgements then we have a type error and abort the traversal.
Our typechecker is a functon Term -> TypecheckM Type
. The implementation will amount to a giant case statement with some monadic effects for throwing errors and accumulating the typing context.
Our minimal calculus conssists soley of Lambda terms (Abs
), variables (Var
), and function application App
.
In plain english, our typing rules are as follows:
Context
and return it. If the binder does not exist in Context
then throw a type error.T1 :-> T2
where the second sub term is of type T1
, then return T2
.T : T1
in context, then typecheck the body of the Lambda. The type of the Abs
term is T1 :-> T2
where the body is of type T2
.typecheck :: Term -> TypecheckM Type
= \case
typecheck Var x -> do
<- asks $ lookup x
ty maybe (throwError TypeError) pure ty
Abs bndr ty1 trm -> do
<- local ((bndr, ty1) :) (typecheck trm)
ty2 pure $ ty1 :-> ty2
App t1 t2 -> do
<- typecheck t1
ty1 case ty1 of
:-> tyB -> do
tyA <- typecheck t2
ty2 if tyA == ty2 then pure tyB else throwError TypeError
-> throwError TypeError _
The Reader
trick happens in the Abs
case where we introduce a new binder. Notice the use of local :: MonadReader r m => (r -> r) -> m a
-> m a
. This function allows us to create a new local Reader
context using an r -> r
function and the current context r
.
In our case r
is Context
and our r -> r
function simply cons's the new binder and its type onto our Context
. This little one liner allows us to create a brand new scope every time we recurse through a Lambda term. We don't need to do anything complicated to track the scope of our bindings at all. Pretty neat. :)