Implementation of the type checker

Implements a type checker (Damas-Hindley-Milner) with extensions.

class xotl.fl.typecheck.Class(typeclass: xotl.fl.ast.typeclasses.TypeClass, instances: Sequence[xotl.fl.ast.typeclasses.Instance])

xotl.fl.typecheck.build_substitution(alist: Sequence[Tuple[str, xotl.fl.ast.types.Type]]) → Callable[[str], xotl.fl.ast.types.Type]

Build a substitution from an association list.

This is the standard interpretation of a mapping from names to types. The substitution, when called upon, will look the list from beginning to end for an item with the same key and return the associated type.

If the same name is assigned more than once, return the first one.

We keep an internal copy of the alist. So, it’s safe to change the argument afterwards.

xotl.fl.typecheck.get_typeenv_unknowns(te: Mapping[Union[str, xotl.fl.meta.Symbol], xotl.fl.ast.types.TypeScheme]) → List[str]

Return all the non-generic variables in the environment.

xotl.fl.typecheck.newinstance(ns: Iterator[xotl.fl.ast.types.TypeVariable], ts: xotl.fl.ast.types.TypeScheme) → xotl.fl.ast.types.Type

Create an instance of ts drawing names from the supply ns.

Each generic variable in ts gets a new name from the supply.

class xotl.fl.typecheck.sub_typeenv(phi: Callable[[str], xotl.fl.ast.types.Type], env: Mapping[Union[str, xotl.fl.meta.Symbol], xotl.fl.ast.types.TypeScheme])

Create a sub-type environment.

Read the warning in subscheme().

xotl.fl.typecheck.tcl(env: Mapping[Union[str, xotl.fl.meta.Symbol], xotl.fl.ast.types.TypeScheme], ns: Iterator[xotl.fl.ast.types.TypeVariable], exprs: Iterable[xotl.fl.ast.base.AST]) → Tuple[Callable[[str], xotl.fl.ast.types.Type], List[xotl.fl.ast.types.Type]]

Type check several expressions in the context of env.

The name supply ns is shared across all other functions to ensure no names are repeated.

xotl.fl.typecheck.typecheck(exp: xotl.fl.ast.base.AST, env: Mapping[Union[str, xotl.fl.meta.Symbol], xotl.fl.ast.types.TypeScheme] = None, ns: Iterator[xotl.fl.ast.types.TypeVariable] = None) → Tuple[Callable[[str], xotl.fl.ast.types.Type], xotl.fl.ast.types.Type]

Check the type of exp in a given type environment env.

The type environment env is a mapping from program identifiers to type schemes. If env is None, we use the a basic type environment.

The type-variables supply ns is used to create new type variables whenever required. The name supply must ensure not to create the same variable twice. If ns is None, we create one with prefix set to ‘.t’ (it will create ‘.t0’, ‘.t1’, …).

xotl.fl.typecheck.typecheck_var(env: Mapping[Union[str, xotl.fl.meta.Symbol], xotl.fl.ast.types.TypeScheme], ns, exp: xotl.fl.ast.expressions.Identifier) → Tuple[Callable[[str], xotl.fl.ast.types.Type], xotl.fl.ast.types.Type]

Type check a single identifier.

The identifier’s name must be in the type environment env. If the identifier is a generic of the associated type scheme, a new name is created.

This is a combination of the TAUT and INST rules in [Damas1982].