[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi, Aaron, I’m honored! :-) I didn’t mean to make a sales pitch — I figured if you had access to a copy it might help, and if not, the references would do it. Others have provided some more recent references, too, and I hope you’re making progress. Thanks, and I hope you find our book a useful addition to your collection! -Mark > On 23Jun, 2022, at 11:29, Aaron Gray <[email protected]> wrote: > > On Fri, 17 Jun 2022 at 18:00, Mark Sheldon <[email protected]> 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!TJHPwJx6mfjdKduqLQoPQCY45K3obf1hr7CB-4Xw0Iy0-6oRFCtaHvPsq7SP6VflJQzBGmSZBbPNycoz7HQBbGPjpO18glvJ$ >> ). 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 <[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 >> >> > > > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language > Researcher, Information Theorist, and amateur computer scientist.
