[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Fri, 17 Jun 2022 at 18:00, Mark Sheldon <shel...@alum.mit.edu> wrote: > > We deal with this topic in our book, Design Concepts in Programming Languages > (https://urldefense.com/v3/__https://mitpress.mit.edu/books/design-concepts-programming-languages__;!!IBzWLUs!VMszV1CswUJMokl4bq4nZ2MiwksJZ8Yv9-8MP3BH1wxJXGi_EuLL1aoglnuW3Ox9O6RYStjSg30TbV4z0GKs7OlslS5BDu4RWPR2mA$ > ). See Chapter 12. There is a section on “Subtyping of Recursive Types on > pages 706–707, Mark, thank you I have ordered a copy of your book, I have a copy of TAPL but Chapter 12 seems pretty limited. Thanks for the other two papers, Aaron > > Here are relevant references given in the Notes section of Chapter 12 on page > 767: > > Kozen, Palsberg, Schwartzbach. Efficent recursive subtyping. POPL 93. > Gapayev, Levin, Pierce. Recursive subtyping revealed. ICFP 00. > Pierce. Types and Programming Languages. MIT Press. 2002. Chapter 12. > > > I hope this is useful! > > -Mark > > Mark A. Sheldon > Associate Teaching Professor > Department of Computer Science > Tufts University > > On 17Jun, 2022, at 03:40, Aaron Gray <aaronngray.li...@gmail.com> wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I am interested if there is any work on the subtyping of mutually > recursive algebraic data types. I am wanting an algorithm for purposes > of implementing an object oriented programming language with ADT's > which lower onto a virtual class implementation which can support > mutually recursive behavior, but need the typ checking and inference > at the ADT level. > > Theres a number of papers and projects in this area I have came across > but none of them actually tackle algebraic data types properly let > alone mutually recursive ones. > > A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. > > - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre > and Christophe Raffalli - subml - > https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ > - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and > simple-sub implementation - > https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ > - A Mechanical Soundness Proof for Subtyping Over Recursive Types > Timothy Jones David J. Pearce - > https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ > > None of these seem to deal with mutually recursive data types. > > I am interested in the papproach of using codata/coinduction and > coalgebras and possibly bisimulation in order to deal with the > mutually recursive nature of real world mutually recursive algebraic > data types like for instance AST's of real world complex computer > languages. > > Any projects, papers, thoughts, or implementations would be of interest. > > Regards, > > Aaron > > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist.