Standard ML with polymorphic recursion

Recursive function definitions in Standard ML are monomorphic: all occurrences of the defined function in its defining term must have the same type. The more general notion of polymorphic recursive definitions allows that these occurrences may be typed with instances of the type of the defining term.

This project implements a type checker for Standard ML with polymorphic recursion, which infers most general types in the Milner-Mycroft rather than the Hindley-Damas-Milner type system.

Since Milner-Mycroft typability is generally undecidable, the implementation allows the user to switch between these type systems. The aim is to gain some experience with the Milner-Mycroft system in practice, and test the conjecture that `hard' examples of type inference do not arise in actual programming.

Examples and future applications of polymorphic recursion.

Standard ML of New Jersey, Version 0.93 [Poly Rec]

Semiunification type constraints are represented as simple lists of type inequations, which are solved on typing recursive definitions. The representation could be improved (i) by using the semiunification graphs of F.Henglein and (ii) by storing properties of individual and type variables in attributes of these variables. But this would need a delicate combination with type unification in the existing compiler and some changes in fundamental datatypes of the existing compiler of SML of New Jersey.

Standard ML of New Jersey, Version 110 [Poly Rec]

After the release of SML/NJ Version 110 by Lucent Technologies in February 1998, an update of Poly Rec has been made that largely gives you the benefits of Poly Rec under SML Version 0.93.

Only the latest version 1.5 of Poly Rec has been adapted to SML/NJ Version 110. The correctness proof was made for version 1.3; the later version is simpler and more efficient due to a different representation of type inequation constraints. (Directory doc of polyrec.110.tar.gz also includes the correctness proof etc.)

Two provisos have to be made:


An implementation of semiunification in C, independent of Poly Rec, made by Dr.Robert Stärk, is also available: These can also be obtained from

Acknowledgement This project has been supported by the Deutsche Forschungsgemeinschaft and by ESPRIT Basic Research Action GENTZEN.

Martin Emms,
Hans Leiß,

Centrum für Informations-
und Sprachverarbeitung (CIS)
Universität München
Oettingenstr. 67
D-80538 München

Created: Mon Mar 16 18:30:06 MET 1998
Last modified: Mon Oct 15 11:21:10 MET 2001