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

An old confusion about undecidability of type checking with subtypes


                         ABSTRACT
This note discusses the significance of the work of
Abiteboul, Kanellakis, and Waller as reported in the 1990 PODS [1].
That paper presents an undecidability result for type checking
method schemes in the presence of subtyping.  The question is:
what is the practical significance of that undecidability result
for programming language theorists (and language designers)?

INTRODUCTION

First a little (personal) history.  In the Spring of 1990, I gave a talk at 
U. Penn and presented some of my work on subtyping for abstract data types
[2] [3] [4] [5] [6] (although I didn't talk about all of these then).
Part of this work was a description of a simple (monomorphic) type system
with subtypes based on Reynolds's category sorted algebras [7] [8].
I had a set of type inference rules for this type system worked out [3] [4],
but had not implemented the toy language or the type checker for it.
During the talk, Peter Buneman asked me whether type checking for my language
was decidable.   I said that I thought it was, as it seemed clear how
to convert my type inference rules into a type checker.  He asked if I had
heard of the work of Abiteboul, Kanellakis, and Waller [1], and briefly
explained it to me.

Since that time I have been puzzled about the significance of
the paper by Abiteboul, Kanellakis, and Waller [1].
Does it really mean that there cannot be a decidable type system for
a language with message passing and subtyping?  How does one reconcile
this with the decidability of my type system and the existence of type
checkers for languages like Trellis/Owl [9]?

AN ANSWER

The answer turns out to be very simple.  Method Schemas, as defined in [1],
are quite general, whereas my type system is a special case.
If a general problem is proved to be undecidable,
that does not mean that a restricted version of that problem is undecidable.

Method Schemas resemble the Common LISP Object System (CLOS) in that
a method calls dispatch on the dynamic types of all arguments (not just the
first as in Smalltalk).  This is similar to Reynolds's category sorted
algebras [7] [8].  Since my toy language was adapted from Reynolds's work,
and since reference [1] emphasizes that the combination of recursion and
multiple argument dispatch leads to undecidability, it was natural for Peter
Buneman to ask me whether my type checking for my type system was decidable.

However, the emphasis in [1] (page 17) on multiple argument dispatch is
misplaced.  The real problem is that in the Method Schemas of [1],
redefinitions of inherited methods are allowed to be covariant,
but there are no restrictions on leaving gaps in the coverage of redefined
methods.   These gaps are combinations of argument types
for which no method is defined.  For example, if S is a subtype of T,
then one can overload a message name with the following types
	T,T -> bool
	T,S -> bool
	S,T -> bool
but one can leave out S,S -> bool.  (In category sorted algebras[7] [8],
the message would also have to be defined with type S,S -> bool.)

So with the unrestricted method schemas of [1], one may leave such gaps,
which are type errors waiting to happen.  For example, one may have
two variables that are statically of type T, but denote objects of type S
(as permitted by subtyping).  Then if one uses the method in question,
a type error will occur, because there is no method that takes two S arguments.
The problem of type checking then boils down to whether such gaps are ever
exploited in a program execution.  It is easy to see how that is undecidable
and a careful proof is given in [1].

CONCLUSION

What is the significance of the paper by Abiteboul, Kanellakis,
and Waller [1]?  To my mind it reinforces the old maxim of language design:
ruling out a problem is much better than allowing it to happen and checking
for it.   In this case, by forcing the programmer to not leave gaps,
the troublesome type errors are ruled out, and type checking becomes decidable.
The other point that is now clear in my mind is that reference [1]
should not trouble designers of type systems that require contravariance,
or type systems based on Reynolds's category sorted algebras.


	Gary Leavens

	229 Atanasoff Hall, Department of Computer Science
	Iowa State University, Ames, Iowa 50011-1040, USA
	phone: (515) 294-1580  fax: (515) 294-0258


REFERENCES

[1] @InProceedings{Abiteboul-Kanellakis-Waller90,
Key="Abiteboul \& Kanellakis \& Waller",
Author="Serge Abiteboul and Paris C. Kanellakis and Emmanuel Waller",
Title="Method Schemas (Preliminary Report)",
BookTitle="Principles of Data Base Systems",
Organization=ACM,
Year=1990,
Pages="16-27",
Annote="Method schemas are a simple model for object-oriented programming.
	Consistency problem is undecidable in general, but decidable
	for monadic and/or recursion-free method schemas.  20 references."
}

[2] @Article{Leavens-Weihl90, Key="Leavens \& Weihl",
Author="Gary T. Leavens and William E. Weihl",
Title="Reasoning about Object-oriented Programs that use Subtypes
	(extended abstract)",
Journal=SIGPLAN,
Volume=25,
Number=10,
Month=Oct,
Year=1990,
Pages="212-223",
Note="{\em OOPSLA ECOOP '90 Proceedings}, N. Meyrowitz (editor).",
Annote="26 references."
}

[3] @TechReport{Leavens89, Key="Leavens",
Author="Gary Todd Leavens",
Title="Verifying Object-Oriented Programs that use Subtypes",
Month=Feb,
Year=1989,
Institution=MITLCS,
Number=439,
Note="The author's Ph.D. thesis.",
Annote="44 references."
}

[4] @TechReport{Leavens90, Key="Leavens",
Author="Gary T. Leavens",
Title="Modular Verification of Object-Oriented Programs with Subtypes",
Month=Jul,
Year=1990,
Institution="Department of Computer Science, Iowa State University",
Address="Ames, Iowa, 50011",
Number="90-09",
Annote="74 references."
}

[5] @Article{Leavens91,
  Key = 	"Leavens",
  Author = 	"Gary T. Leavens",
  Title = 	"Modular Specification and Verification of
		 Object-Oriented Programs",
  Journal = 	"IEEE Software",
  Year = 	1991,
  Volume = 	8,
  Number = 	4,
  Month = 	Jul,
  Pages =       "72-80",
  Annote = 	"8 references."
}

[6] @InCollection{Leavens-Pigozzi92,
  Key = 	"Leavens \& Pigozzi",
  Author = 	"Gary T. Leavens and Don Pigozzi",
  Title = 	"Typed Homomorphic Relations Extended with Subtypes",
  BookTitle =	"Mathematical Foundations of Programming Semantics '91",
  Publisher = 	"Springer-Verlag",
  Year = 	1992,
  Editor = 	"Stephen Brookes",
  Series = 	LNCS,
  Volume = 	598,
  Pages = 	"144-167",
  Address = 	NY,
  Annote = 	"17 references."
}

[7] @InCollection{Reynolds80, Key="Reynolds",
Author="John C. Reynolds",
Title="Using Category Theory to Design Implicit Conversions and Generic Operators",
BookTitle="Semantics-Directed Compiler Generation, Proceedings of a Workshop,
	Aarhus, Denmark",
Publisher="Springer-Verlag",
Series=LNCS,
Editor="Neil D. Jones",
Volume=94,
Month=Jan,
Year=1980,
Pages="211-258",
Annote="Defines category-sorted algebras which are used to avoid problems
	between implicit conversions and generics.  11 references."
}

[8] @InCollection{Reynolds85, Key="Reynolds",
Author="John C. Reynolds",
Title="Three Approaches to Type Structure",
BookTitle="Mathematical Foundations of Software Development,
	Proceedings of the International Joint Conference on
	Theory and Practice of Software Development (TAPSOFT), Berlin.
	Volume 1: Colloquium on Trees in Algebra and Programming (CAAP '85)",
Month=Mar,
Year=1985,
Pages="97-138",
Editor="Hartmut Ehrig and Christiane Floyd and Maurice Nivat and James Thatcher",
Series=LNCS,
Volume=185,
Publisher="Springer-Verlag",
Address=NY
}

[9] @Article{Schaffert-etal86, Key="Schaffert, {\em et al.\/}",
Author="Craig Schaffert and Topher Cooper and Bruce Bullis and Mike Kilian
	and Carrie Wilpolt",
Title="An Introduction to {Trellis/Owl}",
Journal=SIGPLAN,
Volume=21,
Number=11,
Month=Nov,
Year=1986,
Pages="9-16",
Note="OOPSLA '86 Conference Proceedings, Norman Meyrowitz (editor),
	September 1986, Portland, Oregon.",
Annote="Trellis/Owl is a language with multiple inheritance and static type
	checking.  It distinguishes instance from class operations,
	and private from public operations.  Subtyping as an organizational
	principle for generalization and specialization.
	Subtyping as a specification hierarchy.  Subtyping and type checking.
	Inheritance ambiguities must be explicitly resolved.
	Type generators and parameterized types.
	Other features are iterators, exception handling
	and atype case statement for checking the types of objects at run-time.
	7 references."
}