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

Warning.Typechecker

Contents

Description

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 Warning.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 and a list of warnings. 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

This is an increment on top of the Typechecker module, that includes the Writer monad to add warnings to the compiler.

Synopsis

Type checking monad

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

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

Type checking errors

data TCError Source #

Declaration of type checking errors.

Constructors

TCError Error Backtrace 
Instances
Show TCError Source # 
Instance details

Defined in Warning.Typechecker

Methods

showsPrec :: Int -> TCError -> ShowS

show :: TCError -> String

showList :: [TCError] -> ShowS

data Error Source #

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.

Constructors

UnknownClassError Name

Reference of a class that does not exists

UnknownFieldError Name

Reference of a field that does not exists

UnknownMethodError Name

Reference of a method that does not exists

UnboundVariableError Name

Unbound variable

TypeMismatchError Type Type

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

ImmutableFieldError Expr

Immutable field error, used when someone violates immutability

NonLValError Expr

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

PrimitiveNullError Type

Error indicating that the return type cannot be Null

NonClassTypeError Type

Used to indicate that Type is not of a class type

NonArrowTypeError Type

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

ConstructorCallError Type

Tried to call a constructor outside of instantiation

UninferrableError Expr

Cannot infer type of Expr

Instances
Show Error Source # 
Instance details

Defined in Warning.Typechecker

Methods

showsPrec :: Int -> Error -> ShowS

show :: Error -> String

showList :: [Error] -> ShowS

data TCWarning Source #

Declaration of type checking warnings.

Instances
Show TCWarning Source # 
Instance details

Defined in Warning.Typechecker

Methods

showsPrec :: Int -> TCWarning -> ShowS

show :: TCWarning -> String

showList :: [TCWarning] -> ShowS

data Warning Source #

Declaration of available warnings. Value constructors are used to create statically known warnings. For example:

ShadowedVarWarning  (Name c)

creates a ShadowedVarWarning. This error should be created whenever there is a variable who shadows an existing variable in the environment.

Constructors

ShadowedVarWarning Name

Shadowing existing variable warning

UnusedVariableWarning Name

Unused variable warning

Instances
Show Warning Source # 
Instance details

Defined in Warning.Typechecker

Methods

showsPrec :: Int -> Warning -> ShowS

show :: Warning -> String

showList :: [Warning] -> ShowS

tcError :: Error -> TypecheckM a Source #

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.

tcWarning :: Warning -> TypecheckM () Source #

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

when shadow $
  tcWarning $ ShadowedVarWarning x

The code above throws a warning because the variable x was shadowing an existing variable from the environment.

Type checking combinators

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.

Constructors

Env 

Fields

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

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

emptyEnv :: Env Source #

Generates an empty environment.

lookupClass :: Name -> Env -> Maybe ClassDef 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 -> 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.

lookupVar :: Name -> Env -> Maybe Type 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 -> TypecheckM ClassDef Source #

Find a class declaration by its Type

findMethod :: Type -> Name -> TypecheckM MethodDef Source #

Find a method declaration by its Type and method name m

findField :: Type -> Name -> TypecheckM FieldDef Source #

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

findVar :: Name -> TypecheckM Type Source #

Find a variable in the environment by its name x

isBound :: Name -> TypecheckM Bool Source #

Checks whether a variable name is bound

genEnv :: Program -> Env Source #

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

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

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

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

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

tcProgram :: Program -> Either TCError (Program, [TCWarning]) Source #

Main entry point of the type checker. This function type checks an AST returning either an error or a well-typed program and warnigns. 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 and possible warnings.

class Typecheckable a where Source #

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

Minimal complete definition

doTypecheck

Methods

doTypecheck :: a -> TypecheckM a Source #

Type check the well-formedness of an AST node.

typecheck :: Backtraceable a => a -> TypecheckM a Source #

Type check an AST node, updating the environment's backtrace.

checkShadowing :: Name -> TypecheckM () Source #

Checks whether a variable name shadows an existing variable

checkVariableUsage :: Expr -> Name -> TypecheckM () Source #

Checks whether a variable x is used in the expression e.

hasType :: Expr -> Type -> TypecheckM Expr Source #

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.

buildClass :: String -> ClassDef Source #

Helper function for generating classes

testClass1 :: ClassDef 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 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
    x

testClass3 :: [ClassDef] 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
    x

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

testSuite :: IO () Source #

Test suite that runs testProgram.