The type checking monad. The type checking monad is the stacking of the Reader and Exception monads.

Declaration of type checking errors.

Data declaration of available errors. Value constructors are used to create statically known errors. For example:

UnknownClassError  (Name c)

creates a UnknownClassError. This error should be created whenever there is a class whose declaration is unknown or inexistent.

Returns a type checking monad, containing the error err. A common example throughout the code is the following:

tcError $ UnknownClassError c

The code above throws an error because the class c was not found in the environment Env.

Environment. The Env is used during type checking, and is updated as the type checker runs. Most likely, one uses the Reader monad to hide details of how the environment is updated, via the common local function.

Conditionally update the environment to track if we are in a constructor method.

Generates an empty environment.

Helper function to lookup a class given a Name and an Env. Usually it relies on the Reader monad, so that passing the Env can be omitted. For example:

findClass :: Type -> TypecheckM ClassDef
findClass ty@(ClassType c) = do
  cls <- asks $ lookupClass c
  case cls of
    Just cdef -> return cdef
    Nothing -> tcError $ UnknownClassError c
findClass ty = tcError $ NonClassTypeError ty

In this function (findClass), the Reader function asks injects the Reader monad as the last argument. More details in the paper.

Look up a variable by its Name in the Env, returning an option type indicating whether the variable was found or not.

Find a class declaration by its Type

Find a method declaration by its Type and method name m

Find a field declaration by its Type (ty) and field name f

Find a variable in the environment by its name x

Generates an environment (symbol's table) from a Program,

Add a variable name and its type to the environment Env.

Add a list of parameters, Param, to the environment.

Main entry point of the type checker. This function type checks an AST returning either an error or a well-typed program. For instance, assuming the following made up language: > > class C > val f: Foo >

it should be parsed to generate the following AST:

testClass1 =
 ClassDef {cname = "C"
          ,fields = [FieldDef {fmod = Val, fname = "f", ftype = ClassType "Foo"}]
          ,methods = []}

To type check the AST, run the tcProgram combinator as follows:

tcProgram testClass1

which either returns an error or the resulting typed AST.

The type class defines how to type check an AST node.

This combinator is used whenever a certain type is expected. This function is quite important. Here follows an example:

doTypecheck mdef@(MethodDef {mparams, mbody, mtype}) = do
  -- typecheck the well-formedness of types of method parameters
  mparams' <- mapM typecheck mparams
  mtype' <- typecheck mtype

  -- extend environment with method parameters and typecheck body
  mbody' <- local (addParameters mparams) $ hasType mbody mtype'
  ...

in the last line, because we are type checking a method declaration, it is statically known what should be the return type of the function body. In these cases, one should use the hasType combinator.

Test programs of a class with a single field. This program is the AST equivalent of the following syntax:

class C
  val f: Foo

Test program with a class, field, method, and variable access. The class Bar does not exist in the environment. The variable access is unbound.

This program is the AST equivalent of the following syntax:

class D
  val g: Bar
  def m(): Int
    x

Test program with a two classes, field, method, and variable access. The class declaration are duplicated.

This program is the AST equivalent of the following syntax:

class D
  val g: Bar
  def m(): Int
    x

class D
  val g: Bar
  def m(): Int
    x

Test suite that runs testProgram.