[ 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/ >
