Dependently-Typed TypeScript

Dr. Lars Hupel

Dieser Artikel ist auch auf Deutsch verfügbar

The JavaScript Challenge

JavaScript is a language whose early versions were undeniably haphazardly slapped together. The legendary Lightning talk “Wat” by Gary Bernhardt sums this up. Hence, in JS, you can basically add or multiply everything by anything:

> [] + []
''
> [] + {}
'[object Object]'
> {} * 0
NaN

Such behavior is rarely desirable.

Meanwhile, common features, such as class-based inheritance, have been introduced into JavaScript. These developments are largely driven by TC39, the standards committee behind JS. More practical tools are available in each new standard to write better software. For example, “optional chaining”, known as the “Elvis operator” in other languages (e.g., Kotlin).

However, the fundamental problem still exists: A vast amount of JavaScript code runs in browsers. There, it is difficult, if not impossible, to detect or even debug errors with common observability practices because there is an unlimited number of computers running the code in the browser.

Types, but How?

The idea of TypeScript, then, is to bring the benefits of type systems – namely, detecting errors before an application is deployed – to the JavaScript ecosystem.

Unfortunately, this ecosystem is unruly because browser APIs, Node.js, and numerous libraries were designed to be completely type-free. As an example, consider event listeners in Node.js:

server.on("close", f);
server.on("request", g);

In both cases, we register a callback on the server object using its on method; on the one hand for shutting down the server, on the other hand for incoming requests. However, the callbacks have different types. f receives an optional error. g receives a request and a response object, which can be processed by the request handler.

Classical object-oriented languages such as Java cannot represent this. Instead, the methods must be disambiguated by name:

server.onClose(f);
server.onRequest(g);

However, in our case, JavaScript came first. The TypeScript developers had to represent these (and many other cases) in their type system.

Literals and Overloading

The server object’s type signature looks like this in TypeScript:

interface Server {
    on(event: "close", handler: (err?: any) => void): void;
    on(event: "request", handler: (request: Request, response: Response) => void): void;
}

In this superficially very simple use case, you can already see several interesting features. For one, TypeScript allows practically any overloading of methods. However, this overloading is only allowed in declarations. For each method, there may only be a maximum of one implementation, which must then check at runtime which concrete signature has been called. Thus, for a given invocation of server.on, the type checker only checks whether at least one overloaded declaration matches, leaving the rest to the invoked function.

Furthermore, you can see that the first parameter event must be either "close" or "request" as type: so-called literal types. Literal types are allowed for all primitive values in TypeScript:

const a: 3 = 3;
const b: "foo" = "foo";
const c: 4 = 3; 
// Type '3' is not assignable to type '4'.

const d: undefined = undefined;

Even array literals are allowed:

const e: [1, "foo"] = [1, "foo"];

These serve as a replacement for tuples in JavaScript.

Objects and Properties

While the above is also possible in Scala, for example, TypeScript’s type system also has some unique features. A common programming pattern in JavaScript is to pass an arbitrary object to a function, as well as a list of strings which are names of fields in that object:

const obj = { x: 3, y: 4, z: 5 };

validateObject(obj, ["x", "y"]);

Our expectation here is that an invocation with the string "a" should produce a type error.

Before we can take a closer look, we need to briefly get an overview of property access in JavaScript. The following two lines are equivalent to each other:

const x = obj.x;
const x = obj["x"];

Object accesses can be made similar to arrays with square brackets. In most object-oriented programming languages, the statement "x" is a field in obj is not a proper type; in other words, we cannot write this statement down as an annotation. In TypeScript, this is very much possible. The space of all valid keys of an object type T is annotated in TypeScript as keyof T.

We can thus add a signature to the above validation function as follows:

function validateObject<T>(t: T, props: Array<keyof T>): void;

In case of a wrong invocation the compiler complains:

validateObject(obj, ["a"]);
// Type '"a"' is not assignable to type '"x" | "y" | "z"'

Here it was inferred that the key space of obj corresponds exactly to the sum type "x" | "y" | "z".

However, the power of the type system ends where one wants to check the uniqueness of array elements, for example. The following, possibly unintentional invocation, is accepted:

validateObject(obj, ["x", "x"]);

Ducks and Types

The object validation example also took advantage of another TypeScript feature in passing. We defined obj as an object literal without specifying a class or interface. Accordingly, TypeScript infers this type:

obj: { x: number; y: number; z: number; }

But even if we had defined an interface for this object: Interfaces and even classes are nothing more than type aliases for TypeScript, because Duck Typing rules in the JavaScript universe. Consequently, all type checks on object types are structural. This in itself is nothing new (some ML-like languages use this for records). However, TypeScript has implemented it on a much broader scale, as classical OOP languages use only nominal subtyping.

There are few exceptions to these structural types in TypeScript; for example, identically named private fields in classes are considered different if they are defined in separate files. This was a deliberate design decision to avoid mixing implementation details from different libraries.

Narrowing

Before we can look at actual calculations with types, I would like to briefly show another compiler feature that is otherwise only known from languages like Agda and Coq: Dependent Pattern Matching. Let’s imagine the following type definitions:

interface Rectangle {
    type: "rect";
    height: number;
    width: number;
}

interface Circle {
    type: "circle";
    radius: number;
}

type Shape = Circle | Rectangle

If we now want to write a function that works for arbitrary forms, we can make a (runtime) case distinction where the compiler restricts the type based on the condition:

function draw(shape: Shape) {
    switch (shape.type) {
        case "rect":
            const { height, width } = shape;
            break;
        case "circle":
            const { radius } = shape;
    }
}

In the case "rect" it must be a rectangle, so the compiler grants access to height and width. The use of switch is unnecessary; other control flow (e.g. if) is also analyzed.

Although the mechanism of extracting static information from dynamic information is part of the standard repertoire of dependency-typed programming languages, it is rather a “happy accident” in TypeScript. In fact, the following code does not work:

function scale<T extends Shape>(shape: T): T {
    switch (shape.type) {
        case "rect":
            const { height, width } = shape;
            return {
                type: "rect",
                height: height * 2,
                width: width * 2
            };
        // ...

    }
}

Not only can shape not be narrowed down to rectangle here but also the return statement cannot work like this.[1] In certain cases, however, it can also happen the other way around that the compiler accepts obviously incorrect expressions, which can have two common causes:

1. the type any is inferred in an unexpected position (which can be prevented by a compiler flag); a type that is compatible with all arbitrary expressions
2. one runs into an unsoundness of the compiler

Apart from these limitations, narrowing in TypeScript is so powerful that it is very often used in practice.

For the sake of completeness, it should be mentioned that in the classic school of type systems, it is not allowed that the type of one and the same symbol (here shape) changes based on its lexical usage. But since, e.g. Kotlin has also abandoned this tradition, this fight – just like the fight against the terms “transpilation” and “isomorphic JavaScript” – has been lost long ago.

Values in Types

So far, we have seen some constructs that soften the barrier between types and values given in classic ML-style type systems. As an intermediate state, we can note that TypeScript allows (value) literals in type expressions in some places. These literals can be used, for example, to calculate element types or to select variants of an overloaded method.

But it doesn’t stop here by a long shot. We can also do primitive calculations with types.

To get started, we can rewrite the server definition as an example in such a way that no method overloading is necessary:

// with overloading

interface Server {
    on(event: "close", handler: (err?: any) => void): void;
    on(event: "request", handler: (request: Request, response: Response) => void): void;
}

// without overloading

type ServerHandler<T extends "close" | "request"> =
    T extends "close" ?
        (err?: any) => void :
        (request: Request, response: Response) => void
         

interface Server {
    on(event: "close" | "request", handler: ServerHandler<typeof event>): void;
}

In this snippet, the infamous ternary operator cond ? yes : no appears, but at the type level. This allows distinctions to be made between cases depending on subtype; valid conditions are checks of the form X extends Y. Furthermore, with ServerHandler<typeof event>, a genuinely dependent type is included in the signature. It is not just a literal, which appears in a type, but a variable.

As expected, when on is invoked, the type of the callback is inferred correctly:

server.on("close", (err? /* any */) => {});
server.on("request", (req /* Request */, res /* Response */) => {})

However, this notation has a catch to it. If you want to implement this interface, you might be inclined to write the following in the on method:

if (event === "close") {
  handler();
} else {
  // ...
}

Narrowing TypeScript fails here as well: the restriction of event to the literal "close" is not propagated to handler.

You can again make do with casts here; otherwise, the only thing left to do is try further indirections. However, this article is more about the type system, which is why I will not go into the implementation any further.[2]

Last but not least, I would like to simplify the types a bit more. The ServerHandler type shown above does what it is supposed to but scales very poorly to additional variants. A common pattern in TypeScript is therefore to define a phantom type:

interface ServerHandler {
    close: (err?: any) => void;
    request: (request: Request, response: Response) => void
}
    
interface Server {
    on(event: keyof ServerHandler, handler: ServerHandler[typeof event]): void
}

Instances of ServerHandler are not used here; instead, the interface is only used to attach a set of types to names. To do this, the keyof construct can be used to restrict the name of the event to the known events. Instead of pointed parentheses, square brackets are used to select the correct handler type.