Copyright © 2019 Elias Castegren and Kiko Fernandez-Reyes MIT experimental portable Safe

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 Reader.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. 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 Reader monad to remove some of the boilerplate.

Synopsis

# Documentation

data TCError 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 TCError Source # Instance detailsDefined in Reader.Typechecker MethodsshowsPrec :: Int -> TCError -> ShowSshow :: TCError -> StringshowList :: [TCError] -> ShowS

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 Fieldsctable :: Map Name ClassDef vartable :: Map Name Type constructor :: Bool

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

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 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 Environment generation from an AST 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. 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 -> Either TCError Program 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. Methods typecheck :: a -> TypecheckM a Source # Type check the well-formedness of an AST node. Instances  Source # Instance detailsDefined in Reader.Typechecker Methods Source # Instance detailsDefined in Reader.Typechecker Methods Source # Instance detailsDefined in Reader.Typechecker Methods Source # Instance detailsDefined in Reader.Typechecker Methods Source # Instance detailsDefined in Reader.Typechecker Methods Source # Instance detailsDefined in Reader.Typechecker Methods Source # Instance detailsDefined in Reader.Typechecker Methods This combinator is used whenever a certain type is expected. This function is quite important. Here follows an example: typecheck 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

testSuite :: IO () Source #