Documentation

Determine the type of a value. May result in a type variable.

Check whether the values agree with the types (which may be abstract)

This is *probably* too lenient in the case of type variables: it can pass a mixed-type list.

The type of a substitution function, which maps type variables to types

Apply a substitution function to a type (possibly a type with variables)

Composing two substitutions

Identity substitution

A delta substitution is one that affects just a single variable.

Try to extend a substitution by adding a single variable-value pair

A TypeScheme (TypeScheme schematicVariables typeExpression) is a sort of type template, in which schematic variables (i.e., type parameters or "generics") are made explicit; any other type variables in the type expression are unknowns

Apply a substitution to a type scheme, taking care to affect only the unknowns, not the schematic variables

A type environment maps type variable names to type schemes. Oh, is it really type variable names, or just names? It seems to me that in envToTypeEnv, it's function names, instead of type variable names.

Insert a new type variable and its type scheme value

The unknowns of a type environment

A source of variable names

Creates a name supply

Produces next variable from a name supply

Produces next several variables from a name supply

Type check an expression

Type check a variable (actually the variable name). Find the type scheme associated with the variable in the type environment. Return a "new instance" of the type scheme, in which its schematic variables are replaced by new variables, and the unknowns are left as they are.

Create a TypeEnv from an Env Bindings on the left replace bindings of the same name on the right, if any.

The base type environment, derived from the base environment of the Sifflet language (built-in functions)

Convert a function type, such as a -> (b -> c), to a pair consisting of the list of argument types and the result type, such as ([a, b], c).

Decide the type of a function -- called by the function editor when the Apply button is clicked. decideTypes tries to find the argument types and return type of an expression considered as the body of a function, at the same time checking for consistency of inputs and outputs between the parts of the expression. It returns Succ (argtypes, returntype) if successful; Fail errormessage otherwise.