Repository: TypeScript
Issue: Higher-kinded Types... And other stuff
Labels: Suggestion,Awaiting More Feedback

# Higher-kinded Types – Not quite a proposal

HKTs have been a much-discussed and desired feature for most of the language’s existence, with many usecases proposed over the years, but so far there have been no concrete proposals I'm aware of.

One of the difficulties is that HKTs are usually defined in languages with radically different (i.e. nominal) type systems. As such simply porting them into the language doesn’t really make sense – instead, they need to be reimagined and rephrased to fit with the rest of the language.

What follows is one such reimagining.

---

This proposal introduces two new type system constructs.

* **Container types**: These are higher-kinded types. They are not assignable (have no instances). They turn type declarations into structure that TypeScript can reason about.
* **Kinds:** The K in HKT. Kinds are higher-order types, the instances of which are all other types. They are used to quantify over families of container types. A kind alias is declared using `type type`.

# Part 1: Container types

An container type is a type that contains type members and no value members. Here is an example of an container type:

```typescript
// A container type that has two type members.
type Container = {
    type A = number
    type B = string
}
```

Container types are not inhabited – they have no instances, and a type annotation such as `let a: Container` is equivalent to `let a: never`, though in practice it would just be illegal. We can also say that an container type is *non-assignable*.

What container types *do* have is a type-level structure. This structure can produce assignable types.

Here is an example of such an alias producing the assignable type `number` from an container type:

```typescript
// You've seen this before, haven't you?
type Example = Container.A
```

Having defined them, we can actually find container types in the language already. Let’s take a look at the common namespace.

```typescript
// Plot twist! 
// Namespaces have been the key to HKTs all along.
namespace Container {
    type Example1 = number
    type Example2 = string
    export const value = 5 as const;
}
```

The declaration above creates several different entities:

1. The value binding `Container`, which has value members such as `Container.value`.
2. The type `typeof Container` which is equivalent to `{value: 5}`. 

But the type definitions `Example1` and `Example2` are actually in a third entity, a hidden container type also called `Container`. 

## Members of container types

Container types can have generic members as well as regular members. This is analogous to how object types can have value members and function members. Also, we know this because namespaces can have those things too.

## Generic types as container types with generic call signatures

Normal types can define a call signature. Analogously, container types can define a generic call signature:

```typescript
type Example = {
    type <T> = number
}
```

**In fact, every generic type is actually an container type with such a signature.**

Container types can also embed other container types, creating nested structures of types.

```typescript
type Nest = {
    type Parent = {
        type Leaf = string
    }
}
```

## Subtype relation for container types

TypeScript determines subtype relations structurally, and the same is true for container types. However, the structure of an container type is the way in which other types are embedded inside it, and it affects the rest of the program based on the assignable types it can produce.

Before we can abstract over container types, we need to define a subtype relation `⊆` for them. The subtype relation determines what it means for two container types `A`, `B` to be structurally equivalent – `A ≡ B`. The way this relation is defined will change what *structure* means in the context of these types.

We’re going to define a very strict subtype relation, much stricter than the assignability relation used by normal types. Namely:

> For a container type `Sub` to be a subtype of `Super` – `Sub ⊆ Super`, `Sub` must produce the same types as `Super` when subjected to various operations.

Let’s formalize it. To do that we need to define something called a *type formula*.

> **Type formula:** A meta-language construct. A type formula is an expression involving a replacement token φ. A type formula consists of:
>
> 1. φ
> 2. Accessing a member type, `φ.Member`
> 3. Instantiating a type constructor `φ` with  `φ<T₁, …, Tₙ>` 
>
> We’ll write a type formula like this:
>
> ```
> F{φ} ⇒ φ.Something<number>.A
> ```
>
> Here are some more examples.
>
> ```
> F{φ} ⇒ φ.One.Two.Three<number>
> F{φ} ⇒ φ<string>
> ```

Now to define our subtype relation:

> For two container types `Sub`, `Super`, `Sub ⊆ Super` iff for all type formulas `F{φ}` where `F{Super}` is assignable, `F{Sub} ≡ F{Super}`.

Notice that we delegate the final test to the existing assignability relation, which makes sure there is no infinite recursion.

The way we defined the *type formula* tells us that the structure of a container type involves:

1. The names of contained types.
2. For generic types:
   1. The number of type parameters.
   2. Constraints placed on type parameters must be compatible, i.e. if `Super<X₁, …, Xₙ>` is valid, then so must `Sub<X₁, …, Xₙ>` be.
   3. Default parameter values must be the same, if any. This part is actually a bit weird.
3. **Recursion** for container types – If `Super.A` is an container type then `Sub.A` must also be container and `Sub.A ⊆ Super.A`.
4. **Invariance** for assignable types – The leaf assignable types in the resulting tree structure must be equivalent, not just subtypes. If `Super.B` is assignable, then `Super.B ≡ Sub.B`. 

Let’s take a look at some specific examples.

### Assignable types are invariant

```
{ type A = "a" } ⊈ { type A = string }
```

Assignable types must be invariant.

### Partial structure means supertype

```
{ type A = "a", type B = "b" } ⊆ { type A = "a" }
```

### The generic signature is important

```
{ type F<T> = number } ⊈ { type F = number }
{ type F<S> = number } ⊆ { type F<T> = number }
```

### Type parameter constraints must be compatible

```
{ type F<T> = T } ⊆ { type F<T extends number> = T }
```

# Part 2: Kinds

Kinds are the types of types, of which all normal types are instances.

All non-container types have the kind `*`, while container types have kinds that describe their complex type structures.

Aliases for kinds are defined using `type type` and their definitions use double braces `{{}}`.  Here is an example:

```typescript
// These things are complicated. Take it from me
type type SomeKind = {{
    type Scalar:*
    type KindBased:OtherKind
    type Constrained extends string
    type Fixed = number
}}
```

Kinds define type variables as members. Every type variable is defined together with a constraint, which may reference any of the other variables. 

Several constraints are possible:

1. A kind annotation, such as in `type KindBased: OtherKind`, which resembles a type annotation. This restricts that type variable to be an instance of the given kind.
2. A kind annotation with the kind `*`, such as in `type Scalar:*`, which restricts it to a non-container (regular) type.
3. A subtype constraint, such as `type Constrained extends string`.
4. An equality constraint. This makes that type variable fixed.

An instance of a kind is a container type that fulfills all constraints on its members. 

No special type information is conveyed in the alias itself – that part simply binds a *kind expression* of the form `{{ … }}` to a name. Whether you use a reference to an alias or the expression doesn't matter for type checking purposes. It may affect inference but that's a different story.

As with other language constructs, you can nest kind expressions.

Kinds can also define generic type members. These are translated to non-generic container types using a kind annotation. For example, the following are equivalent:

```typescript
type type A = {{
    type F<T> extends number
}}

type type B = {{
    type F: {{
        type <T> extends number
    }}
}}
```

Kinds are basically superpowered object types, with individual instances that are container types. A kind can have many possible instances, which can be easily constructed when needed. Just imagine an object full of types.

In object types every key is constrained with a type annotation. In kinds, every key can be a higher-kinded type (i.e. a container type) or a regular type (like `string`). We just need to constrain every member accordingly. 

Subtype constraints allow constraining with regular types like `string`, while kind constraints are used for container type members, which includes generic types. The `=` constraint is mainly useful for types with the kind `*`. One use case of that constraint is creating helper type variables. You can even prefix one with `_` and pretend it's private.

```typescript
type type WeirdStuff = {{
	type _Something = Blah | string
	type Blah = number
}}
```

Kinds can’t have type parameters themselves. Things are already bad enough without having to deal with that.

## Instance-of vs subtype-of

It’s important not to confuse two relations defined on container types – the subtype relation container types `A extends B` and the kind annotation `A: K`. 

This comes up because container types are both types themselves but also the instances of other types (that is, kinds). There is a relationship between the two however – specifically, if `B: K` and `A ⊆ B` then `A: K`.

## Trivial kinds

There are a few kinds we know about in advance and so call them trivial.

1. `*` which we’ve mentioned
2. `never` makes a reappearance. As a type with no instances, it’s just at home as a kind. There is only one empty set after all.
3. The kind `{{}}` describes an empty container type. It has no purpose. 

## Uninhabited kinds

You can easily define paradoxical kinds.

```typescript
type type Paradox = {{
    type Liar extends (Liar extends true ? false : true)
}}
```

This kind is **uninhabited** – it has no instances. Kinds like `Paradox` are equivalent to `never`. However, the general problem of [whether a type is equivalent to `never`](https://en.wikipedia.org/wiki/Type_inhabitation) is unfeasible, so the language can’t detect things like this.

You can also create kinds that describe types that contain themselves.

```typescript
type type Classic = {{
	type Self: {{
		type Me = Self
	}}
}}
```

## Syntax positions

A kind annotation looks just like a type annotation, except for its operands. These are always a **type** and a **kind**. Kind annotations apply to the following:

1. Type parameter declarations.
2. Type members of other kinds.
3. Type alias declarations for non-generic container types. In this case, the annotation makes sure the type being defined conforms to the given kind.

```typescript
// The type parameter T is restricted to types that are instances of SomeKind
declare function generic<T:SomeKind>();

type type OtherKind = {{
    // This type must conform to SomeKind for the container
    // to be an instance of OtherKind
    type Contained: SomeKind
}}

// The definition of Container is checked against SomeKind,
// similarly to an `implements` clause.
type Container:SomeKind = {
    type A = number
}
```

## Mutually recursive references

The type members of kinds can reference each other in their constraints.

```typescript
type type NumberExample = {{
    type A extends number
    type B extends A
}}
```

Here is an instance of `NumberExample`:

```typescript
type NumberExampleInstance: NumberExample = {
    type A = 5 | 4
    type B = 5
}
```

One can define constraints like the folowing.

```typescript
type type Crazy = {{
    type A extends B
    type B extends A
}}
```

While this may seem like infinite recursion, it’s really not. It doesn't construct a infinitely large type, just place an odd constraint. 

It is true, however, that the only instances of this kind are types of the form:

```typescript
type InstanceOfCrazy = {
    type A = φ
    type B = A
}
```

The compiler will be able to recognize the fact that this is an instance of `Crazy`, but I'm not sure it will be capable of constructing an instance on its own (that is, for inference purposes).

## Regular recursive reference

Type variables can also reference themselves in their constraints. Here it's used to implement a common pattern seen in immutable collections:

```typescript
type type Imm = {{
	type Seq<T> extends {
		push(x: T): Seq<T>
		pop(): Seq<T>
		readonly length: number
	}
}}
```

As a sidenote, this kind of reference might not be possible when defining a generic call signature:

```typescript
type type Seq = {{
	type <T> extends {
		push(x: T): ?
	}
}}
```

There are several ways out of this situation. The first is to just disallow it. If you want to write a type like that, you'd have to do:

```typescript
type type Seq = {{
	type Instance<T> extends {
		push(x: T): Instance<T>
	}
	type <T> = Instance<T>
}}
```

That's pretty awkward though. Another option is to use something like `<T>` or `This<T>`:

```typescript
type type Seq = {{
	type <T> extends {
		push(x: T): <T>
	}
}}
```

My favorite approach is allowing the use of the name `Seq`. When it appears in the position of a type rather than a kind, it will be treated as a self-reference that's similar to `this`.

```typescript
type type Seq = {
	type <T> extends {
		push(x: T): Seq<T>
	}
}
```

I think this would seal the deal on having generic kinds - they would just be too confusing if this syntax was allowed.

In other situations we have an unambiguous symbol being annotated that can be used as a self reference, such as in this function:

```typescript
declare function example<Seq: {{ type <T> extends { push(x: T): Seq<T> }}}>()
```

## Type checking

Let’s say we have a function with kind-constrained type parameters:

```typescript
function test<T: K>(x: T.SomeType<string>): true
```

And we have an invocation such as:

```typescript
test<{
    type SomeType<T> = boolean
}>(thing)
```

Determining if this invocation is legal boils down to the following stages:

1. First, determine if the specified container type is an instance of the kind `K`.
2. Compute all type expressions, substituting the container type for `T`.
3. Standard assignability check involving the type of `thing` versus the type of `x` computed at (2).

All of these are feasible, even if 1 will probably get computationally expensive for complicated kinds.

## Type inference

Let’s say we invoke the `test` function above without specifying type parameters explicitly:

```typescript
test(thing)
```

The compiler must try to **construct** a container type that satisfies `K` and allows the function to be called. This essentially amounts to solving two hard problems:

1. Finding the instances of kind `K`
2. Among those instances, find an instance that results in `thing` being assignable to `x`. 

Both of these problems are untractable for non-trivial kinds, especially since assignability in TypeScript is already a difficult problem. However, there are still strategies for tackling it.

1. Collect existing type information in the call itself or in its context.
2. In the simplest case, the known type of `thing` might already be expressed with a container type that the compiler can just use. Users could use this fact by making sure arguments are asserted to have carefully chosen types. 
3. Another solution involves trying to find an instance of `K` in the context of the call itself, using various systems of implicits.
4. If there are any value inputs annotated with types that are fixed in `K` (i.e. `type Something = Sibling<number>`), we can use them to resolve the other types.

Another way is: Direct type hints in the form of partial container types. 

Let’s say that we have the following:

```typescript
type type Example = {{
    type Num extends number
    type Array = Num[]   
}}

function test<T: Example>(arr: T.Array): T.Num
```

While we could stick the complete container type when calling the function, in fact simply providing the type value of `Example.Num` might be enough, as the compiler could be able to figure it out the rest.

```typescript
test<{type Num = 5}>(...)
```

Let’s phrase this in the language of the type system. 

When calling a generic function that expects a kind-annotated type parameter, you can supply a supertype instead. If the supertype isn’t an instance of the kind, the compiler will try to generate a subtype of the supplied type that *is* an instance of the kind.

## Large container types

Let’s say we define a kind for an immutable sequential collection:

```typescript
type type Imm = {{
    type Seq<T> extends {
        constructor: {
            new<S>(...xs: S[]): Seq<T>
        }
        push(x: T): Seq<T>
        pop(): Seq<T>
        readonly head: T
    }
}}
```

And let’s say we want to write a `map` function that will conserve the collection type. Well, one way to do it is as follows.

```typescript
function map<I: Imm, A, B>(input: I.Seq<A>, f: (x: A) => B): I.Seq<B>
```

However, there is another way to do it – we can put all the type parameters inside the container type.

```typescript
type type Mapping = {{
    type Collection: Imm    
    type InElement:*
    type OutElement:*
    type InCollection = Collection.Seq<InElement>
    type OutCollection = Collection.Seq<OutElement>
    type Mapping = (x: InElement) => OutElement
}}

function map<M: Mapping>(input: M.InCollection, f: M.Mapping): M.OutCollection
```

Is this better? It has advantages. Is it worse? It has drawbacks. You decide!

# Fin

This is not quite a proposal and it doesn’t really cover everything. Here is a partial list of things I haven’t addressed:

* Operators `&` and `|`
* Conditionals on kinds/containers?
* Can these types be `infer`ed?
* What about interfaces and classes?

Have I missed something ? Is there something wrong with the syntax? Is there a better way to explain or represent something? I'd love to hear your feedback!