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

Re: Question: typing with set of most general unifiers


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