ottie (try live)

Monorepo containing the resources for OTTIE, the Online Teaching Type Inference Environment.

Summary

Type inference is a process by which types of a program are determined automatically by a compiler, without needing programmers to supply explicit type annotations. Understanding type inference helps programmers debug type errors and better understand type systems. However, few accessible teaching resources are available. This project presents an interactive type inference teaching tool, OTTIE, for a Hindley-Milner based expression language. It visualises and explains the steps taken by the common type inference algorithms W, W' and M. User testing with undergraduate students shows that OTTIE improves their test scores in a quiz on types and type inference (p < 0.001), and general feedback from users is positive. Analytics data provides evidence that the tool’s output aids understanding and allows users to debug type errors.

What is type inference?

Given a program or expression, we can often infer some (or all) of its types. For example, in the simple expression:

odd(3)

We might make the observations:

• 3 is an integer constant, so has type Int
• odd is a function defined globally (for our language - like a standard library), and we know it has type Int -> Bool (it returns whether the number is odd, e.g. odd(1) == odd(3) == True, odd(2) == False)
• Given we have applied a function Int -> Bool to an Int, we expect the overall result of the expression to be a Bool.

With the expression:

odd(True)

We might make the observations:

• True is a boolean constant, so has type Bool
• odd is has type Int -> Bool, as before
• Given we have applied a function Int -> Bool to an Bool, we raise a type error as these types do not match. This flags to the programmer they have made a mistake which they can fix (and fewer mistakes in programs is good!).

These are both simple examples, but we can take type inference further by adding more constructs to our language. For example we can add function abstraction (written \param -> body), effectively creating a new anonymous function (arrow or lambda functions in JavaScript or Java/C++/Python-speak). We also add let statements, similar to function abstraction but given a parameter directly - this allows us to perform generalisation without making the type system undecidable (as it is in System F, as proved by Joe Wells, which peforms generalisation more). Generalisation is how we get parametric polymorphism, and is the process by which we can convert a type like [t0] -> Int to forall. [t0] -> Int (the difference between being able to apply it to one type of array, or any array. this type would be good for an array length function for example).

All together, we can now get expressions like:

let id = (\x -> x) in (id 3, id [True, False])

Exciting! The typing rules of our language are defined by the type system. The Hindley-Milner type system is one such example, and is the one we use. This formalises what we've discussed with lots of very clever maths. Algorithm W is commonly seen as the type inference algorithm for Hindley-Milner, and is a frequently studied algorithm for type inference. It's the basis for ML's type inference, and Haskell used to perform similar type inference (but later changed for performance and to better support extensions to the type system). Apple's Swift uses an algorithm "reminiscent of the classical Hindley-Milner type inference algorithm".

Algorithm W is presented as a series of rules for differnet expressions:

(These mathematical expressions are a little scary when presented like this, and it's not exactly friendly for newcomers to understand - that's what OTTIE aims to change!)

In addition to W, there are other algorithms that perform type inference on the Hindley-Milner type system including W' and M. All of these are available in OTTIE, which shows a step-by-step derivation for them running on any syntactically valid input expression.

Structure

OTTIE is composed of five loosely-coupled TypeScript packages. These include a language core, which contains shared models and functions for handling a simple expression language (with similar syntax to Haskell) and its type system. On top of this 3 type inference algorithms are implemented: Algorithm W, W' and M (computer scientists do not come up with creative names!). The web application consumes all these libraries and provides an interface to users shows step-by-step type inference derivations for custom user input expressions.

• language: The language core contains shared models such as AST nodes for representing input expressions, contexts to represent bound variables and substitutions useful for type inference algorithms. The language core also includes a lexer and paser (using the Masala parser combinator library) for the basic expression language, along with utility functions for manipulating its models.
• algorithm-w: An implementation of Robin Milner's Algorithm W introduced in A theory of type polymorphism in programming.
• algorithm-w-prime: An implementation of Bruce McAdam's Algorithm W' introduced in On the unification of substitutions in type inference.
• algorithm-m: An implementation of Oukseh Lee and Kwagkeun Yi's Algorithm M introduced in Proofs about a folklore let-polymorphic type inference algorithm.
• web: The web application itself. Allows users to enter an expression and view the resulting type and step-by-step type derivation. Visualises the expression's equivalent AST, highlighting relevant parts being acted upon in the step-by-step instructions. Behind the scenes, the expression is lexed and parsed by the language core, and type inference is done by one of the type inference algorithms. Created with Create React App's TypeScript preset. Sends analytics events to an analytics lambda.

In addition to these packages, this repo contains some supporting files.

• docs: Project documentation, including the specification, progress report and final report LaTeX sources and build scripts. Most of the LaTeX is automatically generated from Google Docs using my gdoc2latex tool.
• .github/workflows: CI scripts for building the packages and documentation with GitHub Actions on each commit. Also handles publishing the static site to the gh-pages branch so it's kept up to date.

Contributing

To set up your coding environment:

• open this monorepo (at the top-level) in VS Code
• install Node 14
• install NPM 7 (after Node 14, you should be able to run npm i -g npm@7)
• follow the setup instructions for the corresponding package