As you might have guessed, the Reader is also quite effective at
type checking. What is particularly interesting is the similarly
between the type checker and evaluator.
For completeness, the context type is defined as a list of string/type pairs:
type Cont = [(String,FBAETy)]
lookupVarTy = lookup
addVarTy :: String -> FBAETy -> Cont -> Cont
addVarTy s i e = (s,i):e
The signature for our new type inference function is roughly the same as the evaluator, except that we return a Reader that encapsulates types. We will still need to use runR to evaluate the result of called typeofM:
typeofM :: FBAE -> Reader Cont FBAETy
The type of number constants is simply TNum. Just return it:
typeofM (Num n) = return TNum
The binary operations on numbers are identical modulo error messages. Both find the types of their arguments and make sure both are numbers. If they are, return TNum as the type of the operation. If not, throw an error:
typeofM (Plus l r) = do
l' <- (typeofM l)
r' <- (typeofM r)
return (if (l'==TNum && r'==TNum) then TNum else error "Type error in +")
typeofM (Minus l r) = do
l' <- (typeofM l)
r' <- (typeofM r)
return (if (l'==TNum && r'==TNum) then TNum else error "Type error in -")
bind adds bindings to the context when type checking. typeofM uses the Reader to pass along the context rather than the environment, but the operations are almost identical. typeofM for bind first uses ask to get the current context. It calculates the type of the identifier being added, and then uses local in the same way as evalM to add the binding to the local context:
typeofM (Bind i v b) = do
con <- ask
v' <- typeofM v
local (addVarTy i v') (typeofM b)
To perform static type checking, we need to use the lambda variant that carries a type for its argument. (i,t) is added to the context and typeofM b used to get r', the range type, that is the typeof the function body. The type of the Lambda becomes (TFun t r'):
typeofM (Lambda i t b) = do
r' <- local (addVarTy i t) (typeofM b)
return (TFun t r')
The App case uses typeofM to get the type of the function and its argument. The function type provides the domain and range of the associated function. If the type of the argument is the domain type, then the app is the range type. If they do not match, then typeofM throws an error. The if expression is where all the work for this function is performed:
typeofM (App f v) = do
(TFun i b) <- typeofM f
v' <- typeofM v
return (if i==v' then b else error "Type Error in app")
Finally finding the type of an identifier is simply looking it up on the context. ask returns the context, a lookup is performed, and either a type is returned or an error message is thrown:
typeofM (Id id) = do
ask >>= \env -> return (case (lookupVarTy id env) of
Just x -> x
Nothing -> error "Variable not found")
Like other functions, we can made the monadic version look like a traditional version with a quick definition:
typeof x = runR (typeofM x) []
The Reader is an exceptionally powerful and useful programming pattern. Utility functions like ask, asks, and local are just few samples of what kinds of operations can be defined on the environment. Even the function useClosure could be rewritten as a custom operation rather than using local:
explicit :: e -> Reader t a -> Reader e a
explicit e r = return (runR r e)
In our work thus far we have used our own Reader. The standard Haskell libraries contain a Reader implementation. However, when learning how to use the Reader it is far better to have visibility into the implementation than simply try to use the Reader interface. Monad type signatures are not enough to understand their utility.
It is worth spending time with a good Haskell tutorial and learning the Reader well.