Search Terms

generic indexed access type dependent function
generic narrowing

Suggestion

TypeScript does not provide dependent types, but by combining various features such as unions, literal types and indexed access types we can obtain fairly similar behaviour to a dependent function from the caller point of view. Unfortunately, the implementer of such functions is faced with either the possibility of creating unsoundness (pre 3.5) or forced to assert the return type with unsound features (post 3.5). There are some differences with typical dependent functions, which is why we call these dependent-type-like functions.

This suggestion proposes an addition to the typechecking part of TypeScript, which aids the programmer in writing dependent-type-like functions. The main attractive point of this suggestion is that it does not introduce any additional syntax, and is meant to be a conservative extension. Thus it is not a breaking change with regards to the changes introduced in 3.5, but it does enable certain sound scenarios to typecheck.

Use Case

The main use case is dependent-type-like functions, the depLikeFun example is a minimalistic scenario showcasing such a situation. In this example, we have the depLikeFun function which returns number when its input is of type "t" and boolean when its input is of type "f".

interface F {
  "t": number,
  "f": boolean,
}

function depLikeFun<T extends "t" | "f">(str: T): F[T] {
  if (str === "t") {
    return 1;
  } else {
    return true;
  }
}

depLikeFun("t"); // has type number
depLikeFun("f"); // has type boolean

This pattern occurs in various places, such as the TypeScript dom bindings, in issues such as #31672 and #32698, in comments of related issues such as #13995, or on stackoverflow questions. This extension could serve as a workaround for related issues such as #22609 and #23861.

Problem

The problem lies in the implementation of the function. The pre-3.5 behaviour enabled the creation of unsoundness in these type of functions. TypeScript checked the return value using the constraint of key type T, simplifying F[T] to number | boolean. However, this is unsound since the caller can provide a more specific type for T such as "t".

// pre-3.5
function depLikeFun<T extends "t" | "f">(str: T): F[T] {
  if (str === "t") {
    return true; // should be error
  } else {
    return 1; // should be error
  }
}

depLikeFun("t"); // has type number, but is actually a boolean
depLikeFun("f"); // has type boolean, but is actually a number

The post-3.5 behaviour also isn't satisfactory for this use case. It disallows the depLikeFun to be implemented, which means the implementer needs to use unsafe type assertions. By #30769, assigning to type F[T] is interpreted as a write to F at key T. This means that the result type F[T] is checked against the intersection of its possibilities, which is number & boolean and thus never.

// post-3.5
function depLikeFun<T extends "t" | "f">(str: T): F[T] {
  if (str === "t") {
    return 1; // unexpected error: '1' is not assignable to never
  } else {
    return true; // unexpected error: 'true' is not assignable to never
  }
}

Mistakes are more likely to occur in complex situations, and thus aiding the user with these types of functions seems in line with TypeScript's design goals.

Examples

In a dependently typed language depLikeFun would be modeled as function depFun(str: "t" | "f"): F[str]. There are meaningful differences between depending on the actual value of the input versus the type of an input. This distinction makes this issue more tricky to solve than appears on first sight. In this section we showcase the expected behaviour of the addition on certain representative examples.

The main idea behind the addition is as follows: in a dependent-type-like function we cannot narrow the type T of a variable when its value is checked. For example, if str has type T extends "t" | "f" and we check whether str === "t", then it is unsafe to narrow T to "t" in that branch, since T could also be instantiated with the wider type "t" | "f". Instead, we add knowledge about the type T within the branch which is more conservative, but makes it possible to allow the behaviour of dependent-type-like functions. In more traditional programming language theory, the knowledge added is very similar to adding a lower bound "t" <: T into the context.

Basic Use Case

First we look at the depLikeFun example. In the if-branch, returning 1 is allowed since after checking str === "t" the type of T can only be "t" or "t" | "f". Thus, the caller will expect either a number or number | boolean, and thus it is safe to return the value 1.

Note: The claim above that T can only be "t" or "t" | "f" is not quite true due to branded types. For example, T could also be the type Branded, defined as type Branded = "t" & {_branded?: any}. In this case the caller expects a value of type unknown, so returning 1 is also safe.

function depLikeFun<T extends "t" | "f">(str: T): F[T] {
  if (str === "t") {
    return 1; // no error
  } else {
    return true; // no error
  }
}

An example which does not occur for dependent functions, but does occur in dependent-type-like functions, is the following. The type T can be attributed to multiple inputs, this possibility is what makes it unsafe to fully narrow the type parameter based on a check of the input str. However, the reasoning above still holds since the added knowledge is true regardless of how many inputs T is linked to.

function depLikeFun<T extends "t" | "f">(str: T, str2: T): F[T] {
  if (str === "t") {
    return 1; // no error
  } else {
    return true; // no error
  }
}

The extension is conservative, and behaviour of other cases should be the same as in 3.5. However, what might change is the error message users see when implementing dependent-type-like functions. In the situation below, instead of comparing true / 1 to never, they get compared against the simplified indexed access type within each branch. This is number in the then branch and boolean in the else branch.

function depLikeFun<T extends "t" | "f">(str: T): F[T] {
  if (str === "t") {
    return true; // Type 'true' is not assignable to type 'number'
  } else {
    return 1; // Type '1' is not assignable to type 'boolean'
  }
}

Non-Return Indexed Access

The type F[T] can occur elsewhere in the function. This extension retains the normal TypeScript behaviour in those cases, and is only enabled when checking the return type of a function. In the following example we have a value of type F[T] as second input to the function. Within the then branch, this type should not be simplified to number, since it can actually be of type boolean. Checking the first input value does not give us any information regarding the second input value, and thus we cannot do any more simplification.

function depLikeFun<T extends "t" | "f">(str: T, ft: F[T]): F[T] {
  if (str === "t") {
    const n: number = ft; // Type 'F[T]' is not assignable to type 'number'.
    return 1;
  } else {
    return true;
  }
}

let x: boolean = false;
depLikeFun<"t" | "f">("t", x); // ft can be of type 'boolean'

Transitive Type Parameters

TypeScript allows an indexed access with a type parameter which has a direct transitive line to a correct bound. For example, it allows function depLikeFun<T extends "t" | "f", B extends T>(str: B): F[B], but disallows function depLikeFun<T extends "t", F extends "f", B extends T | F>(str: B): F[B].

In these situation it seems safe to let information flow through the transitive chain in both directions. For example, when checking an input of type B, we can add knowledge about T. And vice versa for checking an input of type T and an input of type B.

function depLikeFun<T extends "f" | "t", B extends T>(str: B): F[T] {
  if (str === "t") {
    return true; // no error
  } else {
    return 1; // no error
  }
}

function depLikeFun<T extends "f" | "t", B extends T>(str: T): F[B] {
  if (str === "t") {
    return true; // no error
  } else {
    return 1; // no error
  }
}

Consistency with Conditional Types

TypeScript provides alternative means of creating type-level functions by using conditional types. Instead of creating the record type F, we can create the type constructor F which provides a similar mapping.

type F<A extends "t" | "f"> =
  A extends "t" ? number :
  A extends "f" ? boolean :
  never;

Which can be used as seen below.

function depLikeFun<T extends "t" | "f">(str: T): F<T> {
  if (str === "t") {
    return true;
  } else {
    return 1;
  }
}

This raises the question whether the addition of typechecking for dependent-type-like functions should be added for type level functions created with conditional types too, for consistency purposes. Two points worth noting is that: users were never able to implement this behaviour using conditional types (even pre-3.5), and, type level functions with conditional types are not restricted to a domain of string keys which makes things more complex. Nevertheless, we feel it is a point worth bringing up for discussion.

Behaviour with any

The result of instantiating a dependent-type-like function with the any type gives a result of any. This occurs, for example, when disabling --strictNullChecks and calling the function with null. Any behaviour related to interaction with null/any and dependent-type-like functions is supposed to be unchanged compared to 3.5.

Compiler Changes

In this section we roughly outline the suspected changes to the compiler needed to implement this extension.

• The main change is an addition to the checkReturnStatement (checker.ts) function. When the criteria for enabling dependent-type-like function checking are true, we instantiate the type parameter based on a lookup of checks with literals in the control flow graph. These criteria are currently: the index type is a type parameter, this type parameter is declared in the enclosing function, the index type can be used to index the object type and the object type is concrete.
• To be able to check the control flow graph in return statements, the graph for return statements needs to be bound in the bindWorker function (binder.ts).

Workaround

The current suggested workaround seems to be unsafe type assertions or overloaded signatures, both of which are unsafe features. Neither are satisfactory since the typechecker does not help in preventing programmer mistakes when implementing dependent-type-like functions.

Related Suggestions

The following list gathers related suggestions.

1. extending the TypeScript syntax, such as a oneof generic constraint: #25879, #27808 or #30284
2. dependent types in TypeScript, which would have a huge impact on the compiler and is possibly out of scope for the TypeScript project
3. this extension is a more refined idea based on previous ideas of narrowing types based on term-level checks such as #21879

Complementary to oneof constraints

This proposal has some overlapping use cases with proposals which propose to extend TypeScript with a form of oneof generic constraint, as mentioned in point 1. This proposal is not competing with these, but rather should be seen as complementary. The oneof proposals suggest a new generic constraint which is more restrictive in which instantiations it allows. However, for many of these use cases this is only part of the solution. In addition to adding this syntax, the typechecker must also take this restriction into account to typecheck the original use cases. This proposal kickstarts the implementation of this additional behaviour by focusing on a more constrained use case which does not need this new constraint. If a oneof generic constraint is added to TypeScript, the behaviour defined in this proposal can be extended to take this additional constraint into account.

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. library functionality, non-ECMAScript syntax with JavaScript output, etc.)
• This feature would agree with the rest of TypeScript's Design Goals.

NOTE: (Regarding bullet point 1) The goal of this proposal is to provide more complete typechecking than 3.5, and thus we want to avoid breaking any code compared to 3.5.