[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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!UeVFMEtYt8ckfm-t6zKFlGaiVtH17ToAFSrNnbbzCRByAVfFL8Wqo1XYb-zSLszkXmc_8vnfzc_F6OJH3va6LwopH_nYGc2Q$ <https://urldefense.com/v3/__https://mitpress.mit.edu/books/design-concepts-programming-languages__;!!IBzWLUs!UeVFMEtYt8ckfm-t6zKFlGaiVtH17ToAFSrNnbbzCRByAVfFL8Wqo1XYb-zSLszkXmc_8vnfzc_F6OJH3va6LwopH_nYGc2Q$ >). See Chapter 12. There is a section on “Subtyping of Recursive Types on pages 706–707, 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 <[email protected]> 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
