[Prev][Next][Index][Thread]
Re: Decidable polymorphic recursion?
At 1/9/2002 09:57 AM +0100, Ferruccio DAMIANI wrote:
>[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>A decidable type system, between the Damas-Milner and the Milner-Mycroft
>calculus in strength, is already described in Mycroft's original paper:
>
>@CONFERENCE{Myc84,
> AUTHOR="A. Mycroft",
> TITLE="{Polymorphic Type Schemes and Recursive Definitions}",
> BOOKTITLE="{International Symposium on Programming}",
> YEAR={1984},
> EDITOR=" ",
> PAGES={217--228},
> PUBLISHER={Springer},
> SERIES={LNCS 167}
> }
>
>at page 226.
It is worth pointing out the POPL 1983 paper by Lambert Meertens:
@inproceedings{me83,
AUTHOR = "Meertens, L.",
BOOKTITLE = "Proc. 10th ACM Symp. on Principles of Programming
Languages (POPL)",
ENTRYDATE = "7/18/87",
KEY = "Meertens",
PAGES = "265-275",
TITLE = "Incremental Polymorphic Type Checking in {B}",
YEAR = "1983"}
The language B (later ABC) had polymorphic recursion (and a number of
other wonderful programming facilities, such as usable online
syntax-directed editing, powerful bulk types such as sorted lists and
associative maps). Meertens first gives a semi-algorithm AA and then
adds a check to arrive at a (terminating) type inference algorithm for
B. In my thesis I have shown that semiunification can be reduced to
type inference in B (which has no higher-order functions or nested
definitions) -- which we take to be defined by AA -- and that
Meertens' second algorithm is sound, but not complete wrt. AA.
Coincidentally, it is the above two papers that motivated my own work
on polymorphic recursion 14 years ago: I figured it'd take me
something on the order of a week to apply the techniques of the latter
to the problem of the former (what I then termed Milner-Mycroft
typability). Well, it turned out differently.
>Another restriction, based on the notion of "size-bounded typing"
>is presented in the paper:
>
>@ARTICLE{Hen93,
> AUTHOR="F. Henglein",
> TITLE="{Type reconstruction in the presence of polymorphic
> recursion}",
> JOURNAL=TOPLAS,
> YEAR={1993},
> VOLUME={15},
> NUMBER={2},
> PUBLISHER={ACM},
> PAGES={253--289}
> }
Just for the record: The title is actually "Type inference with
polymorphic recursion". The title above is from the article by
Kfoury, Tiuryn, Urzyczyn in the same issue of TOPLAS.
Fritz
------------------------------------------------------------------------
Fritz Henglein, Ph.D., Assoc. Prof. Email: henglein@it.edu
The IT University of Copenhagen Tel.: +45-38 16 88 88 (ITU)
Glentevej 67 Tel.: +45-38 16 88 21 (office)
DK-2400 Copenhagen Fax: +45-38 16 88 99 (ITU)
Denmark URL: http://www.it.edu
------------------------------------------------------------------------