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

[Isaac]

Dear Ben,
Thank you!
I've looked at the source code for the type-script type-checker (https://github.com/microsoft/TypeScript/blob/master/src/compiler/checker.ts), and it appears to be doing two things:

  *   If the type-aliases are the same (i.e. if computing A<T1, ..., Tn> sub-type of A<Y1, ..., Yn>) than it infers the variance of the type-paramaters of A (by using the getAliasVariances function), and then checks each Ti and Yi against this variance information.
  *   If a sub-typing check involving the same type-alias recurs 5 times, it simply returns true (this is done by the isDeeplyNestedType function).

So my ExplodingList example is excepted as it uses variance to infer that ExplodingList<T> is a sub-type of ExplodingList<Y> if T is a sub-type of Y; and so it deduces that
ExplodingList<IntegerExplosion> is a sub-type of ExplodingList<ExplodingList<number>> since by the con-inductive hypothesis, IntegerExplosion is a sub-type of ExplodingList<Number>.

However this variance check dosn't occur if the type-aliases are different but just happen to have the same structure, e.g.
type ExplodingList1<T> = { head: T, explode: ExplodingList1<ExplodingList1<T>> };
type ExplodingList2<T> = { head: T, explode: ExplodingList2<ExplodingList2<T>>};

When checking if ExplodingList1<number> is a sub-type of ExplodingList2<number> it simply hits the recursion limit of 5 and returns true.

Obviously this recursion depth limit is unsound, consider the following two examples:
type A<T1, T2, T3, T4, T5> = { head: T1, tail: A<T2, T3, T4, T5, T1> }
type B<T1, T2, T3, T4, T5> = { head: T1, tail: B<T2, T3, T4, T5, T1> }
function sub1(x: A<number, number, number, number, string>): B<number, number, number, number, number> { return x }

type N<Y> = { head: Y }
function sub2(x: N<N<N<N<N<string>>>>>): N<N<N<N<N<number>>>>> { return x }

Both are accepted as well-typed by type-script. What I find interesting is the second example does not actually involve recursive types, yet it still hits the limit; this is because type-script simply checks whether it's already in a sub-typing check of the same alias-name (in this case N) even if these uses of "N" are unrelated.

I can think of refining this test in two ways to reject the above examples, but I'm sure there are many more that it will still accept:

  *   Make the recursion depth limit be relative to the number of type-parameters (so the cycling trick of my first example would be rejected)
  *   Only count applications of the type-alias that came from the same place in the program (so any recursive applications of A<...> sub-type of B<...> where the A and B applications came from the "tail" field will count towards the recursion limit, but N<...> sub-type of N<...> will not if the "N"s came from different locations in the type signature of "sub2"). The idea is that the recursion limit will only hit if it is actually the result of a type-alias being recursive (and not just having a nested application like my N example).

Let me know if my understanding of type-script is incorrect!

— Isaac Oscar Gariano​

________________________________
From: Types-list <types-list-bounces at LISTS.SEAS.UPENN.EDU> on behalf of Benjamin Lichtman <blichtman623 at gmail.com>
Sent: 19 February 2020 11:14 AM
To: Martin Abadi <abadi at cs.ucsc.edu>
Cc: types-list at lists.seas.upenn.edu <types-list at lists.seas.upenn.edu>
Subject: 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 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/
> >
>