Language.Qux.Annotated.TypeChecker

Type checking functions to verify that a Program is type-safe.

These functions only verify that types are used correctly. They don't verify other properties such as definite assignment.

Environment

type Evaluation = StateT Locals (Reader Context)

An environment that holds the global types (Reader Context) and the local types (Locals).

type Check = ExceptT TypeException Evaluation

Either a TypeException or an a. Contains an underlying Evaluation in the monad transformer.

Contexts

data Context

Global context that holds function definition types. The function name and parameter types are held.

type Locals = Map Id Type

Local context.

context :: Program -> Context

Returns a context for the given program.

Type checking

Program checking

check :: Program SourcePos -> Except TypeException ()

Type checks the program. If an exception occurs then the result will be a TypeException, otherwise Nothing. This function wraps checkProgram by building and evaluating the environment under the hood.

Other node checking

checkProgram :: Program SourcePos -> Check ()

Type checks a program.

checkDecl :: Decl SourcePos -> Check ()

Type checks a declaration.

checkStmt :: Stmt SourcePos -> Check ()

checkExpr :: Expr SourcePos -> Check Type

Type checks an expression.

checkValue :: Value -> Check Type