[TYPES] subtyping of mutually recursive algebraic data types
Mark Sheldon
sheldon at alum.mit.edu
Fri Jun 17 12:59:56 EDT 2022
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 <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
More information about the Types-list
mailing list