[ 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