Pick a lane

rfcs/recursive-type-unrestriction.md

@@ -45,11 +45,81 @@ Examples like this are quite common in TypeScript code, for example in [ReduxJS]
 
 ## Design
 
-*This section to be filled in once we decide which alternative to use*
+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<a1,...,aN>`, if we encounter a recursive use
+`T<U1,...,UN>` we proceed as follows:
+
+* If every `UI` is `aI`, or if every `UI` does not contain any of the `aJ`s:
+    * look `<U1,...,UN>` 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 `<U1,...,UN>` and value `X`, unify `X` with
+  the result of expanding `T<U1,...,UN>`.
+
+* expanding `T<U1,...,UN>` may encounter a generic function,
+  for example `<b>(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<a> = { data: a, children: {Tree<a>}, map: <b>(a -> b) -> Tree<b> }
+```
+
+The type alias is `Z` where
+
+```
+  Z = { data: a, children: {Z}, map: <b>(a -> b) -> X }
+```
+
+the cache contains
+
+```
+  <b> |-> X
+```
+
+and after unification
+
+```
+  X = { data: b, children: {X}, map: <c>(b -> c) -> Y }
+```
+
+which introduces a new cache entry
+
+```
+  <c> |-> Y
+```
+
+and after unification
+
+```
+  Y = { data: b, children: {Y}, map: <b>(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
 
-*This section to be filled in once we decide which alternative to use*
+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<a, b> = { this: a, that; b, children : {T<number, b>} }
+```
+
+This algorithm does not support type graphs with infinite expansions.
 
 ## Alternatives
 
@@ -82,7 +152,7 @@ recursive types are defined, and used when types are used recursively.
 
 For example:
 ```
-type T<a,b> = { foo: T<b,number>? } 
+type T<a,b> = { foo: T<b,number>? }
 ```
 would result in cache entries:
 ```
@@ -92,7 +162,7 @@ T<number,number> = { foo: T<number,number>? }
 ```
 This can result in exponential blowup, for example:
 ```
-type T<a,b> = { foo: T<b,number>?, bar: T<b,string>? } 
+type T<a,b> = { foo: T<b,number>?, bar: T<b,string>? }
 ```
 would result in cache entries:
 ```
@@ -109,12 +179,12 @@ 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<a> = { foo: T<Promise<a>>? } 
+type T<a> = { foo: T<Promise<a>>? }
 ```
 results in an infinite type graph with cache:
 ```
-T<a> = { foo: T<Promise<a>>? } 
-T<Promise<a>> = { foo: T<Promise<Promise<a>>>? } 
+T<a> = { foo: T<Promise<a>>? }
+T<Promise<a>> = { foo: T<Promise<Promise<a>>>? }
 T<Promise<Promise<a>>> = { foo: T<Promise<Promise<Promise<a>>>>? }
 ...
 ```
@@ -128,15 +198,15 @@ We can use occurrence checks to ensure there's less blowup. We can restrict
 a recursive use `T<U1,...,UN>` in the definition of `T<a1...aN>` so that either `UI` is `aI`
 or contains none of `a1...aN`. For example this bans
 ```
-type T<a> = { foo: T<Promise<a>>? } 
+type T<a> = { foo: T<Promise<a>>? }
 ```
 since `Promise<a>` is not `a` but contains `a`, and bans
 ```
-type T<a,b> = { foo: T<b,number>? } 
+type T<a,b> = { foo: T<b,number>? }
 ```
 since `a` is not `b`, but allows:
 ```
-type T<a,b> = { foo: T<a,number>? } 
+type T<a,b> = { foo: T<a,number>? }
 ```
 
 This still has exponential blowup, for example