[TYPES] subtyping of mutually recursive algebraic data types

[Aaron Gray]

Matthew,

Thank you for showing me Motoko's implementation, sorry its taken me
so long to get back to you but theres been a wealth of replies, and
still a lot to look at properly.

Motoko looks like very neat and reasonably small SML code, so I will
take a proper look at it  Its interesting to me as it implements
lattice like/based LUB and GLB code, which is how I am intending on
implementing the core of the type system as well, and with kinds and
interval types.

I was originally looking for the use of coinduction for solving
subtyping for mutually recursive datatypes which Frank's paper and
implementation gives, so am looking at that currently still.

Regards,

Aaron




On Sun, 19 Jun 2022 at 00:15, Matthew A. Hammer
<matthew.hammer at gmail.com> wrote:
>
> PS: There's also a playground online to support experiments in the
> browser, and no downloading:
> https://urldefense.com/v3/__https://m7sm4-2iaaa-aaaab-qabra-cai.raw.ic0.app/__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTpUlGb3Tg$ 
>
> And I realize that URL is starting out looking quite strange, even
> before mailing list mangling.  The playground is partially written in
> Motoko itself, and is running on "Web3", so that's why.  You can see
> the source on good old Web2, here:
> https://urldefense.com/v3/__https://github.com/dfinity/motoko-playground__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTo18VoVVg$ 
>
> Happy to talk further, if it seems interesting or you have questions.
>
> Kind wishes,
> Matthew
>
> On Sat, Jun 18, 2022 at 5:08 PM Matthew A. Hammer
> <matthew.hammer at gmail.com> wrote:
> >
> > Hi Aaron,
> >
> > Due to oddities of the mailing list, I didn't get the original message
> > you sent, but from the title and other responses that quote you, I see
> > that you are currently involved in designing a new OO language with
> > FP-style data types, and subtyping.
> >
> > Have you given Motoko a look?
> >
> > In either case, I wonder how it compares to the vision you have.
> >
> > If you are curious about the type system and subtyping checks, I'd
> > start here: (hopefully these URLs stay usable; I worry.)
> > https://urldefense.com/v3/__https://github.com/dfinity/motoko/blob/master/src/mo_types/type.mli__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTpSGErMkA$ 
> >
> > And here:
> > https://urldefense.com/v3/__https://github.com/dfinity/motoko/blob/master/src/mo_types/type.ml__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTpYJ_e7DQ$ 
> >
> > The general sales pitch and some small examples are here:
> > https://urldefense.com/v3/__https://internetcomputer.org/docs/current/developer-docs/build/languages/motoko/__;!!IBzWLUs!WgY_4vSpPi0jgq_qGkVH35MzzXX63D112L28FuPqcfEjHvkU_CsX-zWRluiPZcYefOgW5zCifZIHBzeFnriASFsur_vJxTpFfIFV4w$ 
> >
> > The compiler repo has lots of tests with more examples that
> > demonstrate how the language and typing work.  See the .mo files under
> > tests.
> >
> > My team implemented the subtyping check, which I understand from
> > talking with them that it is tricky.  I'm not familiar with the
> > internals myself, but you could reach out to Andreas Rossberg, Claudio
> > Russo and Joachim Breitner who did that work (and most other parts of
> > the language design and implementation).
> >
> > KInd wishes,
> > Matthew
> >
> > On Sat, Jun 18, 2022 at 8:09 AM Frank Pfenning <fp at cs.cmu.edu> wrote:
> > >
> > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> > >
> > > You  might find our recent ESOP paper relevant:
> > >
> > > Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning:
> > > Polarized Subtyping. ESOP 2022: 431-461
> > > https://urldefense.com/v3/__https://link.springer.com/chapter/10.1007/978-3-030-99336-8_16__;!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwzqkdvV8$
> > >
> > > There are some further references in that paper in the related work section.
> > > A version with polymorphism, but without explicit polarization
> > > (essentially: all types
> > > are interpreted coinductively because they are session types) can be found
> > > in
> > >
> > > Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning:
> > > Subtyping on Nested Polymorphic Session Types. CoRR abs/2103.15193 (2021)
> > > https://urldefense.com/v3/__https://arxiv.org/abs/2103.15193__;!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwMw8Y7mY$
> > >
> > > There we show that a natural formulation of the problem in the presence of
> > > polymorphism
> > > is undecidable, but also give an algorithm that has performed well for us
> > > in practice.
> > >
> > >   - Frank
> > >
> > > On Fri, Jun 17, 2022 at 9:11 AM 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
> > > >
> > >
> > >
> > > --
> > > Frank Pfenning, Professor
> > > Computer Science Department
> > > Carnegie Mellon University
> > > Pittsburgh, PA 15213-3891
> > >
> > > https://urldefense.com/v3/__http://www.cs.cmu.edu/*fp__;fg!!IBzWLUs!QrMnoLw8qFRxtzf2zu5w8Gc14aO6rhn_cCBMv4Q0dczTVPBFrRikSVu7fiARjhLIovnBm3oBBgYJ2dYwrgSsDME$
> > > +1 412 268-6343
> > > GHC 6017



--
Aaron Gray

Independent Open Source Software Engineer, Computer Language
Researcher, Information Theorist, and amateur computer scientist.