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