[Prev][Next][Index][Thread]
Corrigendum (LICS 87 paper)
Atsushi Ohori of the University of Pennsylvania has pointed out an error in my
1987 LICS paper ``Complete Type Inference for Simple Objects''. There are
programs without principal type schemes in the system in that paper.
Consider, for example:
\f. \x. f(x with a:=3) + f(emptyrec with a:=3)
This term will accept any x such that (x with a:=3) has the same type as
(\emptyrec~\with~a:=3). Thus either x can be the empty record, or x can
consist of a single ``a'' field (of any type). Thus the types of this term are
those of the forms
(\Pi\emptyrow[a<-int]->int) -> \Pi\emptyrow -> int
and
(\Pi\emptyrow[a<-int]->int) -> \Pi\emptyrow[a<-t] -> int
for any type t. Because of the difference in the second argument, there is no
single typescheme which generates just these types.
The correct result is that any program has a finite set of types, such that
any typing is an instance of some typing in the set.
The bug is in the part of the unification algorithm which does reasoning about
rows. There are actually two separate bugs:
First, consider the row equation r1[a<-t1] = r2[a<-t2]. It is not correct to
deduce that r1=r2 and t1=t2, since r1 and r2 might differ at label "a" and the
equation would still hold (since the difference at "a" is immediately
overwritten). The correct statement is that one of four situations hold:
1. r1 = r2
2. r1 = r0[a<-u1] and r2=r0[a<-u2] (ie r1 and r2 are both defined at a, but
there is no constraint on their values there)
3. r1 = r0 and r2=r0[a<-u2] (r2 is defined at a, but r1 need not be)
4. Symmetrical with #3.
Hence there is no principal solution. We can, however, come up with a finite
set of principal solutions by splitting the algorithm along these cases, and
taking the union of the resulting unifiers.
Second, if r1 and r2 are the same row variable, then these transformations do
not decrease the halting measure. Wlog, one can consider only equations of
the form r = r[a1<-t1]...[an<-tn]. Such an equation expresses the idea that r
has a1, ..., an in its domain. Termination can still be proved by treating
such equations specially. This bug was pointed out by Luca Cardelli.
All these corrections will be reflected in the revised version of the paper,
which is currently in preparation.
We thank Atsushi Ohori, Luca Cardelli, Pavel Curtis, Mads Tofte, and Chris
Haynes for their close reading and helpful comments.
Mitchell Wand
College of Computer Science
Northeastern University
360 Huntington Avenue #161CN
Boston, MA 02115
CSNet: wand@corwin.ccs.northeastern.edu