This page presents my prototype typechecker for the MLF language. The prototype currently features the core ML constructs presented in this paper, as well as the ability to define new inductive types and (monomorphic, ML-style) recursion. The syntax is inspired from that of OCaml, except for the richer grammar of types and a few differences detailed below.

The prototype can be downloaded here. The tarball also includes an IDE in which constraints can be solved interactively, one step at a time.

Current limitations:

The prototype will be updated regularly, some of these limitations should be resolved soon.

Syntax differences with OCaml:

Experimental features