Free-types: Higher kinded types in TypeScript (opens in new tab)

A situation where I needed this were typings for Cycle.js a couple years ago. At this time, you could configure it to use the observable library of your choice but it was hard to type. In particular the observable could be a `Stream from "xstream"` or `Observable from "rxjs"`

This lib has a method `select` to return an observable list of DOM elements for a given CSS selector. What should be its signature? If using `xstream`, it should be `select(selector: string): Stream<HTMLElement[]>`, and if using `rxjs` it should be `select(selector: string): Observable<HTMLElement[]>`. Let's also assume that it has a second method `windowHeight` returning an observable for the window height (`Stream<number>` or `Observable<number>`).

We can make the lib object generic over the observable implementation, but you need HKTs to type it properly. The reason is that the lib is generic over an already generic type.

Here is an example:

    // Without HKT (regular generic)
    // Problem: both `select` and `windowHeight` return the same type (we lose the HTMLElement[]/number information)
    interface Cycle<Obs> {
      select(selector: string): Obs;
      windowHeight(): Obs;
    }
    // The best we can do is type it as `Cycle<Stream<unknown>>` or `Cycle<rxjs.Observable<unknown>>`.
    
    // With HKTs, using syntax from this lib, you could do:
    interface Cycle<$HktObs> {
      select(selector: string): apply<$HktObs, HTMLElement[]>;
      windowHeight(): apply<$HktObs, number>;
    }
    // This allows to get the precise signatures we wanted (with the right observable impl, without `unknown`)

Higher (-order) kinded types describe functions on type constructors. Type constructors are "generic types", like `T[]` that generate a list from a single type `T` or like `Map<S, T>` that generates a new type from two types `S` and `T`. A higher kinded type constructor is one, where you could use any (well, with certain prerequisites) of these type constructors to generate a new type. Let's say you want to have a function `map` (like `Array.map`) that works not only with `T[]` but also with `Tree<T>`, `Maybe<T>` (`= T | undefined`), ... HKT give you the possibility to write the type of such type functions.

The thing is, it takes a bit of experience to appreciate why HKT are important, and typically you can only get this experience using Haskell.

There’s a couple of ways to think about it: it gives you a way to talk about List rather than List of T, it enables you to write partial types like partially-applied functions, or it makes it possible to define Monads.

But as I say, none of these things will sound immediately useful unless you have experience of using those concepts already.

It's easier to make the parallel between type-level and value-level reasoning.

1 is a value, and int is a concrete type.

function increment(x) { return x + 1 } is a value-level function. You feed it a value x and you get a value back. List<T> is a type-level function: you give it a concrete type T, you get another type back.

function applyTwice(f, x) { return f(f(x)) } is a higher-order function that takes a functions as an input. A higher-kinded type is a higher-order type function.

As a concrete example, consider this pseudo-Java method:

    List<B> map<A,B>(Function<A,B> fn, List<A> as) { ... }

You take a list, and you return a list. Thing is, Java has several list implementations: LinkedList, ArrayList, CopyOnWriteArrayList, and a few others. What I'd like to express is that whatever concrete list type goes in is also the concrete type that comes out. If java allowed it, you could express it like this:

    L<B> map<L<T> extends List<T>,A,B>(Function<A,B> fn, L<A> as) { ... }

This map is generic on L, A, and B, but also L is itself generic, so map is "twice-generic", if you will.

"A type that accepts types that generates another type" is called a type constructor. And a "kind" is the type of a type constructor, just to have a new name and not needing to call that "type" too. "Generic types" like `Vec<T>` (in Rust) are type constructors, they "generate" a type `Vec<T>` from the type `T`. Type constructors that take one type as argument have the kind `* -> *` (or as Rust-y notation `fn(*) -> *` - read each asterisk as "type". Type constructor that take two types arguments have the kind `* -> * -> *` (Rust-y: `fn(*, *) -> *`). A higher (-order) kinded type takes (for example) a type constructor (here a type constructor which takes just one argument) and generates a type from it: `(* -> *) -> *` (Rust-y: `fn(fn(*) -> *) -> *`.

Edit: I hope now all asterisks are properly escaped ...

For Rust, pre-GAT, there was no way to “output” a type which could be “called” with further arguments (very fuzzy terminology, sorry, best I can do!) or maybe in other words, you could write functions which retuned values, but not new functions.

Nowadays, GATs support a bigger subset of HKTs, but still not everything as I understand it.

https://blog.rust-lang.org/2022/10/28/gats-stabilization.htm...

A simple example I could recall from the other day is something like this:

  export type LinkedWorksheetsRecord = Record<WorksheetId, Record<WorksheetId, ReferenceTypeId[]>>;
  export type LinkedWorksheetsMap = Map<WorksheetId, Map<WorksheetId, ReferenceTypeId[]>>;

What I would rather have written instead is however something like this:

  export type LinkedWorksheets<T> = T<WorksheetId, T<WorksheetId, ReferenceTypeId[]>>;
  ...
  const myMap: LinkedWorksheets<Map> = ...;

This is however not possible, because `Map` is a type constructor which expects two more type arguments `K, V` until it is a fully applied, concrete type `Map<K, V>`.

With a library like this, this is probably possible (unless I've missed something which wouldn't surprise me). It would unfortunately surely be more verbose.

Still, I would be against pulling in a dependency only for something like this. The above example is simple I believe, but not exactly a "killer-app". And no, Monads aren't either (if you don't limit effects and don't have do-notation) :P

I'm using fp-ts https://gcanti.github.io/fp-ts/

Might be wrong here, but I'm of the understanding that a dependent type system is undecidable, and so to have static dependent types you need to have a more restricted language, like the inability to write arbitrarily recursive functions.

In short I don't think so but I'd also love a good explanation as to why I'm wrong.

I guess you could use it to implement an algebra that allows you to build dependent types, but that would be unfit for practical uses.

As a case in point, Haskell has first-class experience for HKTs, and dependent types implementation in haskell is getting hindered by the limits of the language.

No. Typescript cannot access runtime values (I assume you mean types that depend on runtime values). In TypeScript types can depend on other types and it does support literal types which covers a lot of use cases. What do you need dependent types for?

[Edit: why the down vote?]

They are related, but different concepts. An HKT is the type of a type constructor. An example described in another comment in this thread is if you want to define the map function on any collection C (in pseudo-Java),

    C<B> map(C<A> coll, Function<A, B> fun)

Mapping over an Array would return an Array while mapping over a List would return a List. C<_> here is an HKT, the type of a type constructor with one argument.

In OOP a class is a description of what an object can do, often with a constructor that produces instances of the class with values as arguments. A type class is the same thing, but the constructor of a type class takes types as arguments. Type classes are useful because they allow defining functions for many types that share something without having to make the types inheritors of a common class (composition over inheritance basically).

For the example above I could define (pseudo Java) a type class like this,

    interface Mappable<C> {
      C<B> map(C<A> coll, Function<A,B> fun);
    }

and then if I want to define a function generic over anything that has a map I can do so by requesting both the thing and a Mappable of the thing,

     C<B> foo(Mappable<C> inst, C<A> coll)

Then I can use the Mappable instance to call map over any coll instances. For example a generic "size" function could be defined like this [1],

    C<B> foo(Mappable<C> inst, C<A> coll) {
      var out = 0;
      inst.map(coll, k -> {out++; return k});
      return out;
    }

So that function would be enough to prove that Mappable<C> implies that C has a size and you can then define a function that gives you Sizeable from Mappable, which is useful composition.

The example above is very boilerplate heavy because Java doesn't really support type classes but in Scala and especially Haskell the syntax is a lot cleaner.

[1] Usually you would use a fold here instead of a side effecting map.