Type checking monad

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

The function <:> takes two Either monads and returns an error if one of them is an error or aggregates both results. For example:

let error = Left "Error" <:> Right 42
let errors = Left "Error" <:> Left "Error2"
let valid = Right "42" <:> Right "0"

evaluates error = Left Error, errors = Left ErrorError2, and valid = 420.

Forks two computations in the Except monad, and either returns both of their results, or aggregates the errors of one or both of the computations. For example:

    (fields', methods') <- forkM precheck fields <&>
                           forkM precheck methods

In this example, if the evaluation of forkM precheck fields and and forkM precheck methods return errors, we aggregate them using <:>. If only one of them fails, then return the single error. If both computation succeed, return a monad wrapped around the tuple with both results.

Allows typechecking a list of items, collecting error messages from all of them.

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

tcError $ DuplicateClassError (Name "Foo")

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

Declaration of a type checking error, where Error represents the current type checking error and Backtrace the up-to-date backtrace.

Declaration of a type checking warnings in TCWarning.

Available warnings in Warning.

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.

Returns a type checking monad, containing the warning wrn. An example of the usage of tcWarning follows:

checkShadowing :: Name -> TypecheckM ()
checkShadowing x = do
  shadow <- isBound x
  when shadow $
    tcWarning $ ShadowedVarWarning x

In this example, the combinator tcWarning ShadowedVarWarning x throws a warning because there is a new declaration of a variable, which shadows an existing one.

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

DuplicateClassError (Name c)

creates a DuplicateClassError. This error should be created whenever there is a class whose declaration is duplicated (declaration of two classes with the same name).

Environment method entry. Contains method parameters and types. The MethodEntry is created during the Precheckable phase, which creates an Environment (symbol's table). After the MethodEntry has been created, it can be queried via helper functions, e.g., findMethod ty m.

Environment field entry. Contains class' fields parameters and types. The FieldEntry is created during the Precheckable phase, which creates an Environment (symbol's table). After the FieldEntry has been created, it can be queried via helper functions, e.g., findField ty m.

Environment class entry. Contains fields parameters and methods. The ClassEntry is created during the Precheckable phase, which creates an Environment (symbol's table). After the ClassEntry has been created, it can be queried via helper functions, e.g., findClass ty m.

Environment form from the PreEnv (pre-environment) and the Env (environment). The PreEnv contains a simple list of class names and is used to simply lookup whether a class name has already been defined, before the type checking phase. 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.

This is a helper to update the backtrace node in the environment Env. Usually not relevant for the developer of the compiler. Its main use case is during precheck function:

precheck x = local (pushBT x) $ doPrecheck x

which updates the backtrace of an Env.

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 p -> TypecheckM ClassEntry
findClass (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 will inject the Reader monad as the last argument. More details in the paper.

Check whether the name exists in the list of classes in the Env.

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

Lookup a Name, returning either an error or its type in the TypecheckM monad

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

Check whether a variable name is bound

Generate the pre-enviroment, that is, get the top level declaration of classes, methods and fields.

The type class defines how to precheck an AST node.

Environment generation from a parsed AST 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 program and its warnings. 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 errors or the resulting typed AST and its warnings.

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

Check whether a name shadows an existing variable name. For example:

checkShadowing name

checks whether name shadows an existing variable from Env.

Check whether the variable has been used or not. Throw a warning if the variable is not used. For example:

checkVariableUsage body name

This example checks whether the variable name is used in the AST node body, returning a warning if it is not used.

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

doTypecheck MethodDef {mname, mparams, mbody, mtype} = do
  (mparams', mtype') <- forkM typecheck mparams <&>
                         typecheck mtype
  -- extend environment with method parameters and typecheck body
  mbody' <- local (addParameters mparams') $ hasType mbody mtype'

in the last line we are type checking a method declaration, and 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