Copyright© 2019 Elias Castegren and Kiko Fernandez-Reyes
Safe HaskellSafe



This module includes everything you need to get started type checking a program. To build the Abstract Syntax Tree (AST), please import and build the AST from PhantomPhases.AST.

The main entry point to the type checker is the combinator tcProgram, which takes an AST and returns either an error, or the typed program with the current Phase. By Phase we mean that the type checker statically guarantees that all AST nodes have been visited during the type checking phase. For example, for the following program (using a made up syntax):

class C
  val f: Foo

should be parsed to generate this 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


data TCError where Source #

Declaration of a type checking errors


DuplicateClassError :: Name -> TCError

Declaration of two classes with the same name

UnknownClassError :: Name -> TCError

Reference of a class that does not exists

UnknownFieldError :: Name -> TCError

Reference of a field that does not exists

UnknownMethodError :: Name -> TCError

Reference of a method that does not exists

UnboundVariableError :: Name -> TCError

Unbound variable

TypeMismatchError :: Type Checked -> Type Checked -> TCError

Type mismatch error, the first Type refers to the formal type argument, the second Type refers to the actual type argument.

ImmutableFieldError :: Expr Checked -> TCError

Immutable field error, used when someone violates immutability

NonLValError :: Expr Checked -> TCError

Error to indicate that a one cannot assign a value to expression Expr

PrimitiveNullError :: Type Checked -> TCError

Error indicating that the return type cannot be Null

NonClassTypeError :: Type p -> TCError

Used to indicate that Type p is not of a class type

NonArrowTypeError :: Type Checked -> TCError

Expecting a function (arrow) type but got another type instead.

ConstructorCallError :: Type Checked -> TCError

Tried to call a constructor outside of instantiation

UninferrableError :: Expr Parsed -> TCError

Cannot infer type of Expr

Show TCError Source # 
Instance details

Defined in PhantomPhases.Typechecker


showsPrec :: Int -> TCError -> ShowS

show :: TCError -> String

showList :: [TCError] -> ShowS

data MethodEntry Source #

Environment method entry. Contains method parameters and types. The MethodEntry is created during the generateEnvironment function, 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.



data FieldEntry Source #

Environment field entry. Contains class' fields parameters and types.




data ClassEntry Source #

Environment class entry. Contains fields parameters and methods.



data Env Source #

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.




setConstructor :: Name -> Env -> Env Source #

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

lookupClass :: Name -> Env -> Maybe ClassEntry Source #

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 p1 -> 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.

lookupVar :: Name -> Env -> Maybe (Type Checked) Source #

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

findClass :: Type p -> TypecheckM ClassEntry Source #

Find a class declaration by its Type

findMethod :: Type p1 -> Name -> TypecheckM MethodEntry Source #

Find a method declaration by its Type and method name m

findField :: Type p1 -> Name -> TypecheckM FieldEntry Source #

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

findVar :: Name -> TypecheckM (Type Checked) Source #

Find a variable in the environment by its name x

generateEnvironment :: Program Parsed -> Except TCError Env Source #

Environment generation from a parsed AST program.

addVariable :: Name -> Type Checked -> Env -> Env Source #

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

addParameters :: [Param Checked] -> Env -> Env Source #

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

type TypecheckM a = forall m. (MonadReader Env m, MonadError TCError m) => m a Source #

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

tcProgram :: Program Parsed -> Either TCError (Program Checked) Source #

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

class Typecheckable a where Source #

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


typecheck :: a Parsed -> TypecheckM (a Checked) Source #

Type check the well-formedness of an AST node.

hasType :: Expr Parsed -> Type Checked -> TypecheckM (Expr Checked) Source #

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.

testClass1 :: ClassDef ip Source #

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])

testClass2 :: ClassDef ip Source #

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

testClass3 :: [ClassDef ip] Source #

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

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