hask.lang.hindley_milner – Hindley-Milner type-checking and inference

Implementation of Hindley-Milner type inference system for Python, based on Robert Smallshire’s implementation for OWL BASIC.

Robert’s original version can be found here: http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hindley-milner-type-inference-implementation-in-python/

Changes from Robert’s version:

1. Simplified type language somewhat (Let and Letrec are merged, as are Var and Ident)
2. Type system expanded to handle polymorphic higher-kinded types (however, in its current state it does not do this correctly due to the way that typeclasses were bolted on; this will be fixed in future versions)
3. Interface tweaked a bit to work better with Python types, including pretty-printing of type names and some useful subclasses of TypeOperator
4. Type unification also unifies typeclass constraints

class hask.lang.hindley_milner.AST

A low-level AST node in a typed lambda calculus.

class hask.lang.hindley_milner.App(fn, arg)

Function application.

An App node represents the application of a single argument. Functions over several arguments are curried.

class hask.lang.hindley_milner.Function(from_type, to_type)

A binary type constructor which builds function types

class hask.lang.hindley_milner.Lam(v, body)

Lambda abstraction

class hask.lang.hindley_milner.Let(v, defn, body)

Let binding (always recursive)

class hask.lang.hindley_milner.ListType(list_type)

Unary constructor which builds list types

class hask.lang.hindley_milner.Tuple(types)

N-ary constructor which builds tuple types

class hask.lang.hindley_milner.TypeOperator(name, types)

An n-ary type constructor which builds a new type from old

class hask.lang.hindley_milner.TypeVariable(constraints=())

A type variable standing for an arbitrary type.

All type variables have a unique id, but names are only assigned lazily, when required.

Note that this approach is not thread-safe.

name

Names are allocated to TypeVariables lazily, so that only TypeVariables converted to strings are given names.

class hask.lang.hindley_milner.Var(name)

Variable/Identifier

hask.lang.hindley_milner.analyze(node, env, non_generic=None)

Computes the type of the expression given by node.

The type of the node is computed in the context of the supplied type environment, env. Data types can be introduced into the language simply by having a predefined set of identifiers in the initial environment. This way there is no need to change the syntax or, more importantly, the type-checking program when extending the language.

Parameters:

• node – The root of the abstract syntax tree.
• env – The type environment is a mapping of expression identifier names to type assignments. to type assignments.
• non_generic – A set of non-generic variables, or None

Returns:

The computed type of the expression.

Raises:

TypeError – The type of the expression could not be inferred, for example if it is not possible to unify two types such as Integer and Bool or if the abstract syntax tree rooted at node could not be parsed

hask.lang.hindley_milner.fresh(t, non_generic)

Makes a copy of a type expression.

The type t is copied. The the generic variables are duplicated and the non_generic variables are shared.

Parameters:

• t – A type to be copied.
• non_generic – A set of non-generic TypeVariables

hask.lang.hindley_milner.getType(name, env, non_generic)

Get the type of identifier name from the type environment env.

Parameters:

• name – The identifier name
• env – The type environment mapping from identifier names to types
• non_generic – A set of non-generic TypeVariables

Raises:

ParseError – Raised if name is an undefined symbol in the type environment.

hask.lang.hindley_milner.isGeneric(v, non_generic)

Checks whether a given variable occurs in a list of non-generic variables

Note that a variables in such a list may be instantiated to a type term, in which case the variables contained in the type term are considered non-generic.

Note

Must be called with v pre-pruned

Parameters:

• v – The TypeVariable to be tested for genericity
• non_generic – A set of non-generic TypeVariables

Returns:

True if v is a generic variable, otherwise False

hask.lang.hindley_milner.occursIn(t, types)

Checks whether a types variable occurs in any other types.

Parameters:

• v – The TypeVariable to be tested for
• types – The sequence of types in which to search

Returns:

True if t occurs in any of types, otherwise False

hask.lang.hindley_milner.occursInType(v, type2)

Checks whether a type variable occurs in a type expression.

Note

Must be called with v pre-pruned

Parameters:

• v – The TypeVariable to be tested for
• type2 – The type in which to search

Returns:

True if v occurs in type2, otherwise False

hask.lang.hindley_milner.prune(t)

Returns the currently defining instance of t.

As a side effect, collapses the list of type instances. The function prune is used whenever a type expression has to be inspected: it will always return a type expression which is either an uninstantiated type variable or a type operator; i.e. it will skip instantiated variables, and will actually prune them from expressions to remove long chains of instantiated variables.

Parameters:t – The type to be pruned Returns:An uninstantiated TypeVariable or a TypeOperator

hask.lang.hindley_milner.show_type(type_name)

Pretty-print a Python type or internal type name.

Parameters:type_name – a Python type, or a string representing a type name Returns:a string representation of the type

hask.lang.hindley_milner.unify(t1, t2)

Unify the two types t1 and t2. Makes the types t1 and t2 the same.

Note that the current method of unifying higher-kinded types does not properly handle kind, i.e. it will happily unify f a and g b c. This is due to the way that typeclasses are implemented, and will be fixed in future versions.

Parameters:

• t1 – The first type to be made equivalent
• t2 – The second type to be be equivalent

Modify t1 and t2 in-place, by modifying their constraints for the unification.

Raises:TypeError – Raised if the types cannot be unified.

hask.lang.hindley_milner.unify_var(v1, t2)

Unify the type variable v1 and the type t2, i.e. makes their types the same and unifies typeclass constraints. Note: Must be called with v1 and t2 pre-pruned

Parameters:

• v1 – The type variable to be made equivalent
• t2 – The second type to be be equivalent

Instead of returning, modify v1 and t2 to add the unification as a constraint.

Raises:TypeError – Raised if the types cannot be unified.