[TYPES] subtyping of mutually recursive algebraic data types

[Roberto Di Cosmo]

Dear Aaron,
   probably not exactly what you are looking for, but this old article that
addresses subtyping of recursive types may contain some useful piece of
information.

Roberto Di Cosmo, François Pottier, and Didier Rémy. Subtyping recursive
types modulo associative commutative products. Typed Lambda Calculus and
Applications, 2005, https://urldefense.com/v3/__http://dx.doi.org/10.1007/11417170_14__;!!IBzWLUs!W56eVak-fIjNK6SjoBie6PabAIqpQ2eJspOLTnNw5nIhHa4vYvun3qyAgz-hLNyiR4KFU7v7RxzWu8WcPm3w43kqOf_G$ 
You can get a green open access copy here:
https://urldefense.com/v3/__https://hal.archives-ouvertes.fr/hal-00149563__;!!IBzWLUs!W56eVak-fIjNK6SjoBie6PabAIqpQ2eJspOLTnNw5nIhHa4vYvun3qyAgz-hLNyiR4KFU7v7RxzWu8WcPm3w49yEkAm1$ 

Cheers

--
Roberto


On Fri, 17 Jun 2022 at 09: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
>