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

Final.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 Final.AST.

The main entry point to the type checker is the combinator tcProgram, which takes an AST and returns either a list of errors, or the program and the generated 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
Synopsis

Type checking monad

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

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

(<:>) :: Semigroup e => Either e a -> Either e b -> Either e (a, b) Source #

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.

(<&>) :: (Semigroup e, MonadError e m) => m a -> m b -> m (a, b) Source #

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.

forkM :: (Semigroup e, MonadError e m) => (a -> m b) -> [a] -> m [b] Source #

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

newtype TCErrors Source #

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.

Constructors

TCErrors (NonEmpty TCError) 
Instances
Show TCErrors Source # 
Instance details

Defined in Final.Typechecker

Methods

showsPrec :: Int -> TCErrors -> ShowS

show :: TCErrors -> String

showList :: [TCErrors] -> ShowS

Semigroup TCErrors Source # 
Instance details

Defined in Final.Typechecker

Methods

(<>) :: TCErrors -> TCErrors -> TCErrors

sconcat :: NonEmpty TCErrors -> TCErrors

stimes :: Integral b => b -> TCErrors -> TCErrors

data TCError Source #

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

Constructors

TCError

Type checking error value constructor

Fields

  • Error

    Current type checking error

  • Backtrace

    Backtrace of the type checker

Instances
Show TCError Source # 
Instance details

Defined in Final.Typechecker

Methods

showsPrec :: Int -> TCError -> ShowS

show :: TCError -> String

showList :: [TCError] -> ShowS

data TCWarning Source #

Declaration of a type checking warnings in TCWarning.

Instances
Show TCWarning Source # 
Instance details

Defined in Final.Typechecker

Methods

showsPrec :: Int -> TCWarning -> ShowS

show :: TCWarning -> String

showList :: [TCWarning] -> ShowS

data Warning Source #

Available warnings in Warning.

Constructors

ShadowedVarWarning Name

Warning for shadowing a variable

UnusedVariableWarning Name

Warning for unused variables.

Instances
Show Warning Source # 
Instance details

Defined in Final.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. 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 Error where Source #

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

Constructors

DuplicateClassError :: Name -> Error

Declaration of two classes with the same name

UnknownClassError :: Name -> Error

Reference of a class that does not exists

UnknownFieldError :: Name -> Error

Reference of a field that does not exists

UnknownMethodError :: Name -> Error

Reference of a method that does not exists

UnboundVariableError :: Name -> Error

Unbound variable

TypeMismatchError :: Type p -> Type p -> Error

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

ImmutableFieldError :: Expr p -> Error

Immutable field error, used when someone violates immutability

NonLValError :: Expr p -> Error

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

PrimitiveNullError :: Type p -> Error

Error indicating that the return type cannot be Null

NonClassTypeError :: Type p -> Error

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

NonArrowTypeError :: Type p -> Error

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

ConstructorCallError :: Type p -> Error

Tried to call a constructor outside of instantiation

UninferrableError :: Expr p -> Error

Cannot infer type of Expr p

Instances
Show Error Source # 
Instance details

Defined in Final.Typechecker

Methods

showsPrec :: Int -> Error -> ShowS

show :: Error -> String

showList :: [Error] -> ShowS

data MethodEntry Source #

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.

Constructors

MethodEntry 

data FieldEntry Source #

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.

Constructors

FieldEntry 

Fields

data ClassEntry Source #

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.

Constructors

ClassEntry 

data Env Source #

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.

Constructors

PreEnv 

Fields

Env 

Fields

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

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

pushBT :: Backtraceable a => a -> Env -> Env Source #

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.

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

validClass :: Name -> Env -> Bool Source #

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

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.

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

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

findClass :: Type p -> TypecheckM ClassEntry Source #

Find a class declaration by its Type

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

Find a method declaration by its Type and method name m

findField :: Type p -> 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

isBound :: Name -> TypecheckM Bool Source #

Check whether a variable name is bound

generatePreEnv :: Program p -> Env Source #

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

class Precheckable a b | a -> b where Source #

The type class defines how to precheck an AST node.

Minimal complete definition

doPrecheck

Methods

doPrecheck :: a -> TypecheckM b Source #

Precheck an AST node

precheck :: Backtraceable a => a -> TypecheckM b Source #

Precheck an AST, updating the environment's backtrace.

generateEnvironment :: Program Parsed -> TypecheckM 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.

tcProgram :: Program Parsed -> Either TCErrors (Program Checked, [TCWarning]) Source #

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.

class Typecheckable a b | a -> b where Source #

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

Minimal complete definition

doTypecheck

Methods

doTypecheck :: a Parsed -> TypecheckM (b Checked) Source #

Type check the well-formedness of an AST node.

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

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

Instances
Typecheckable (Expr :: Phase (Proxy :: Type -> Type) -> Type) (Expr :: Phase Identity -> Type) Source # 
Instance details

Defined in Final.Typechecker

Typecheckable (MethodDef :: Phase (Proxy :: Type -> Type) -> Type) (MethodDef :: Phase Identity -> Type) Source # 
Instance details

Defined in Final.Typechecker

Typecheckable (Param :: Phase (Proxy :: Type -> Type) -> Type) (Param :: Phase Identity -> Type) Source # 
Instance details

Defined in Final.Typechecker

Typecheckable (FieldDef :: Phase (Proxy :: Type -> Type) -> Type) (FieldDef :: Phase Identity -> Type) Source # 
Instance details

Defined in Final.Typechecker

Typecheckable (ClassDef :: Phase (Proxy :: Type -> Type) -> Type) (ClassDef :: Phase Identity -> Type) Source # 
Instance details

Defined in Final.Typechecker

Typecheckable (Program :: Phase (Proxy :: Type -> Type) -> Type) (Program :: Phase Identity -> Type) Source # 
Instance details

Defined in Final.Typechecker

Typecheckable (Type :: Phase (Proxy :: Type -> Type) -> Type) (Type :: Phase Identity -> Type) Source # 
Instance details

Defined in Final.Typechecker

checkShadowing :: Name -> TypecheckM () Source #

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

checkShadowing name

checks whether name shadows an existing variable from Env.

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

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.

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 #

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

class C
  val f: Foo

testClass2 :: ClassDef Parsed 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 Parsed] 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