Higher-kinded Types... And other stuff

[GregRos]

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:

// 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:

// 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.

// 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:

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.

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:

// 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:

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.

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.

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 is unfeasible, so the language can’t detect things like this.

You can also create kinds that describe types that contain themselves.

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.

// 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.

type type NumberExample = {{
    type A extends number
    type B extends A
}}

Here is an instance of NumberExample:

type NumberExampleInstance: NumberExample = {
    type A = 5 | 4
    type B = 5
}

One can define constraints like the folowing.

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:

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:

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:

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:

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>:

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.

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:

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:

function test<T: K>(x: T.SomeType<string>): true

And we have an invocation such as:

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:

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:

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.

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:

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.

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.

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 infered?
• 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!

[fatcerberus]

FWIW it’s been my observation over the years that, when people ask for higher-kinded type support in TypeScript, for the most part they ultimately just want to be able to do this:

type Instantiate<F^, T> = F<T>;

i.e. to be able to pass generic type aliases as type arguments and instantiate them generically. Introducing what basically amounts to full-on type classes, as in e.g. Haskell, feels like overengineering and actually counter to the goal, which is to have effortless first-class generics, just like JS has first-class functions.

[GregRos]

@fatcerberus
I think you might be underestimating how many people want actual type classes. There are multiple working encodings of HKTs that revolve around type classes and type classes have often been at the center of discussions about HKTs.

A core problem of implementing HKTs in TypeScript is that as far as the subtype relation is concerned, type declarations don't exist, and neither do generic types. This is unlike in other languages, where types are nominal and revolve around declarations. Types can just be declared generic, and when a generic type is instantiated you can recover the arguments because they're an inherent part of the type.

TypeScript is very different. Because everything is purely structural, any HKT proposal will need to invent new structure and define a new subtype relation to operate on that structure. While I think other solutions are definitely possible, I don't think they'd be all that different from what I've done. Maybe if they turned towards nominal typing.

On the other hand, I'm not necessarily against restricting, weakening, or simplifying any concrete part of the proposal.

[GregRos]

I think I should scrap container types. Or rather call them something else. The subtype relation is supposed to be based on instances, similar to a subset relation. That's not how it works in programming languages in practice, but the idea of having a type with no instances but something else instead may not make sense.

I think it can be explained differently. The functional elements don't have to change -- the relation is still there, kinds look just like did previously, but we just describe it as a different thing.

The container types, instead of being types, are higher-order entities called type objects. Ascended objects if you will. And they have both value members and method members, as we talked about previously.

You define one like this, using the same system as before:

type object Whatever = {
    // I'm less sure how to explain the use of the 'type' keyword here
    // It's important because otherwise people might confuse it for some sort of runtime thing.
    type A = number
    type B<T> = {
        type C = string
        type D = object
    }
}

And type objects can pass for type parameters if they get a kind annotation that’s not *. We can call them a type object parameter in that case.

The subtype relation becomes a sub-object relation, which is a better description. It still has the quality that if A is a sub object of B and B: Kind then A: Kind.

I feel like this makes a lot of sense. Regular HKTs are defined in Haskell as being functions. TypeScript isn't as focused about function types as it is on object types, so it makes sense that the cornerstone of TypeScript's HKT system would be an object.

Maybe kind is not word to use for type types. One way of rebranding them is type class which fits with type object, but it would be confusing because type types aren't really typeclasses and class already means something else.

---

So I'm starting to get a feel for how & and | could work. You could use & on type objects to combine their structures, but | doesn't work because the result can't be a type object, it's some sort of mess.

| can be applied to kinds, but if you have a type object parameter constrained like T: A | B then just like in TypeScript, you'd have to figure out what you're holding. Is it an A or B? And you can only do that using a test.

You could actually reproduce a pattern that's common in runtime TypeScript code:

type object Option1 = {
    type Type = "Option1"
    type OneThing = number
}

type object Option2 = {
    type Type = "Option2"
    type An = {
        type Other= string
    }
}

declare function example<Either: Option1 | Option2>(): 
    Either.Type extends "Option1" ? Either.OneThing : Either.An.Other

I don't think it's that useful here. You ought to be able to just do Either extends Option1, since we're fully in TypeScript's make believe type wonderland.

---

I don't think I'm going to change the original post right now, regarding the type objects. I think the container types are easier to understand than just pulling a "higher-order object" right out the gate.

[MartinJohns]

Because everything is purely structural

It's not. Classes with private members are treated nominally.

[GregRos]

Because everything is purely structural

It's not. Classes with private members are treated nominally.

You're right! Didn't know that. I kind of thought that private member would still be compatible.

Classes are different enough you might be able to make a strictly class-based HKT proposal. This would be turning more towards nominal typing, but it might work.

[rotu]

You can also use symbols. They're kinda designed to be "nominal values"

declare const nominalValue: unique symbol
const NominalType = typeof nominalValue

But note that both classes and symbols are only unique to their declaration. A function that creates a new private class for each call or a new symbol for each call will not create a new type for each call.

---

I don't quite understand what the purpose of this proposal is. What does this seek to do that can't be done with existing HKT implementations?

[GregRos]

Well, as the second paragaraph put it:

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.

1. This proposal aims to express HKTs using the structural principles that underpin the language.
2. It describes how HKTs would interact with ordinary types and each other.
3. It describes how they would be compared, as they are very different from anything else in the language.
4. It talks about how inference would work.

I don't quite understand what the purpose of this proposal is. What does this seek to do that can't be done with existing HKT implementations?

The purpose of this proposal is to be for TypeScript. Existing HKT implementations are for other languages.

There is no other proposal that even tries to answer any of the above questions. They all just point at some other languages and give a few vague examples of possible syntax.

In reality, the many problems posed by HKTs are solved in every language separately. In fact, most don't solve them at all by not having them. It's absurd to think that you can shop around for an existing implementation and just... copy-paste it into the compiler.

[rotu]

As you said:

There are multiple working encodings of HKTs that revolve around type classes and type classes have often been at the center of discussions about HKTs.

Do these libraries you mention fail to capture what you want?

What would you like to express that you can't do in the existing TypeScript language?

How would existing language constructs fail to meet your needs? E.g. the below pattern:

// this is merely a generic type that captures type variables
// the properties exist only to enforce variance constraints
type MappingTypeClass<X,Y> = {
    inX: (x:X)=>unknown,
    outY: ()=>Y
}

// here's a definition of your associated types
namespace MappingTypeClass{
    export type InElement<C> = C extends MappingTypeClass<infer X, any> ? X : never
    export type OutElement<C> = C extends MappingTypeClass<any, infer Y> ? Y : never
    export type InCollection<C> = ArrayLike<InElement<C>>
    export type OutCollection<C> = ArrayLike<OutElement<C>>
    export type Mapping<C> = (x:InElement<C>) => OutElement<C>
}

[GregRos]

As you said:

There are multiple working encodings of HKTs that revolve around type classes and type classes have often been at the center of discussions about HKTs.

Do these libraries you mention fail to capture what you want?

What would you like to express that you can't do in the existing TypeScript language?

How would existing language constructs fail to meet your needs? E.g. the below pattern:

// this is merely a generic type that captures type variables
// the properties exist only to enforce variance constraints
type MappingTypeClass<X,Y> = {
    inX: (x:X)=>unknown,
    outY: ()=>Y
}

// here's a definition of your associated types
namespace MappingTypeClass{
    export type InElement<C> = C extends MappingTypeClass<infer X, any> ? X : never
    export type OutElement<C> = C extends MappingTypeClass<any, infer Y> ? Y : never
    export type InCollection<C> = ArrayLike<InElement<C>>
    export type OutCollection<C> = ArrayLike<OutElement<C>>
    export type Mapping<C> = (x:InElement<C>) => OutElement<C>
}

Well, I'm really not sure how to answer that, so I'd like to provide some background.

HKTs can be described as type parameters that are themselves generic. A basic use-case is expressing the signature of a single map function that takes a generic collection such as Set<T> and returns a collection of the same kind but with a different element type.

In other words, if the function is given a Set<number> and the function x => "" + x, it should return Set<string>. If the collection input is instead a number[], it should return string[].

Here is an example of this in Scala:

//             ↓-- Higher-kinded type parameter
trait Bind[F[_]] {
  def map[A, B](fa: F[A], f: A => B): F[B]
  def flatMap[A, B](fa: F[A], f: A => F[B]): F[B]
}

TypeScript does not have this feature. It has, however, been requested multiple times, with the earliest request being #1213. I participated in the discussion back then and I've been thinking about the problem ever since. I eventually came to realize the feature can't really be applied to TypeScript as-is due to its unique structural type system.

The point of this proposal was to present a concrete system that makes HKTs possible and to describe how they interact with the language's other features.

I hope you see that a library can't really provide this functionality.