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 Check = ReaderT Context (Writer [TypeException])

A type that allows collecting errors while type checking a program. Requires a Context for evaluation.

runCheck :: Check a -> Context -> (a, [TypeException])

Runs the given check with the context.

execCheck :: Check a -> Context -> [TypeException]

Runs the given check with the context and extracts the exceptions.

Global context

data Context

Global context that holds function definition types.

Constructors

Context

Fields

functions :: Map Id [Type]

A map of function names to parameter types.

context :: Program -> Context

Returns a context for the given program.

emptyContext :: Context

An empty context.

Local context

type Locals = Map Id Type

Local context. This is a map of variable names to types (e.g., parameters).

retrieve :: MonadReader Context m => Id -> StateT Locals m (Maybe [Type])

Retrieves the type of the given identifier. Preference is placed on local variables. A local variable type is a singleton list, while a function type is it's parameter types and return type.

Type checking

check :: Program SourcePos -> [TypeException]

Type checks the program, returning any errors that are found. A result of [] indicates the program is well-typed.

checkProgram :: Program SourcePos -> Check ()

Type checks a program.

checkDecl :: Decl SourcePos -> Check ()

Type checks a declaration.

checkStmt :: Stmt SourcePos -> StateT Locals Check ()

Type checks a statement.

checkExpr :: Expr SourcePos -> StateT Locals Check Type

Type checks an expression.