Copyright | © 2019 Elias Castegren and Kiko Fernandez-Reyes |
---|---|
License | MIT |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
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 TypecheckM a = forall m. (MonadReader Env m, MonadError TCErrors m, MonadWriter [TCWarning] m) => m a
- (<:>) :: Semigroup e => Either e a -> Either e b -> Either e (a, b)
- (<&>) :: (Semigroup e, MonadError e m) => m a -> m b -> m (a, b)
- forkM :: (Semigroup e, MonadError e m) => (a -> m b) -> [a] -> m [b]
- newtype TCErrors = TCErrors (NonEmpty TCError)
- data TCError = TCError Error Backtrace
- data TCWarning = TCWarning Warning Backtrace
- data Warning
- tcError :: Error -> TypecheckM a
- tcWarning :: Warning -> TypecheckM ()
- data Error where
- DuplicateClassError :: Name -> Error
- UnknownClassError :: Name -> Error
- UnknownFieldError :: Name -> Error
- UnknownMethodError :: Name -> Error
- UnboundVariableError :: Name -> Error
- TypeMismatchError :: Type p -> Type p -> Error
- ImmutableFieldError :: Expr p -> Error
- NonLValError :: Expr p -> Error
- PrimitiveNullError :: Type p -> Error
- NonClassTypeError :: Type p -> Error
- NonArrowTypeError :: Type p -> Error
- ConstructorCallError :: Type p -> Error
- UninferrableError :: Expr p -> Error
- data MethodEntry = MethodEntry {}
- data FieldEntry = FieldEntry {}
- data ClassEntry = ClassEntry {
- cefields :: Map Name FieldEntry
- cemethods :: Map Name MethodEntry
- data Env
- setConstructor :: Name -> Env -> Env
- pushBT :: Backtraceable a => a -> Env -> Env
- lookupClass :: Name -> Env -> Maybe ClassEntry
- validClass :: Name -> Env -> Bool
- lookupVar :: Name -> Env -> Maybe (Type Checked)
- resolveClass :: Name -> TypecheckM (Type Checked)
- findClass :: Type p -> TypecheckM ClassEntry
- findMethod :: Type p -> Name -> TypecheckM MethodEntry
- findField :: Type p -> Name -> TypecheckM FieldEntry
- findVar :: Name -> TypecheckM (Type Checked)
- isBound :: Name -> TypecheckM Bool
- generatePreEnv :: Program p -> Env
- class Precheckable a b | a -> b where
- doPrecheck :: a -> TypecheckM b
- precheck :: Backtraceable a => a -> TypecheckM b
- generateEnvironment :: Program Parsed -> TypecheckM Env
- addVariable :: Name -> Type Checked -> Env -> Env
- addParameters :: [Param Checked] -> Env -> Env
- tcProgram :: Program Parsed -> Either TCErrors (Program Checked, [TCWarning])
- class Typecheckable a b | a -> b where
- doTypecheck :: a Parsed -> TypecheckM (b Checked)
- typecheck :: Backtraceable (a Parsed) => a Parsed -> TypecheckM (b Checked)
- checkShadowing :: Name -> TypecheckM ()
- checkVariableUsage :: Expr p -> Name -> TypecheckM ()
- hasType :: Expr Parsed -> Type Checked -> TypecheckM (Expr Checked)
- testClass1 :: ClassDef ip
- testClass2 :: ClassDef Parsed
- testClass3 :: [ClassDef Parsed]
- testProgram :: Program Parsed
- testValidProgram :: Program Parsed
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.
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.
Declaration of a type checking error, where Error
represents
the current type checking error and Backtrace
the up-to-date backtrace.
TCError | Type checking error value constructor |
Declaration of a type checking warnings in TCWarning
.
Available warnings in Warning
.
ShadowedVarWarning Name | Warning for shadowing a variable |
UnusedVariableWarning Name | Warning for unused variables. |
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
throws
a warning because there is a new declaration of a variable, which shadows
an existing one.tcWarning
ShadowedVarWarning x
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).
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 |
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 |
PrimitiveNullError :: Type p -> Error | Error indicating that the return type cannot be |
NonClassTypeError :: Type p -> Error | Used to indicate that |
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 |
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
.
Instances
Precheckable (MethodDef Parsed) MethodEntry Source # | |
Defined in Final.Typechecker |
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
.
Instances
Precheckable (FieldDef Parsed) FieldEntry Source # | |
Defined in Final.Typechecker |
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
.
ClassEntry | |
|
Instances
Precheckable (ClassDef Parsed) ClassEntry Source # | |
Defined in Final.Typechecker |
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.
setConstructor :: Name -> Env -> Env Source #
Conditionally update the environment to track if we are in a constructor method.
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
.
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.
doPrecheck :: a -> TypecheckM b Source #
Precheck an AST node
precheck :: Backtraceable a => a -> TypecheckM b Source #
Precheck an AST, updating the environment's backtrace.
Instances
Precheckable (MethodDef Parsed) MethodEntry Source # | |
Defined in Final.Typechecker | |
Precheckable (FieldDef Parsed) FieldEntry Source # | |
Defined in Final.Typechecker | |
Precheckable (ClassDef Parsed) ClassEntry Source # | |
Defined in Final.Typechecker | |
Precheckable (Param Parsed) (Param Checked) Source # | |
Defined in Final.Typechecker | |
Precheckable (Type p) (Type Checked) Source # | |
Defined in Final.Typechecker doPrecheck :: Type p -> TypecheckM (Type Checked) Source # |
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.
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 # | |
Defined in Final.Typechecker | |
Typecheckable (MethodDef :: Phase (Proxy :: Type -> Type) -> Type) (MethodDef :: Phase Identity -> Type) Source # | |
Defined in Final.Typechecker | |
Typecheckable (Param :: Phase (Proxy :: Type -> Type) -> Type) (Param :: Phase Identity -> Type) Source # | |
Defined in Final.Typechecker | |
Typecheckable (FieldDef :: Phase (Proxy :: Type -> Type) -> Type) (FieldDef :: Phase Identity -> Type) Source # | |
Defined in Final.Typechecker | |
Typecheckable (ClassDef :: Phase (Proxy :: Type -> Type) -> Type) (ClassDef :: Phase Identity -> Type) Source # | |
Defined in Final.Typechecker | |
Typecheckable (Program :: Phase (Proxy :: Type -> Type) -> Type) (Program :: Phase Identity -> Type) Source # | |
Defined in Final.Typechecker | |
Typecheckable (Type :: Phase (Proxy :: Type -> Type) -> Type) (Type :: Phase Identity -> Type) Source # | |
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