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

[ 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 <[email protected]>
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
> [email protected]
> http://cambium.inria.fr/~fpottier/
>