[TYPES] subtyping of mutually recursive algebraic data types

[Frank Pfenning]

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.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
>


-- 
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