[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
You might find our recent ESOP paper relevant: Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning: Polarized Subtyping. ESOP 2022: 431-461 https://urldefense.com/v3/__https://link.springer.com/chapter/10.1007/978-3-030-99336-8_16__;!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwzqkdvV8$ There are some further references in that paper in the related work section. A version with polymorphism, but without explicit polarization (essentially: all types are interpreted coinductively because they are session types) can be found in Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning: Subtyping on Nested Polymorphic Session Types. CoRR abs/2103.15193 (2021) https://urldefense.com/v3/__https://arxiv.org/abs/2103.15193__;!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwMw8Y7mY$ There we show that a natural formulation of the problem in the presence of polymorphism is undecidable, but also give an algorithm that has performed well for us in practice. - Frank On Fri, Jun 17, 2022 at 9:11 AM Aaron Gray <aaronngray.li...@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 > -- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp__;fg!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwrgSsDME$ +1 412 268-6343 GHC 6017
