[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
