Documentation

Define our own Exception datatype to be able to redefine the Applicative interface

Throw a type checking Error

Declaration of type checking errors. An error will (usually) be created using the helper function throwError. As an example:

throwError $ DuplicateClassError (Name "Foo")

throws an error that indicates that the class is defined multiple times.

Declaration of a type checking errors

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.

Generates an empty environment.

Helper function to lookup a class given a Name and an Env. For example:

typecheck env (ClassType c) = do
  _ <- lookupClass env c
  return $ ClassType c

Look up a field by its Type and Name in the Env, returning an error indicating whether the field was found or not.

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

Look up a variable by its Name in the Env, returning an exception with the type checking error, TCError, or the Type of the variable 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 a list of errors 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 a list of errors 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.

Class definition for didactic purposes. This AST represents the following class, which is named C, contains an immutable field f of type Foo:

class C:
  val f: Foo

This class is ill-typed, as there is no declaration of Foo anywhere. To check how to type checker catches this error, run:

tcProgram (Program [testClass1])

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