[Prev][Next][Index][Thread]

type inference in ML+


Followup concerning:

"Type Inference and Semi-Unification"
by Fritz Henglein, to appear in Proc. LISP and Functional Programming,
July 1988, Snowbird, Utah

I would like to clarify the previous announcement of my forthcoming
paper in the LISP and Functional Programming Conference.  In
particular, I would like to offer a brief chronology of recent work on
ML+ typability and a comparison of my work to the prior contribution
of Kfoury, Tiuryn, and Urzyczyn published in POPL, January '88.

Kfoury, Tiuryn, and Urzyczyn reported an exponential upper bound
for solving the typability problem of ML+ in POPL Jan. '88.  These
authors have just announced a gap in the proof that their algorithm is
correct.  Meanwhile, they have formulated a "Generalized Unification
Problem" (GUP) (which formalizes and improves the systems of
inequations approach found in their POPL '88 paper) to which the ML+
typing problem is reducible.  In the Fall of '87 I independently
developed a similar formulation of the typability problem in terms of
inequations (which I called semi-unification problem) and submitted an
extended abstract to LICS (Logic In Computer Science).  Unfortunately,
my algorithm was incorrect, and the paper was rejected.  In January
'88 I believed I had fixed up the algorithm and calculated a
polynomial upper bound on its time complexity.  These results were
resubmitted to the LISP and Functional Programming conference.
However, after a private communication with Prof. Kfoury, in which he
expressed a strong disbelief in a polynomial-time typability
algorithm, I found a basic error in my complexity analysis.
Consequently, the paper to appear at the July '88 LFP conference
describes the same semi-unification model (as found in the LICS
submission), a new graph theoretic algorithm and partial correctness
proof, but -- unfortunately -- no termination proof.

In comparison with GUP, my semi-unification model of typability can be
viewed as a quantifier-free version of the GUP problem and the
problem of solving "generic instance" relations (see, for example,
Damas, Milner, "Principal type schemes for functional programs", POPL '82).

Fritz Henglein
NYU/SETL project