Feature request: lift the circular constraint for conditional types

[dead-claudia]

Search Terms

circular type conditional type

Suggestion

Currently, Last1 is valid, but seemingly-equivalent Last2 is not:

type Head<T extends any[]> = T extends [infer X, ...any[]] ? X : never;

type Tail<T extends any[]> =
 ((...x: T) => void) extends ((x: any, ...xs: infer XS) => void) ? XS : never;

type Last1<T extends any[]> = {
 0: never,
 1: Head<T>,
 2: Last1<Tail<T>>,
}[T extends [] ? 0 : T extends [any] ? 1 : 2];

type Last2<T extends any[]> =
 T extends [] ? never :
 T extends [infer R] ? R :
 Last2<Tail<T>>;

My suggestion is to make Last2 valid, since the recursion isn't necessarily unbounded.

Use Cases

It'd make recursive conditional types a lot easier and more intuitive to write. It'd also eliminate the need to guard against impossible cases when using the workaround like when using Last1 above. If you wanted to mandate termination, all I'd want is direct recursion - this makes it much easier to check for infinite recursion. (Other types are generally assumed to terminate, so you're only assessing control flow.)

Examples

See above in the suggestion summary. Here's a concrete example of how this file (with dependency) would be simplified:

type Last<L extends any[], D = never> =
 L extends [] ? D :
 L extends [infer H] ? H :
 ((...l: L) => any) extends ((h: any, ...t: infer T) => any) ? Last<T> :
 D;

type Append<T extends any[], H> =
 ((h: H, ...t: T) => any) extends ((...l: infer L) => any) ? L : never;

type Reverse<L extends any[], R extends any[] = []> =
 ((...l: L) => any) extends ((h: infer H, ...t: infer T) => any) ?
 Reverse<T, Append<R, H>> :
 R;

type Compose<L extends any[], V, R extends any[] = []> =
 ((...l: L) => any) extends ((a: infer H, ...t: infer T) => any) ?
 Compose<T, H, Append<R, (x: V) => H>> :
 R;

export type PipeFunc<T extends any[], V> =
 (...f: Reverse<Compose<T, V>>) => ((x: V) => Last<T, V>);

Currently, you could achieve similar via this, but as you can see, it's highly repetitive and boilerplatey:

type Last<L extends any[], D = never> = {
 0: D,
 1: L extends [infer H] ? H : never,
 2: ((...l: L) => any) extends ((h: any, ...t: infer T) => any) ? Last<T> : D,
}[L extends [] ? 0 : L extends [any] ? 1 : 2];

type Append<T extends any[], H> =
 ((h: H, ...t: T) => any) extends ((...l: infer L) => any) ? L : never;

type Reverse<L extends any[], R extends any[] = []> = {
 0: R,
 1: ((...l: L) => any) extends ((h: infer H, ...t: infer T) => any) ?
 Reverse<T, Append<R, H>> :
 never,
}[L extends [any, ...any[]] ? 1 : 0];

type Compose<L extends any[], V, R extends any[] = []> = {
 0: R,
 1: ((...l: L) => any) extends ((a: infer H, ...t: infer T) => any) ?
 Compose<T, H, Append<R, (x: V) => H>>
 : never,
}[L extends [any, ...any[]] ? 1 : 0];

export type PipeFunc<T extends any[], V> =
 (...f: Reverse<Compose<T, V>>) => ((x: V) => Last<T, V>);

(The original code snippet is linked to from here as a possible solution to the issue of _.compose, _.flow, and friends.)

Checklist

My suggestion meets these guidelines:

• This wouldn't be a breaking change in existing TypeScript / JavaScript code
• This wouldn't change the runtime behavior of existing JavaScript code
• This could be implemented without emitting different JS based on the types of the expressions
• This isn't a runtime feature (e.g. new expression-level syntax)

[dead-claudia]

BTW, here's the Wikipedia article on total functional programming, where TS's type system models to a very large extent in my experience (probably unintentionally). And yes, this could enable a type-encoded quicksort across integers and potentially strings if they were made comparable, without even requiring the type system to remain Turing-complete.

---

After including this, you could then permanently break the Turing-complete aspect by making a similar check with indexed types. Note that AFAICT, the Turing-complete nature is dependent on indexed types not being checked for recursive cases. It may require support for corecursive functions, depending on how much code breaks.

[dead-claudia]

Oh, and another reason to address Turing completeness and potentially kill it is because the original "solution" to variadic composition happens to hang when plugged into the playground, due to a bug not very clear when just looking. It maxes out my computer's CPU without taking much memory at all, which is a pretty obvious problem, but it can happen when a type system is Turing-complete, but not sound enough to force you to be explicit about your intent (you see similar with C-like procedural languages and infinite loops with non-trivial logic, hence various control-flow-sensitive lints for it).

[jcalz]

(Moving the conversation from #5453)

Regarding the Last1<> implementation, the official word is something like "don't do it". Anders Hejlsberg (@ahejlsberg) said:

It's clever, but it definitely pushes things well beyond their intended use. While it may work for small examples, it will scale horribly. Resolving those deeply recursive types consumes a lot of time and resources and might in the future run afoul of the recursion governors we have in the checker.

Don't do it!

I would be enormously in favor of something that lets me express more recursive type functions without running afoul of the current pitfalls (warnings, hanging compiler, crashing compiler). Not sure how to get there from here, though. I suspect if the circularity warning were simply removed, the Last2<> implementation would bog down the compiler in the same way that Last1<> does. Assuming that the type checker sometimes treats T extends U ? X : Y like X | Y for testing assignability, any recursion that depends on conditional types to express termination could be a problem.

I'm not holding my breath for any solution involving a significant overhaul of the type checker. Can we think of some addition which wouldn't break existing code but would allow some (bounded) type function iteration/recursion?

[jcalz]

Copying from the Design Notes for ease of linking.

Daniel Rosenwasser (@DanielRosenwasser) said:

Recursive Types

• The intuition is not possible to form object graphs with circularities unless you defer somehow (either via laziness or state).
• Really there's no way to know if any arbitrary type will terminate.
• We can have limited types of recursion in the compiler, but the problem isn't whether or not the type terminates, it's how computationally intensive and memory heavy the resolution is.
• We have a meta-question: do we want people writing code like this?
  • The motivating scenarios that people have are legitimate, but achieving them with these types is not necessarily going to work well for library consumers.
• Conclusion: we're not quite ready for this sort of thing.