[TYPES] subtyping of mutually recursive algebraic data types

[Mark Sheldon]

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 <aaronngray.lists at gmail.com> wrote:
> 
> On Fri, 17 Jun 2022 at 18:00, Mark Sheldon <sheldon at 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!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 <aaronngray.lists at 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.