[TYPES] subtyping of mutually recursive algebraic data types

[Aaron Gray]

On Thu, 23 Jun 2022 at 20:20, Mark Sheldon <sheldon at alum.mit.edu> wrote:
>
> 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.

Mark,

Thank you, this is a very long term project for me, and subtyping has
become a monster thats been tamed on many levels but still keeps
escaping, you could write a book on it alone, I am surprised no one
has done that yet :)

Regards,

Aaron

>
> 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!QAv4EtwSw_gYVTzSrqYnAM1svOt58VpLCGnhStxGVIVJTVRGfj8Wwij4pYR3JT6Rkvb5maOVIic3qaDBjZgAitRRa3g2KapfhG-5NA$ ).  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.
>


-- 
Aaron Gray

Independent Open Source Software Engineer, Computer Language
Researcher, Information Theorist, and amateur computer scientist.