[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Giuseppi, Sorry it has taken so long to get back to you theres been such a rich wealth of replies and papers. I am starting to read your two papers on Semantic Subtyping as they seem a good place to start before Set-Theoretic Types for Polymorphic Variants and Tommaso Petrucciani's PhD thesis. I have a pile of papers on sub typing I have read over the years but this and the coinduction approach are relatively new to me. CDuce looks very interesting so I will study that in conjunction with your papers. Many thanks Aaron On Sat, 18 Jun 2022 at 23:07, Giuseppe Castagna <g...@irif.fr> wrote: > > In our ICFP 16 Paper Set-Theoretic Types for Polymorphic Variants we defined > type inference for polymorphic variants with recursive set-theoretic types > (type are defined coinductively with a couple of standard restrictions). > https://urldefense.com/v3/__https://www.irif.fr/*gc/papers/icfp16.pdf__;fg!!IBzWLUs!XKdWD60h2cKWz0GzrVroGQkYYWMHIJXtEbZmQoUmf_BRSU-sEdQ6qtV93GrJXQ0es1B5E_jW5c_2BELiElxdKqHpQnSA9LIEDfuiNg$ > > > More generally, you may want to refer to Tommaso Petrucciani's PhD thesis > Polymorphic set-theoretic types for functional languages which studies type > inference for recursive set-theoretic types (they can encode ADT' s via > products and unions), which uses and improves some results of Stephen Dolan' > s PhD thesis as well as of the paper cited above. > https://urldefense.com/v3/__http://www.theses.fr/2019USPCC067__;!!IBzWLUs!XKdWD60h2cKWz0GzrVroGQkYYWMHIJXtEbZmQoUmf_BRSU-sEdQ6qtV93GrJXQ0es1B5E_jW5c_2BELiElxdKqHpQnSA9LKwx3nBHQ$ > > > Hope it is useful > > Cheers > > Beppe > > > On 17/06/2022 09.40, Aaron Gray 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