From d31ed9665a564489badad5a0f1a7f849a48b2cd4 Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Mon, 30 Oct 2023 15:25:03 -0500 Subject: [PATCH] Add recursive-type-unrestriction.md --- docs/recursive-type-unrestriction.md | 222 +++++++++++++++++++++++++++ 1 file changed, 222 insertions(+) create mode 100644 docs/recursive-type-unrestriction.md diff --git a/docs/recursive-type-unrestriction.md b/docs/recursive-type-unrestriction.md new file mode 100644 index 0000000..4d9e368 --- /dev/null +++ b/docs/recursive-type-unrestriction.md @@ -0,0 +1,222 @@ +# Loosening the recursive type restriction + +## Summary + +Luau supports recursive type aliases, but with an important +restriction: users can declare functions of recursive types, but *not* +recursive type functions. This has problems with sophisticated uses of +types, for example ones which mix recursive types and nested generics. +This RFC proposes loosening this restriction. + +## Motivation + +Luau supports recursive type aliases, but with an important restriction: +users can declare functions of recursive types, such as: +```lua + type Tree = { data: a, children: {Tree} } +``` +but *not* recursive type functions, such as: +```lua + type TreeWithMap = { ..., map: (a -> b) -> Tree } + +``` +These examples come up naturally in OO code bases with generic types, for example +```lua +--!strict +export type PromiseFor = { + andThen: ( + self: PromiseFor, + onFulfilled: ((result: T) -> U)?, + onRejected: ((err: string) -> U)? + ) -> PromiseFor, + catch: ( + self: PromiseFor, + onRejected: ((err: string) -> U)? + ) -> PromiseFor, + finally: ( + self: PromiseFor, + onResolvedOrRejected: ((wasFulfilled: boolean, resultOrErr: T | string) -> U) + ) -> PromiseFor, +} +``` +as discussed at the [Roblox DevForum](https://devforum.roblox.com/t/regression-with-genericrecursively-defined-types/1616647). + +Examples like this are quite common in TypeScript code, for example in [ReduxJS](https://github.com/reduxjs/redux-thunk/blob/master/src/types.ts). + +## Design + +The design is to continue to use strict type aliases, but to use a +cache during type alias definition. Type aliases are handled as they +currently are, except for recursive cases. + +When defining a type alias `T`, if we encounter a recursive use +`T` we proceed as follows: + +* If every `UI` is `aI`, or if every `UI` does not contain any of the `aJ`s: + * look `` up in the cache, + * if the cache lookup succeeds, return the cached result, + * otherwise create a fresh type variable, add it to the cache, and return it. + +* Otherwise, produce a type error and return an error type. + +Once we are finished defining the type alias, iterate through the cache + +* for each entry with key `` and value `X`, unify `X` with + the result of expanding `T`. + +* expanding `T` may encounter a generic function, + for example `(S) -> R`, which needs a bit of care, since `a` may occur free in + some of the `Ui`. We need to rename `b` to `c`, but this renaming may also + introduce new cache entries, since any cache entry for `U` containing `c` + needs a new cache entry for `U[c/b]`. + +For example, with type + +``` + type TreeWithMap = { data: a, children: {Tree}, map: (a -> b) -> Tree } +``` + +The type alias is `Z` where + +``` + Z = { data: a, children: {Z}, map: (a -> b) -> X } +``` + +the cache contains + +``` + |-> X +``` + +and after unification + +``` + X = { data: b, children: {X}, map: (b -> c) -> Y } +``` + +which introduces a new cache entry + +``` + |-> Y +``` + +and after unification + +``` + Y = { data: b, children: {Y}, map: (c -> b) -> X } +``` + +This algorithm can be generalized to handle mutual recursion, by using a cache for each mutually recursive type. + +This design is the strictest one we came up with that copes with the examples we're interested in, in particular the `PromiseFor` example. + +## Drawbacks + +Renaming can double the size of the type graph, with the result that nested type aliases can result in exponential blowup. + +This algorithm doesn't cope with examples which mix concrete and generic types +``` + type T = { this: a, that; b, children : {T} } +``` + +This algorithm does not support type graphs with infinite expansions. + +## Alternatives + +### Lazy recursive type instantiations + +The most permissive change would be to make recursive type +instantiation lazy rather than strict. In this approach `T` would +not be instantiated immediately, but only when the body is needed. In +particular, during unification we can unify `T` with `T` by +first trying to unify `U` and `V`, and only if that fails try to unify +the instantiations. + +*Advantages*: this allows recursive types with infinite expansions like: +```lua + type Foo = { ..., promises: {Foo>} } +``` + +### Lazy recursive type instantiations with a cache + +As above, but keep a cache for each type function. + +*Advantages*: reduces the size of the type graph. + +### Strict recursive type instantiations with a cache + +Rather than lazily instantiating type functions when they are used, we +could carry on instantiating them when they are defined, and use a +cache to reuse them. In particular, the cache would be populated when the +recursive types are defined, and used when types are used recursively. + +For example: +``` +type T = { foo: T? } +``` +would result in cache entries: +``` +T = { foo: T? } +T = { foo: T? } +T = { foo: T? } +``` +This can result in exponential blowup, for example: +``` +type T = { foo: T?, bar: T? } +``` +would result in cache entries: +``` +T = { foo: T?, bar: T? } +T = { foo: T?, bar: T? } +T = { foo: T?, bar: T? } +T = { foo: T?, bar: T? } +T = { foo: T?, bar: T? } +T = { foo: T?, bar: T? } +T = { foo: T?, bar: T? } +``` +Applying this to a type function with N type variables results in more than 2^N +types. Because of blowup, we would need a bound on cache size. + +This can also result in the cache being exhausted, for example: +``` +type T = { foo: T>? } +``` +results in an infinite type graph with cache: +``` +T = { foo: T>? } +T> = { foo: T>>? } +T>> = { foo: T>>>? } +... +``` + +*Advantages*: types are computed strictly, so we don't have to worry about lazy types +producing unbounded type graphs during unification. + +### Strict recursive type instantiations with a cache and an occurrence check + +We can use occurrence checks to ensure there's less blowup. We can restrict +a recursive use `T` in the definition of `T` so that either `UI` is `aI` +or contains none of `a1...aN`. For example this bans +``` +type T = { foo: T>? } +``` +since `Promise` is not `a` but contains `a`, and bans +``` +type T = { foo: T? } +``` +since `a` is not `b`, but allows: +``` +type T = { foo: T? } +``` + +This still has exponential blowup, for example +```lua +type T = { + p1: T, + p2: T, + ... + pN: T, +} +``` + +*Advantages*: types are computed strictly, and may produce better error messages if the occurs check fails.