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

Re: Decidable polymorphic recursion?


Dear Josef,

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.

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

Moreover, as explained in the following papers, the decidable restriction
of polymorphic recursion described by Mycroft can be natually extended
to use rank 2 intersection.

@CONFERENCE{Jim96,
        AUTHOR="T. Jim",
        TITLE="{What are principal typings and what are they good for?}",
        BOOKTITLE="{POPL'96}",
        YEAR={1996},
        EDITOR="",
        PAGES={42--53},
        PUBLISHER={ACM}
        }

@TECHREPORT{Jim95bTR,
        AUTHOR="T. Jim",
        INSTITUTION="{LCS,
                      Massachusetts Institute of Technology}",
        TITLE="{Rank 2 type systems and recursive definitions}",
        YEAR={1995},
        NUMBER="{MIT/LCS/TM-531}"
        }

Best regards,
   Ferruccio Damiani

_____________________________________________________________________________
Dr. Ferruccio DAMIANI                   Phone:(+39) 011 670 6719
Dipartimento di Informatica             Fax  :(+39) 011 75 16 03
Universita' degli Studi di Torino       Email:damiani@di.unito.it
C.so Svizzera 185, 10149 Torino, Italy  URL  :http://www.di.unito.it/~damiani

On Tue, 8 Jan 2002, Josef Svenningsson wrote:

> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>
> Hi!
>
> Does anybody know of any work on type systems which are somewhere in
> between the Damas-Milner and the Milner-Mycroft calculus in strength? What
> I am looking for is a type system for which we can infer the types but
> still gives some kind of (but of course not full) polymorphic recursion.
> Any pointers appreciated.
>
> 	/Josef
>