Home > computing, Functional programming, OWL BASIC, Python, software > A Hindley-Milner type inference implementation in Python

A Hindley-Milner type inference implementation in Python

Before you get too excited this is an implementation of a type inference algorithm that happens to be written in Python; it has nothing to do with the Python language itself!

I’ve been working on OWL BASIC, a compiler for BBC BASIC for the .NET CLR. The compiler itself is written in IronPython. One of the challenges of compiling BBC BASIC is to infer the types of functions from the type of their return types. The return value of a BBC BASIC function can be an arbitrary expression, including calls to other functions or recursive calls to itself. I’ve implemented a simple type inference scheme which works well in the common cases, but for a fully capable solution my type checker and type inferencer need to be beefed up somewhat. To that end, I’ve been investigating standard type systems such as Hindley-Milner and inferencing algorithms such as Damas-Milner, sometimes known as Algorithm W. These algorithms or derivatives thereof are using in the ML family of languages (Standard ML, Ocaml, F#) and Haskell.

I managed to locate a Modula-2 implementation, a Perl implementation and a Scala implementation of the algorithm, each descended from the previous. With a view to improving my understanding of the algorithm I set about reimplementing in Python, largely guided by the Scala implementation, making mine the fourth in this sequence. I also located a Haskell implementation which seems to have independent ancestry. I’ve gone back to the companion paper (Cardelli 1987) to the original Modula-2 implementation and carried forward some of the code comments which had been omitted from its descendants to assist others who wish to understand the algorithm.

The program implements abstract syntax tree nodes for a small functional language, the type inferencing algorithm and finally exercises the algorithm by inferring the types of some canned expressions in the context of some predefined types. When executed it produces the following output:

> python hindley_milner.py
(letrec factorial = (fn n => (((cond (zero n)) 1) ((times n) (factorial (pred n))))) in (factorial 5)) :  int
(fn x => ((pair (x 3)) (x true))) :  Type mismatch: bool != int
((pair (f 4)) (f true)) :  Undefined symbol f
(let f = (fn x => x) in ((pair (f 4)) (f true))) :  (int * bool)
(fn f => (f f)) :  recursive unification
(let g = (fn f => 5) in (g g)) :  int
(fn g => (let f = (fn x => g) in ((pair (f 3)) (f true)))) :  (a -> (a * a))
(fn f => (fn g => (fn arg => (g (f arg))))) :  ((b -> c) -> ((c -> d) -> (b -> d)))

The Python code is shown below in its entirety or is available on GitHub. It will run without modification on Python 2.7 or Python 3.

#!/usr/bin/env python
.. module:: inference
   :synopsis: An implementation of the Hindley Milner type checking algorithm
              based on the Scala code by Andrew Forrest, the Perl code by
              Nikita Borisov and the paper "Basic Polymorphic Typechecking"
              by Cardelli.
.. moduleauthor:: Robert Smallshire

from __future__ import print_function

# =======================================================#
# Class definitions for the abstract syntax tree nodes
# which comprise the little language for which types
# will be inferred

class Lambda(object):
    """Lambda abstraction"""

    def __init__(self, v, body):
        self.v = v
        self.body = body

    def __str__(self):
        return "(fn {v} => {body})".format(v=self.v, body=self.body)

class Identifier(object):

    def __init__(self, name):
        self.name = name

    def __str__(self):
        return self.name

class Apply(object):
    """Function application"""

    def __init__(self, fn, arg):
        self.fn = fn
        self.arg = arg

    def __str__(self):
        return "({fn} {arg})".format(fn=self.fn, arg=self.arg)

class Let(object):
    """Let binding"""

    def __init__(self, v, defn, body):
        self.v = v
        self.defn = defn
        self.body = body

    def __str__(self):
        return "(let {v} = {defn} in {body})".format(v=self.v, defn=self.defn, body=self.body)

class Letrec(object):
    """Letrec binding"""

    def __init__(self, v, defn, body):
        self.v = v
        self.defn = defn
        self.body = body

    def __str__(self):
        return "(letrec {v} = {defn} in {body})".format(v=self.v, defn=self.defn, body=self.body)

# =======================================================#
# Exception types

class InferenceError(Exception):
    """Raised if the type inference algorithm cannot infer types successfully"""

    def __init__(self, message):
        self.__message = message

    message = property(lambda self: self.__message)

    def __str__(self):
        return str(self.message)

class ParseError(Exception):
    """Raised if the type environment supplied for is incomplete"""

    def __init__(self, message):
        self.__message = message

    message = property(lambda self: self.__message)

    def __str__(self):
        return str(self.message)

# =======================================================#
# Types and type constructors

class TypeVariable(object):
    """A type variable standing for an arbitrary type.

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

    next_variable_id = 0

    def __init__(self):
        self.id = TypeVariable.next_variable_id
        TypeVariable.next_variable_id += 1
        self.instance = None
        self.__name = None

    next_variable_name = 'a'

    def name(self):
        """Names are allocated to TypeVariables lazily, so that only TypeVariables
        if self.__name is None:
            self.__name = TypeVariable.next_variable_name
            TypeVariable.next_variable_name = chr(ord(TypeVariable.next_variable_name) + 1)
        return self.__name

    def __str__(self):
        if self.instance is not None:
            return str(self.instance)
            return self.name

    def __repr__(self):
        return "TypeVariable(id = {0})".format(self.id)

class TypeOperator(object):
    """An n-ary type constructor which builds a new type from old"""

    def __init__(self, name, types):
        self.name = name
        self.types = types

    def __str__(self):
        num_types = len(self.types)
        if num_types == 0:
            return self.name
        elif num_types == 2:
            return "({0} {1} {2})".format(str(self.types[0]), self.name, str(self.types[1]))
            return "{0} {1}" .format(self.name, ' '.join(self.types))

class Function(TypeOperator):
    """A binary type constructor which builds function types"""

    def __init__(self, from_type, to_type):
        super(Function, self).__init__("->", [from_type, to_type])

# Basic types are constructed with a nullary type constructor
Integer = TypeOperator("int", [])  # Basic integer
Bool = TypeOperator("bool", [])  # Basic bool

# =======================================================#
# Type inference machinery

def analyse(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 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. environment; this way there is no need to change the syntax or, more
    importantly, the type-checking program when extending the language.

        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

        The computed type of the expression.

        InferenceError: 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
        ParseError: The abstract syntax tree rooted at node could not be parsed

    if non_generic is None:
        non_generic = set()

    if isinstance(node, Identifier):
        return get_type(node.name, env, non_generic)
    elif isinstance(node, Apply):
        fun_type = analyse(node.fn, env, non_generic)
        arg_type = analyse(node.arg, env, non_generic)
        result_type = TypeVariable()
        unify(Function(arg_type, result_type), fun_type)
        return result_type
    elif isinstance(node, Lambda):
        arg_type = TypeVariable()
        new_env = env.copy()
        new_env[node.v] = arg_type
        new_non_generic = non_generic.copy()
        result_type = analyse(node.body, new_env, new_non_generic)
        return Function(arg_type, result_type)
    elif isinstance(node, Let):
        defn_type = analyse(node.defn, env, non_generic)
        new_env = env.copy()
        new_env[node.v] = defn_type
        return analyse(node.body, new_env, non_generic)
    elif isinstance(node, Letrec):
        new_type = TypeVariable()
        new_env = env.copy()
        new_env[node.v] = new_type
        new_non_generic = non_generic.copy()
        defn_type = analyse(node.defn, new_env, new_non_generic)
        unify(new_type, defn_type)
        return analyse(node.body, new_env, non_generic)
    assert 0, "Unhandled syntax node {0}".format(type(node))

def get_type(name, env, non_generic):
    """Get the type of identifier name from the type environment env.

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

        ParseError: Raised if name is an undefined symbol in the type
    if name in env:
        return fresh(env[name], non_generic)
    elif is_integer_literal(name):
        return Integer
        raise ParseError("Undefined symbol {0}".format(name))

def 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.

        t: A type to be copied.
        non_generic: A set of non-generic TypeVariables
    mappings = {}  # A mapping of TypeVariables to TypeVariables

    def freshrec(tp):
        p = prune(tp)
        if isinstance(p, TypeVariable):
            if is_generic(p, non_generic):
                if p not in mappings:
                    mappings[p] = TypeVariable()
                return mappings[p]
                return p
        elif isinstance(p, TypeOperator):
            return TypeOperator(p.name, [freshrec(x) for x in p.types])

    return freshrec(t)

def unify(t1, t2):
    """Unify the two types t1 and t2.

    Makes the types t1 and t2 the same.

        t1: The first type to be made equivalent
        t2: The second type to be be equivalent


        InferenceError: Raised if the types cannot be unified.

    a = prune(t1)
    b = prune(t2)
    if isinstance(a, TypeVariable):
        if a != b:
            if occurs_in_type(a, b):
                raise InferenceError("recursive unification")
            a.instance = b
    elif isinstance(a, TypeOperator) and isinstance(b, TypeVariable):
        unify(b, a)
    elif isinstance(a, TypeOperator) and isinstance(b, TypeOperator):
        if a.name != b.name or len(a.types) != len(b.types):
            raise InferenceError("Type mismatch: {0} != {1}".format(str(a), str(b)))
        for p, q in zip(a.types, b.types):
            unify(p, q)
        assert 0, "Not unified"

def 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

        t: The type to be pruned

        An uninstantiated TypeVariable or a TypeOperator
    if isinstance(t, TypeVariable):
        if t.instance is not None:
            t.instance = prune(t.instance)
            return t.instance
    return t

def is_generic(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

    Note: Must be called with v pre-pruned

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

        True if v is a generic variable, otherwise False
    return not occurs_in(v, non_generic)

def occurs_in_type(v, type2):
    """Checks whether a type variable occurs in a type expression.

    Note: Must be called with v pre-pruned

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

        True if v occurs in type2, otherwise False
    pruned_type2 = prune(type2)
    if pruned_type2 == v:
        return True
    elif isinstance(pruned_type2, TypeOperator):
        return occurs_in(v, pruned_type2.types)
    return False

def occurs_in(t, types):
    """Checks whether a types variable occurs in any other types.

        t:  The TypeVariable to be tested for
        types: The sequence of types in which to search

        True if t occurs in any of types, otherwise False
    return any(occurs_in_type(t, t2) for t2 in types)

def is_integer_literal(name):
    """Checks whether name is an integer literal string.

        name: The identifier to check

        True if name is an integer literal, otherwise False
    result = True
    except ValueError:
        result = False
    return result

# ==================================================================#
# Example code to exercise the above

def try_exp(env, node):
    """Try to evaluate a type printing the result or reporting errors.

        env: The type environment in which to evaluate the expression.
        node: The root node of the abstract syntax tree of the expression.

    print(str(node) + " : ", end=' ')
        t = analyse(node, env)
    except (ParseError, InferenceError) as e:

def main():
    """The main example program.

    Sets up some predefined types using the type constructors TypeVariable,
    TypeOperator and Function.  Creates a list of example expressions to be
    evaluated. Evaluates the expressions, printing the type or errors arising
    from each.


    var1 = TypeVariable()
    var2 = TypeVariable()
    pair_type = TypeOperator("*", (var1, var2))

    var3 = TypeVariable()

    my_env = {"pair": Function(var1, Function(var2, pair_type)),
              "true": Bool,
              "cond": Function(Bool, Function(var3, Function(var3, var3))),
              "zero": Function(Integer, Bool),
              "pred": Function(Integer, Integer),
              "times": Function(Integer, Function(Integer, Integer))}

    pair = Apply(Apply(Identifier("pair"),

    examples = [
        # factorial
        Letrec("factorial",  # letrec factorial =
               Lambda("n",  # fn n =>
                          Apply(  # cond (zero n) 1
                              Apply(Identifier("cond"),  # cond (zero n)
                                    Apply(Identifier("zero"), Identifier("n"))),
                          Apply(  # times n
                              Apply(Identifier("times"), Identifier("n")),
                                    Apply(Identifier("pred"), Identifier("n")))
                      ),  # in
               Apply(Identifier("factorial"), Identifier("5"))

        # Should fail:
        # fn x => (pair(x(3) (x(true)))
                         Apply(Identifier("x"), Identifier("3"))),
                   Apply(Identifier("x"), Identifier("true")))),

        # pair(f(3), f(true))
            Apply(Identifier("pair"), Apply(Identifier("f"), Identifier("4"))),
            Apply(Identifier("f"), Identifier("true"))),

        # let f = (fn x => x) in ((pair (f 4)) (f true))
        Let("f", Lambda("x", Identifier("x")), pair),

        # fn f => f f (fail)
        Lambda("f", Apply(Identifier("f"), Identifier("f"))),

        # let g = fn f => 5 in g g
            Lambda("f", Identifier("5")),
            Apply(Identifier("g"), Identifier("g"))),

        # example that demonstrates generic and non-generic variables:
        # fn g => let f = fn x => g in pair (f 3, f true)
                   Lambda("x", Identifier("g")),
                             Apply(Identifier("f"), Identifier("3"))
                       Apply(Identifier("f"), Identifier("true"))))),

        # Function composition
        # fn f (fn g (fn arg (f g arg)))
        Lambda("f", Lambda("g", Lambda("arg", Apply(Identifier("g"), Apply(Identifier("f"), Identifier("arg"))))))

    for example in examples:
        try_exp(my_env, example)

if __name__ == '__main__':
  1. Andy
    May 1st, 2010 at 10:34 | #1

    Wow! This is *very* cool, Robert! Many thanks for posting that code!

    I was just wondering – I’m thinking of doing a small public-domain programming language and am thinking of including H.M. type-checking in it. So, would I be able to use the above code in that public-domain language? I’ll certainly acknowledge you as the author, no problem there… :)

    Thanks again for this really interesting post!
    Bye for now –
    - Andy

  2. Robert Smallshire
    May 1st, 2010 at 11:12 | #2

    @Andy Of course! You are free to use this code in any way you like. Attribution of my authorship, and that of the ‘ancestral’ authors would be good sportsmanship, but is not required. I’m glad you found it useful.

  3. Andy
    May 1st, 2010 at 22:56 | #3

    @Robert Smallshire
    Great! Thanks very much for that, Robert!
    I will indeed credit yourself and the ‘ancestral’ authors.
    I’m looking forward to seeing more great posts like this! ( No pressure though… :D )

  4. Ali
    November 29th, 2011 at 01:40 | #4

    Awesome! I wanna ask you that have you done similar work in Groovy, Mozart-Oz or Go?
    I’m in a dire need of similar code in those languages

  5. November 20th, 2015 at 20:17 | #5

    Thanks for posting this. Some time ago I was able to use your Python code as the basis for type inference in the proof engine used in the mathtoys.org web site. Just returning to express my appreciation.

  1. January 29th, 2013 at 21:24 | #1
  2. March 6th, 2014 at 07:51 | #2