# Re: Question: typing with set of most general unifiers

• To: simonc@dcs.kcl.ac.uk
• Subject: Re: Question: typing with set of most general unifiers
• From: Mitchell Wand <wand@ccs.neu.edu>
• Date: Tue, 21 Mar 1995 09:13:34 -0500
• Approved: types@dcs.gla.ac.uk

I did one example that fell into this category:  a record calculus with
concatenation (for doing multiple inheritance).  Here's the citation:

@Article{Wand91,
author = 	"Wand, Mitchell",
title = 	"Type Inference for Record Concatenation and Multiple
Inheritance",
journal = 	"Information and Computation",
year = 	"1991",
volume = 	"93",
pages = 	"1--15",
note = " Preliminary version appeared in {\it Proc. 4th IEEE
Symposium on Logic in Computer Science\/} (1989), 92--97." ,
URL =  {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/ic-91.dvi},
abstract = "We show that the type inference problem for a lambda
calculus with records, including a record concatenation operator, is
decidable.  We show that this calculus does not have principal types,
but does have finite complete sets of types: that is, for any term $M$
in the calculus, there exists an effectively generable finite set of
type schemes such that every typing for $M$ is an instance of one the
schemes in the set.

We show how a simple model of object-oriented programming, including hidden
instance variables and multiple inheritance, may be coded in this calculus.
We conclude that type inference is decidable for object-oriented programs,
even with multiple inheritance and classes as first-class values."
}

--Mitch

Mitchell Wand				      Internet: wand@ccs.neu.edu
College of Computer Science, Northeastern University
360 Huntington Avenue #161CN, Boston, MA 02115     Phone: (617) 373 2072
World Wide Web: http://www.ccs.neu.edu/home/wand   Fax:   (617) 373 5121