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:
>        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:  

   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:
>        AUTHOR="F. Henglein",
>        TITLE="{Type reconstruction in the presence of polymorphic
>                recursion}",
>        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 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