[Prev][Next][Index][Thread]
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 = "115",
note = " Preliminary version appeared in {\it Proc. 4th IEEE
Symposium on Logic in Computer Science\/} (1989), 9297." ,
URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/ic91.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 objectoriented programming, including hidden
instance variables and multiple inheritance, may be coded in this calculus.
We conclude that type inference is decidable for objectoriented programs,
even with multiple inheritance and classes as firstclass 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