# Publication details

##
A Constraint-Based Recast of ML-Polymorphism

Martin Müller

8$^th$ # International Workshop on Unification, June 1994

We implement the classical Damas-Milner type inference algorithm in a calculus with higher-order abstractions and 1st-order
constraints.
We encode mono(morphic) types as constraints, and poly(morphic) types
as abstractions
over monotypes.
Our calculus Rho_deep
is intended as computation model of a concrete programming language,
i.e., to be what the Lambda-calculus is for ML, or the Gamma-calculus for Oz.
Unlike usual in programming language research, Rho_deep
allows reduction below abstraction.
This allows to simplify our encoding of polytypes before usage.
In the envisaged programming language, the type inferencer can be run
just as specified.
We claim that deep reduction is one of the essential
features for such a high-level
implementation of type inference or abstract interpretation algorithms.
The algorithm can also be viewed as an extension of
Wand's type inference algorithm towards let-polymorphism.
Like Wand's, our algorithm is easily modified to supply
other monomorphic type systems with ML style polymorphism.

Download PDF
Show BibTeX

@INPROCEEDINGS{UNIF94,
title = {A Constraint-Based Recast of ML-Polymorphism},
author = {Martin M{\"u}ller},
year = {1994},
month = {jun # {23--25}},
editor = {{Denis Lugiez}},
booktitle = {8$^th$ # International Workshop on Unification},
note = {{Technical Report, Universit\'e de Nancy, to appear}},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009