[Prev][Next][Index][Thread]
Summary: type inference
On March 7, 1995, I sent the following question to the types list:
Question:
Consider a typed lambda-calculus with records.
Suppose that the record types are ordered by a
subtyping relation, and suppose that there is a
subsumption rule. The question of type inference
is to decide if a given unannotated program is typable.
Which papers are published about type inference
problems of this form?
Appended is a summary of the replies I have received.
Thanks to everybody who responded.
As expected, the problem has been considered by various people.
The question was asked because I noticed that the algorithms in
my LICS'94 paper for inferring object types can easily be modified
to handle also functions and records.
Jens Palsberg
Computer Science Department
Aarhus University
DK-8000 Aarhus C
Denmark
------------------------------------------
>From: Laurent Dami <dami@cui.unige.ch>
Most of the work on type inference for records has been collected
in the recent book:
Carl A. Gunter and John C. Mitchell, eds.
Theoretical aspects of OO programming:
types, semantics, and language design.
MIT Press, Foundations of computing series, 1994.
The main people involved are Mitchell Wand and Didier Remy. The
paper of Aiken&Wimmers in POPL'94 is also relevant. A WWW page
containing pointers to all those people is available at
http://cuiwww.unige.ch/OSG/Hop/types.html
Now I should also talk about my own work, not published yet, but
available on-line. I designed the "lambda-N" calculus, i.e. a
calculus with several named parameters at any abstraction level.
This can be used as a basic tool for implementing records and variants.
The HOP language, based on this calculus, is described at
http://cuiwww.unige.ch/OSG/Hop/
and a paper on type inference (with record subtyping, extensible
records and record concatenation) is available at
ftp://cui.unige.ch/pub/dami/typedLN.ps.Z
------------------------------
>From: Marcin Benke <benke@mimuw.edu.pl>
Well, it depends on what ordering between records you have in mind.
If it is coordinatewise, with underlying base ordering being a tree or
a lattice than it is solvable in P. In fact in this settings records
do not add to complexity provided by arrow.
See for example my Tech Report at
ftp://grab.mimuw.edu.pl/pub/benke/tr199.dvi
You may also access it via my home page
http://grab.mimuw.edu.pl/~benke
-------------------------------
>From: sheldon@alexandria.lcs.mit.edu (Mark A. Sheldon)
Mitch Wand at Northeastern has done a lot of work in this area. I've
been out of touch with it for a while, but I would talk to him directly
and read anything of his you can find. You could start with these older
references, but you'd probably be better off with something newer.
@inproceedings{wand87,
author = {Mitchell Wand},
title = {Complete Type Inference for Simple Objects},
booktitle = {Proceedings of the {IEEE} Symposium on
Logic in Computer Science},
year = 1987,
pages = {37--44}
}
Contains errors that were later published in 1988. I have a copy attached
to the above paper, but I don't know what IEEE publication it appeared in.
@misc{wand88,
author = {Mitchell Wand},
title = {Corrigendum: Complete Type Inference for Simple Objects},
year = 1988,
pages = {132}
}
Retraction of wand87 --- there are programs without principle types in the
system.
----------------------------------
>From: scott@blaze.cs.jhu.edu (Scott Smith)
Our type inference approach fits into this category. We have other
syntax like ref and let, but if the untyped programs don't use these
features, then our approach will fit into your category I believe. Of
course the types are in this "constraint" form. So, this might not be
what you are after since the constraints could also be recursive.
@inproceedings{Eifrig&95,
Author = "J. Eifrig and S. Smith and V. Trifonov",
Title = "Type Inference for Recursively Constrained Types and its
Application to {OOP}",
Booktitle = "Mathematical Foundations of Programming Semantics, New Orleans",
Year = "1995",
Note = "To Appear. Currently available
as {\tt ftp://ftp.cs.jhu.edu/pub/scott/ooinfer.ps.Z}"
}
Another one I can think of is
@inproceedings{Sekiguchi&94,
author = "T. Sekiguchi and A. Yonezawa",
title = "A Complete Type Inference System for Subtyped Recursive Types",
volume = 789,
series = "Lecture Notes in Computer Science",
pages = "667-686",
booktitle = "Proc. Theoretical Aspects of Computer Software",
year = 1994,
publisher = "Springer-Verlag"
}
(this version has some significant bugs).
Also, there is
@InProceedings{HS94,
author = "Andreas V. Hense and Gert Smolka",
title = "A Record Calculus with Principal Types",
journal = lncs,
year = "1994",
volume = "845",
pages = "219-236",
booktitle = "1st International Conference on Constraints in
Computational Logics",
year = "1994",
editor = "Jean-Pierre Jouannaud",
publisher = spr,
month = sep
}
@Book{Hen94,
author = "Andreas V. Hense",
title = "Polymorphic Type Inference for Object-Oriented
Programming Languages",
publisher = "Pirrot Verlag",
year = "1994",
address = {Trierer Str. 7, D-66125 Saarbr\"ucken-Dudweiler},
note = "ISBN 3-930714-00-0"
}
---------------------------
>From: lalita@graceland.ih.att.com (Lalita Jategaonkar Jagadeesan)
John Mitchell and I have a paper on this topic, in the context of
extending ML-style type inference with subtyping of records. The
reference is:
@Article{JategaonkarMi92,
author={Jategaonkar, Lalita and Mitchell, John C.},
title={Type Inference with extended pattern matching and subtypes},
journal={Fundamenta Informaticae},
volume={19},
number={1,2},
month={september/october},
year={1993},
pages={127--166},
note={An earlier version appeared in the
Proceedings of the ACM Symposium on Lisp and Functional Programming
Languages, 1988}
}
------------------------------
>From: palsberg@daimi.aau.dk (Jens Palsberg)
@InProceedings{Palsberg93b,
author = "Jens Palsberg",
title = "Efficient Inference of Object Types",
booktitle = "Proc. LICS'94, Ninth Annual IEEE Symposium on
Logic in Computer Science",
month = "Paris, France, July",
year = 1994,
pages = "186--195"}
------------------------------