Re: typing in ML+

To: types@theory.lcs.mit.edu
Subject: Re: typing in ML+
From: Fritz Henglein <henglein@henglein.cs.nyu.edu>
Date: Mon, 23 May 88 16:30:12 EDT
Cc: henglein@acf2.nyu.edu, paige@acf2.nyu.edu, kfoury@bu-cs.bu.edu

Announcement concerning:

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

This report is a corrected version of the original submission
entitled "The Milner-Mycroft Calculus is Tractable", which contained
a fatal flaw in the main theorem.

Since a report apparently containing work similar to ours has been
announced by Prof. Kfoury from Boston University we outline the
contents of the paper below.  The paper itself and two technical
reports entitled "Semi-Unification" and "The Milner-Mycroft Calculus",
respectively, on which the conference paper is based, are
available from

Fritz Henglein
New York University
715 Broadway, 7th floor
New York, N.Y. 10003
w#(212) 998-3488
(henglein@nyu.edu or henglein@rutgers.edu)

Outline of "Type Inference and Semi-Unification":

A set of equations and inequations is a pair (E, I) such that E is a
set of pairs { (T11, T12), ..., (Tn1, Tn2) } called equations and I is
a set of pairs { (U11, U12), ..., (Um1, Um2) } called inequations
where Tij and Uij are first-order terms over some ranked alphabet.
A substitution s is called a solution or semi-unifier of (E, I) if
s(T11) = s(T12), ..., s(Tn1) = s(Tn2) and r1(s(U11)) = s(U12), ...,
rm(s(Um1)) = s(Um2) hold simultaneously for some substitutions
r1, ..., rm where "=" is syntactic identity.

We show that the set of solutions (semi-unifiers) of any given set of
equations and inequations has a lattice structure similar, but not
identical to the structure of unifiers in unification problems.

We present an effective (polynomial-time) reduction of the typability
problem in the Mycroft Calculus (ML+) for a given (applied) lambda
expression e to a set of equations and inequations of size O(n^2)
where n is the size of e such that e is typable (in the Mycroft Calculus)
if and only if the constructed set of equations and inequations
has a solution.  Similar reductions can be applied to reduce
typability problems in the Milner Calculus (ML) and in the Hindley
Calculus (let-free ML) to sets of equations and inequations (in the
last case the set of inequations is empty).  The algebraic structure
of semi-unifiers yields, as a corollary, alternative proofs of the
principal typing properties of these calculi.

We then present a functional specification of a program for computing
the most general unifier (guaranteed to be unique upto an equivalence
relation on substitutions slightly weaker than renamings with
permutation substitutions) of a given set of equations and
inequations.  This specification is proved partially correct.

Finally, we present a nondeterministic graph-theoretic
"implementation" of the functional specification, which appears to be
"practical" as a type checking algorithm in a concrete language
design.  We show that this algorithm terminates for the case in which
the cardinality of I (the set of inequations) is 1, and we conjecture
that the algorithm terminates for any finite cardinality of I.  If
this conjecture is true it implies decidability of the Mycroft
Calculus (ML+).