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]

Source code of the modified type checker, installation guide, etc.: polyrec.093.tar.gz (400 KB)
The batch compiler of SML of New Jersey is needed to generate the modified compiler. In the root directory of your SML/NJ 0.93 distribution, unpack the file with
```
 gunzip -c polyrec.093.tar.gz | tar xvf - 
```
This creates a subdirectory polyrec; follow the install notes there.
Binaries for a SUN-4 architecture under SunOS 4.1.4 (sml.polyrec.5.sun4.gz) (1.5 MB)
Extending the Type Checker of SML by Polymorphic Recursion --
A Correctness Proof (with M.Emms). CIS-Bericht-96-101.ps.gz.

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.

Source code of the modified type checker, installation guide, etc.: polyrec.110.tar.gz (~ 320k)
To install SML/NJ Version 110 [Poly Rec], unpack the file in the root directory of your SML distribution. You need the compilation manager CMB included in the distribution of SML/NJ Version 110 (target sml-full-cm of config/targets).
Binaries for x86-machines under Linux: sml-polyrec-x86bin.tgz (2.3 MB)
Uncompressing this file with tar xvzf sml-polyrec-x86bin.tgz creates two subdirectories: a directory polyrec containing the documentation files and source code, and a directory bin containing
```
    bin/.arch-n-opsys
    bin/.run/
    bin/.run/run.x86-linux
    bin/.heap/
    bin/.heap/smlpr.x86-linux
    bin/smlpr
    bin/.run-sml
```
Edit the file bin/.run-sml by setting its BIN_DIR variable to the subdirectory bin of the directory where you unpacked sml-polyrec-x86bin.tgz. To run sml-polyrec, call bin/smlpr.
The SML-structure containing the control flags of the type checker and the viewing options of the semiunification solver actually is Compiler.Control, not Compiler.Control.CG, as it is called in doc/USER_MANUAL.

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:

Since the intermediate language of Version 110 is typed (as opposed to the one of Version 0.93), some programs typable under under polymorphic recursion are not accepted by Version 110 [Poly Rec].
If the defining expression t of a recursive function f has principal type ty1 -> ... -> tyN and tyN is a type variable(!), then f must not be used in t with some instance ty1' -> ...-> tyN' where tyN' is (ty -> ty'). Thus, the arity of f in t must not exceed the one of the defining expression (a natural restriction that seems to exclude nonterminating functions only). For example,
```
fun f x = f f x 
```
is rejected. We have not yet incorporated an arity check into Poly Rec, so you will recieve a compiler bug:
```
Error: Compiler bug: LambdaType: unexpected case in tcd_arw
```
The datatype of types in Version 110 differs from that of Version 0.93. Some adaption to the semiunification algorithm in Poly Rec has been made to account for that, but no extensive tests have been made. Please report any problems to leiss@cis.uni-muenchen.de

Semiunification

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 http://www.inf.ethz.ch/~staerk/semiunify-1.0.tar.gz.

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

Martin Emms, emms@cis.uni-muenchen.de
Hans Leiß, leiss@cis.uni-muenchen.de

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