[TYPES] subtyping of mutually recursive algebraic data types

[Giuseppe Castagna]

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!QYIv5kZfRZ_sM_dbcvKdrXLsHb-tjd_4jpTeLE-n3m-E8TJ2qqx4c-2QqB1nepcRXZPlaUrqjL2yHCM5-OiV$ 

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!QYIv5kZfRZ_sM_dbcvKdrXLsHb-tjd_4jpTeLE-n3m-E8TJ2qqx4c-2QqB1nepcRXZPlaUrqjL2yHFyPLk_c$ 

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