Javier Casas

A random walk through computer science

Dependent Types in Typescript

On my previous article, we explored how to make Type Families (also known as Type-level Functions). But this is not the only trick that TypeScript can do. In fact, we can go a step further, and construct some types that depend on values.

What is a Dependent Type?

A plain old type is a label that says something about a value, and either it is standalone, or depends on another type. For example, Int is a "standalone" type, and Maybe is a type that depends on another type, because you have to add it another type for it to be complete, such as Maybe Int. Hence, Maybe is a kind of a function that takes a type, and returns a type. In other programming languages, like Typescript, you have the same stuff: number is a "standalone" type, whereas Array is a type function, that when applied to a type like number, produces another type, like Array<number>.

Type Families, as explained on the previous article, are kind of fancy plain old types. They have parameters (the stuff that goes between the angles), like Array or Maybe, and these parameters are types themselves. At the end of the day, we manufacture new types out of old types, but we never leave the world of "type goes in, type goes out".

Dependent Types are different beast. While a plain old type depends on other types, dependent types depend on stuff different than types. And when we say "stuff different than types", we usually mean values, like the runtime value stored in some variable. What this means is that we can have a variable somewhere, whose type depends on the value of another variable.

To the cynic eye, this is something almost comical: we have invented dynamic types. Congratulations, now our fancy programming languages will start to support what the dynamic languages have been doing for ages. Well, no. This doesn't invent dynamic types. This invents SAFE dynamic types. You know, the type of a variable can change dynamically depending on what's on another variable, but it can't change to any random type. It can only change in a very specific way as defined in the typesystem, and the typesystem will check, guarantee and enforce the usage of the specific type out of the many possible at compile time. Your dynamic languages can't do this. They can only do the types-can-be-dynamic part.

Why would I want Dependent Types?

As usual with typechecking, the objective is getting some kind of type safety, preferably at compile time, with the objective of verifying some level of correctness automatically before running the program. With static types, we can confirm at compile time that we call the integer-accepting function only with integers. But, in some cases, we want somewhat dynamic types, but we also want confirmation that we are calling the integer-accepting function with integers. We want to have the cake and eat it too.

A sample case could be the division function: in order to prevent dividing by zero, we could make the output value a type depending on the divisor. If the divisor is nonzero, we get a double. If the divisor is zero, we get a never, because it will throw an exception and not return. This creates a dependent type: the output type depends on the value of the divisor. This also creates type safety: we can't use the result of the division if it's never, so to prevent it from being never we have to guarantee that the divisor will never be zero. And now the typechecker prevents us from dividing by zero.

A first touch of Dependent Types in Typescript

Believe it or not, you have already seen some cases of Dependent Types in Typescript. They are called Discriminated Unions, or Algebraic Data Types:

type MyADT = {
  type: "case_1",
  field: number
} | {
  type: "case_2",
  field: string
}

In an ADT in Typescript, you have a common field (usually named type) which value can be one of a few strings. In the example above, the two valid strings are "case_1" and "case_2". And Typescript will happily discriminate the rest of the fields based on this string. But nothing prevents us from reusing the other fields' names. Again, in the example above, field is present in both cases, and is present with different types. And this is the trick: in a given MyADT, the type of field depends on the value of type. If type === "case_1", then field is a number. If type === "case_2", then field is a string. Voila, a type depending on a value.

But Dependent Types have to be more than ADTs, right?

If this was all we could do with Dependent Types, it would be great, but not awesome. In fact the Idris and Agda guys would be so annoying if they didn't have a good reason for pushing for better Dependent Types. We have to make it better. In fact, we want to make Dependent Types that go through a function. We want to narrow the type of the output of a function depending on the value of its parameters. We want the divide function that prevents us from dividing by zero.

In order to do this, Typescript provides four features that, when interacting together, can be used to almost reach it.

The Type Quartet

We need four bits to make this incantation work: A way to make a type depend on another, a way to extract a type from a value, ultra-narrowed-down types, and a way to convert explicit values to ultra-narrowed down types.

A type that depends on another: Type Families/Conditional Types

On my last article I explained how can we make a function that receives a type and returns another. This is the trick we are going to use here. By using conditional types, we can make a type that depends on another, like this:

type Foo<A> = A extends number ? string : Array<number>;

const x : Foo<number> = "banana"; // If the type parameter is `number`, the result is a `string`
const y : Foo<string> = [1,2,3]; // If the type parameter is not a `number`, the result is an array of numbers

With this, we can define something that will return a type that depends on something else.

A way to extract a type from a value: typeof

Typescript offers a way to extract the type of a value: the operator typeof:

const x : number = 5;

const y : typeof x = 7;  // typeof x is `number`

// The identity function, returns the same value it was provided
function id(v) : typeof v {
  return v;
}

This operator is very helpful and powerful, as it allows you to copy the type of something. This comes very handy when we have a monster type somewhere and we just don't want to type the whole thing again.

Ultra-narrowed-down types

One of those great features of Typescript is the ability to have ultra-narrowed-down types, types that effectively can hold a single value. For example:

var x : 4 = 4;  // `x` can only be 4, and another 4 is the only thing we can assign to it.
const y : false = false  // `y` can only be `false`

Typescript allows to mix and match these single-value-types to construct something a little bit more useful:

const x : 4 | 5 | 6 = 5;  // `x` can either be 4, 5 or 6
const y : true | false = true;  // `y` can either be `true` or `false`

The last example should make you think: Isn't true | false a longer way to write boolean? Well, yes, but to be able to do it we need to assume another bit: that there will not be a value that is a boolean that is neither true or false. This looks obvious, but it isn't in reality.

The boolean that was neither true nor false

Typescript uses the concept of "type assignability". A type can be assignable to another if it can be used in place of the other. For example, any can be assigned to any other type. And the type 4 | 5 | 6 can be assigned to number. In some sense, a type is assignable to another if it's a subtype of it, or thinking Object Oriented, if it is a subclass.

But what does this have to do with booleans?

Imagine a possible implementation of boolean where we have an abstract class boolean, with two subclasses: class true extends boolean and class false extends boolean. Conceptually, this looks fine. We can create instances of true and false, and every true or false is an instance of boolean.

But we could create another subclass of boolean: class headache extends boolean, and get us a headache.

The problem with this approach is that we can no longer state that boolean = true | false. We have a third value that is neither true nor false, but it is a boolean.

Fortunately, Typescript has some exceptions for these cases, and primitive values are an exhaustive list. Which means, if we enumerate all of them, it is guaranteed that there won't be any other cases created later via subtyping.

By having a closed set of values, we can do things like checking for every value, and be sure that there won't be any other values created later that we are not taking care of. It also means Typescript can do this for us:

const x : boolean = Math.random() > 0.5;
if(x === true) {
  console.log("x is larger than 0.5");
} else if(x === false) {
  console.log("x is smaller or equal to 0.5");
} else {
  console.log("The typechecker guarantees that this is dead code");
  console.log("Furthermore, x is of type `never` at this point");
  const y : never = x;
}

A way to convert explicit values to ultra-narrowed down types

We just saw a case of this, in the code above, but it's not very explicit. Let's make it more explicit:

const x : boolean = Math.random() > 0.5;
if(x === true) {
  const y = x;  // The type of `y` is `boolean & true`, which effectively is just `true`
} else {
  const z = x;  // The type of `z` is a `boolean` where `true` has been excluded.
                // Because `boolean` is either `true` or `false`, Typescript infers that `z` must be `false`.
}

In most cases we can be less explicit (for example by removing the === true. In any case, in the corresponding branch, we have the type narrowed down to a type that represents a single value, and now we can combine everything.

(Almost) A Dependent Type in Typescript

Let's start with a motivating case: an API call. So we have this API, and it has a boolean parameter. If the parameter is false, the API provides basic information, but if it is true it provides extra information. Let's model this:

type BasicInformation = {
  user: string;
  url: string;
}

type ExtraInformation = {
  user: string;
  url: string;
  extra_information: {
    created_at: string;
    total_karma: number;
  };
}

function apiCall(withExtraInformation: boolean): BasicInformation | ExtraInformation {
  ...
}

Well, this kind of says it, but doesn't actually. I mean, apiCall could return a BasicInformation when withExtraInformation is true, and the typechecker would not complain.

function apiCall(withExtraInformation: boolean): BasicInformation | ExtraInformation {
  if(withExtraInformation) {
    const result : BasicInformation = {
      ...  // This is not fine, but the typechecker allows it
    }
    return result;
  } else {
    const result : ExtraInformation = {
      ...  // This is also not fine, and again the typechecker allows it
    }
    return result;
  }
}

But we have a few tricks we can apply. First trick: conditional types:

type APIResult<T extends boolean> = T extends true ? ExtraInformation : BasicInformation

Now we have a type that can mutate into a single possibility with the right parameter. Second trick: narrowed down type:

function apiCall(withExtraInformation: boolean): BasicInformation | ExtraInformation {
  if(withExtraInformation) {
    // The type of `withExtraInformation` is `true` 
    const result : APIResult<typeof withExtraInformation> = {
      ...  // This object must be an ExtraInformation
    }
    return result;
  } else {
    // The type of `withExtraInformation` is `false` 
    const result : APIResult<typeof withExtraInformation> = {
      ...  // This object must be a BasicInformation
    }
    return result;
  }
}

Now tying down the function parameter:

function apiCall(withExtraInformation: boolean): APIResult<typeof withExtraInformation> {
  ...
}

At this point everything kinda aligns properly:

  • The types of the values to be returned is the type of the return of the function.
  • These types are narrowed down to specific types in each branch of the conditional.
  • Typescript actually checks them instead of allowing anything.

Unfortunately, we can't get that far when using it. When faced with a conditional type, Typescript tends to narrow it to the two possibilities, ignoring the parameters we pass.

const x = apiCall(true); // x is of type BasicInformation | ExtraInformation
                         // Typescript is unable to narrow it down to ExtraInformation

So, we can have some Dependent Types inside a function, but not outside of it.

Update: a variant that almost works

As Jeralm notes, we can add a type parameter to improve the typing outside the function, as:

function apiCall<E extends boolean>(withExtraInformation: E): APIResult<E> {
  ...
}

const result = apiCall(true);  // Now typed as ExtraInformation

Unfortunately, this causes Typescript to no longer type the function inside it properly:

function apiCall<E extends boolean>(withExtraInformation: E): APIResult<E> {
  if(withExtraInformation) {
    // The type of `withExtraInformation` is `E` 
    // Typescript no longer narrows it down to `true`
    const result : APIResult<E> = {
      ...  // Typescript can't narrow down the APIResult<E> type anymore. This never typechecks.
    }
    return result;
  } else {
    // The type of `withExtraInformation` is `E` 
    // Typescript no longer narrows it down to `false`
    const result : APIResult<typeof withExtraInformation> = {
      ...  // This also never typechecks
    }
    return result;
  }
}

So we have to choose if we want it to be properly typed inside or outside.

Update 2: A variant that finally works

As Arielh notes, there is a further change that we can do to get it to work:

function apiCall<E extends boolean>(withExtraInformation: E): APIResult<E>;
function apiCall(withExtraInformation: boolean): ApiResult<typeof withExtraInformation> {
    if (withExtraInformation) {
        // The type of `withExtraInformation` is `true` 
        const result: APIResult<typeof withExtraInformation> = {
            ...  // This object must be an ExtraInformation
        }
        return result;
    } else {
        // The type of `withExtraInformation` is `false` 
        const result: APIResult<typeof withExtraInformation> = {
            ...  // This object must be a BasicInformation
        }
        return result;
    }
}

const extraInformation = apiCall(true);  // Typed as ExtraInformation
const basicInformation = apiCall(false);  // Typed as BasicInformation

This uses function overloads to basically note that this function has two different call signatures, and makes the type system try to use the call signature that works on each usage site.

Takeaway

Turns out Typescript has several features that are very interesting. Furthermore, we can mix them and get surprising results, results that may go way further that what Typescript was designed to do. Which means there is a lot more to explore than what you can see in the documentation, and there is a lot of margin for improvement beyond putting basic types.

Back to index
Copyright © 2018-2023 Javier Casas - All rights reserved.