[TYPES] Has anyone seen a language with sub-typing and recursive parametric type aliases?

[Benjamin Lichtman]

Hello all,

TypeScript team member here.
This example actually is supported by TypeScript.
See here for a demonstration.
<http://www.typescriptlang.org/play/index.html?ssl=40&ssc=1&pln=39&pc=57#code/MYewdgzgLgBBMF4YG8C+MA+GYCIcG4BYAKBKgE8AHAUxgBkBLaAHgBUA+RFEmXmAC2oBDACYAuGKwA0PPlCEMANhMYsOJdNjABXRYqKliFGjACSYKNQDm1AE6rYSZLN6DREnQFsARnZnE+GHklCXNLG3smKBc4bU8PON9bDUwYHT0DElBIWGUzC2s7By5nAL43cRgAVn9A4Lz0xVq+CDiJKo1M4mzoGEUAJhUo5i8kziRFGCF4MMLI6C7jWgBRAA9KRRARBjArBzZx7jLXYUrpGOp1zZFqCTWNrZ294fvrp-2OdhStXX0SMiotFmEVeIAgDHAJRiFQSPj8FyuW1uMFB212+2BdlB4PA7GavFa8TSiTs32JGX+3XAvWRmNs2IhYChxwEp3a+JglweNwSeg5hPanUpPVg1EGKMRaOeLFGdkOtGm+XCWMROLABiAA>


Best,
Ben

On Tue, Feb 18, 2020 at 1:14 PM Martin Abadi <abadi at cs.ucsc.edu> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Hello,
>
> TypeScript <https://www.typescriptlang.org/> has parameterized recursive
> definitions and structural subtyping. The language has evolved over time,
> and I am afraid I have not looked at the current definitions, but, early
> on, the designers were aware of some of the algorithmic difficulties
> that François Pottier mentions and introduced restrictions to avoid them. I
> don't know whether the examples of interest to Isaac Oscar Gariano would be
> expressible.
>
> Regards,
>  Martin
>
>
> On Tue, Feb 18, 2020 at 10:36 AM François Pottier <
> francois.pottier at inria.fr>
> wrote:
>
> > [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list
> > ]
> >
> >
> > Hello,
> >
> > If I am not mistaken, already deciding the *equivalence* of two types
> > in the presence of recursive and parameterized type abbreviations is
> > extremely costly: Marvin Solomon proved it equivalent to the DPDA
> > equivalence problem ("Type definitions with parameters", POPL'78).
> >
> > --
> > François Pottier
> > francois.pottier at inria.fr
> > http://cambium.inria.fr/~fpottier/
> >
>