Typechecker

[yc2454]

Untested type checker. Might need a lot more debugging.

Pending tasks:

1. testing the type checker
2. create an environment to store the variables etc.

[Rewbert]

I can give some general tips if it's of interest:

A nice monad transformer stack for type checking:

import Control.Monad.Reader  -- Reader for context
import Control.Monad.Except  -- Except for error handling (synonymous with manually throwing around Either e a, as you are doing now)

type TC a = ReaderT Context (Except TypeError) a

runTC :: TC a -> Either TypeError a
runTC tca = runExcept $ runReaderT tca context
  where
    context = -- some initial context containing the procedure signatures --

I like using Reader instead of State for type checking because we then don't need to worry about restoring the state once we leave a scope. The reader monad takes care of that with local.

We need some type of errors:

data TypeError = UnboundVariable Ident   -- ^ variable @Ident@ is not ins cope
               | TypeError SSMExp t1 t2  -- ^ The expression failed to type check, found t1 when t2 was expected
               -- more variants as needed

When you type check a language like this, you need to (as you point out yourself) maintain a context that gives you access to the types of any identifiers in scope. This context really consists of two parts - that which does not change (function signatures) and that which is dynamic (identifiers in scope).

import qualified Data.Map as Map

data Context = Context { procedures :: Map Ident Type  -- ^ types of procedures
                       , scopes     :: [Map Ident Type]  -- ^ types of variables (head of this list is the youngest scope)
                       }

lookupProcedure :: Ident -> TC Type
lookupProcedure id = do
  e <- ask
  case Map.lookup id (procedures e) of
    Just t -> return t
    Nothing -> throwError $ UnboundVariable id

{- | Look up the type of a variable. As our language has scopes (e.g if-branches & while loops), we must
dig through all the scopes to search for a type for the variable. We allow shadowing variables, so we start
looking for the type in the youngest scope and work our way towards the oldest. If no scope contains the variable,
it is clearly unbound and we encountered an error. -}
lookupVar :: Ident -> TC Type
lookupVar id = do
  e <- ask
  lookupVar' id (scopes e)
  where
    lookupVar' :: Ident -> [Map Ident Type] -> TC Type
    lookupVar' id [] = throwError $ UnboundVariable id
    lookupVar' id (c:cs) = case Map.lookup id c of
      Just t -> return t
      Nothing -> lookupVar' id xs

We also need some way of extending this environment with additional type information. We also want to be very clear with the lifetime of this variable, so we include a computation that the variable should remain alive for.

withVar :: Ident -> Type -> TC a -> TC a
withVar id t tca = local (\c -> c { withVar' id t (scopes e) }) tca
  where
    withVar' :: Ident -> Type -> [Map Ident Type] -> [Map Ident Type]
    withVar' id t (c:cs) = Map.insert id t c : cs

Now when we are type checking a procedure body, e.g, I would type check NewRef like this:

assertType :: SSMExp -> Type -> Type -> TC ()
assertType e t1 t2 =
  if t1 == t2
    then return ()
    else throwError $ TypeError e t1 t2

stmts :: [Stmt] -> TC ()
stmts (x:xs) = case x of
  NewRef id t e -> do
    t' <- checkExp e -- typecheck e
    assertType e t' t -- check that the type of the expression is the one we expect it to be (t)
    withVar id t' $ stmts xs -- here we say to call @stmts xs@ with the extended environment
    -- but here, after that call returned, the environment is just as it was before! :)

The final crux is scoping. If we are type checking a while-statement, the body of the while should be evaluated in a new scope. Any local variables must be removed from the typing context when we leave the while. local seems like just the thing!

-- | perform a computation with a new scope in the context. Context is restored once the computation terminates.
withNewScope :: TC a -> TC a
withNewScope tca = local (\c -> c { scopes = Map.empty : (scopes s) }) tca

stmts :: [Stmt] -> TC ()
stmts (x:xs) = case x of
  If c thn els -> do
    t <- checkExp c
    assertType c t TBool
    withNewScope $ stmts thn
    withNewScope $ stmts els

If I were to write the type checker I think I would take an approach like this one. It is possible to use State instead of Reader, but it comes with some extra care needed to make sure the state is restored after scoped computations, etc. Maybe there are some issues in my code above (I only wrote it here, I didn't type check it), but it should be mostly correct I hope.

I think writing a type checker for a language like ours (no polymorphic types etc, which makes checking quite straightforward) is a good exercise to get comfortable with monads. It was for me when I took a course in programming language technology :)