Type Enthusiast's Notes about TypeScript. Part 5. Advanced Types

Please Leave Feedback in: git discussions

Previous post: Part 4. Programming with Type Variables.

Disclaimers: (imagine this is a very small font, read it very fast in a half whisper)
I assume strict compiler flags are on, something you get by default with scaffolding, e.g. using create-react-app my-project --template typescript is close enough.
The code examples have been tested with TypeScript v4.5.2.
This post is a pandoc output of a markdown document and code examples are not interactive.
Most of the code examples are published in ts-notes folder in this github repo: ts-experiments.

Motivating Quote for the series:

“TypeScript began its life as an attempt to bring traditional object-oriented types to JavaScript so that the programmers at Microsoft could bring traditional object-oriented programs to the web. As it has developed, TypeScript’s type system has evolved to model code written by native JavaScripters. The resulting system is powerful, interesting and messy.”

From typescriptlang TypeScript for Functional Programmers

Nutshell

This is the fifth post in the series devoted to types in TypeScript. In this series, I explore type-centric approaches to writing code and push TS to its limits in doing so. I am writing these posts for like minded developers who are interested in types and either use or consider using TypeScript.

In the last post I referenced the Types and Programming Languages book. Similarly to the previous post, this installment will be a little more advanced and a little TAPL-ish. I will also introduce a tiny bit of Category Theory. A great blog series (really a book) about Categories is Category Theory for Programmers, here it is on goodreads.

Recursive types

type JsonVal from Part 1 surprised me. It is recursive, the name JsonVal appears on both the LHS and the RHS of the definition. Here is this definition repeated:

type JsonVal = 
| {type: "object", val: Map<string, JsonVal>}
| {type: "array", val: JsonVal[]}
| {type: "string", val: string}
| {type: "number", val: number}
| {type: "bool", val: boolean}
| {type: "null"}

and there are TAPLish reasons why this is interesting:

JsonVal-like types appear to be hard on the TS type checker. I have played with some advanced recursive types and have experienced it first hand. I got quite a few

‘Type instantiation is excessively deep and possibly infinite’

compiler errors (e.g. code in https://github.com/rpeszek/ts-typecheck-peano). However, I did not succeed in creating a simple example to demonstrate this.

Here is another example of a recursive type:

type List<T> = 
| {type: "nil"} 
| {type: "cons", head: T, tail: List<T>}

That is a recursive definition of a functional cons list².

IMO, it is impressive that TS is able to pull these off. I consider this feature very useful and underutilized by the ecosystem. Here is some more advanced use of recursive types:

Type level programming

TS literal types are singletons (i.e. type "boo" has exactly one value "boo":"boo"). This allows singletons to magically connect types with values and values with types. That provides a lot of power to create very precise types.
Literal types should not be that hard to implement in a programming language and it is interesting why they are so uncommon. Kudos to TS for introducing these! They are, clearly, a great fit for JS.
However, TS literal types are very limited in scope (I remember reading somewhere that it was a design decision). For example, you can do some very basic type level string manipulation but you cannot concatenate strings or do any arithmetic on type level numbers and you have no way of defining any additional features on your own (e.g. DIY number addition).

TypeScript allows for type-level ternary (Conditional Types) as well as various type-level built-in functions (e.g. keyof).
Apparently, the type level programming in TypeScript is Turing Complete (see https://github.com/microsoft/TypeScript/issues/14833).
However, type level programming in TS is focused on creating type safety for various JS code idioms rather than creating a foundation for DIY type level programming. IMO this makes it harder to learn. The Turing completeness appears to be a completely accidental language feature.

Type level programming can be very useful, we have seen some of it in action in the previous post where we were able to prevent subtyping and prevent compiler from using the unknown type.

IMO the best language design direction is for the type level and the value level code to look the same (e.g. dependently typed language like Idris). The second best approach is for type level and value level to be very similar (e.g. Haskell).
TS cannot and should not do either. We do not want JavaScript (or very similar) on the type level!

At the same time, the lack of synergy between type level and value level programs makes things very complicated. E.g.:

//example type from https://www.typescriptlang.org/docs/handbook/2/conditional-types.html
type Flatten<Type> = Type extends Array<infer Item> ? Item : Type; 

const head = <T> (t: T[]) : Flatten<T[]> => {
    return t[0] //compiles (as expected)
}

const generalizedHead = <T> (t: T) : Flatten<T> => {
    if(Array.isArray(t)) 
        return t[0]  //still compiles (as expected)
    else 
        return t //compiler error: Type 'T' is not assignable to type 'Flatten<T>' (not as I would expect)
}

here is another one:

type HasContent<C> = {content: C}

type GetContent<T> = T extends HasContent <infer C> ? C : T

const getContent = <C, T extends HasContent<C>> (t: T): GetContent<T> => {
   //return t.content //compiler error:  Type 'C' is not assignable to type 'GetContent<T>' (not as expected)
}

It feels clunky. It feels like type level and value level have a broken marriage. This lack of synergy also feels very confusing.

I think TS type level programming will keep improving and we may see some very interesting use cases in the future.

Subtyping

This series has discussed subtyping already. I will keep this section comparatively short.

Personally, I try to avoid using subtyping features. Subtyping is related to Object Orientation. OO programming has an appeal of simplicity and I was seduced by it for many years. It took me a long time to realize that OO is not that simple. Today, I think about OO as very complex. Even language designers often get it wrong (this series has provided a lot of evidence for this statement in the context of TypeScript). The first 3 parts of this series could have been alternatively titles “Dangers of OO with examples in TS”⁴. This negative view of OO should be filed under IMO as many developers disagree.

Before continuing reading pass this code, please try to implement (at least in your head) the amIFooOrBar function:

function verifyExtends<T2 extends T1, T1>() {}

//more specific, fewer variants
type FooOrBar =  
| {foo: string} 
| {bar: string}

//A challenge: implement this function:
declare function amIFooOrBar(o: FooOrBar): "foo" | "bar"

declare function genFooOrBar(): FooOrBar

//more general, more variants
type FooOrBarOrBuz =
| {foo: string} 
| {bar: string}
| {baz: string}

declare function genFooOrBarOrBuz(): FooOrBarOrBuz

const fooOrBarOrBuz: FooOrBarOrBuz = genFooOrBar() //compiles assigns specific to more general 
//const fooOrBar: FooOrBar = genFooOrBarOrBuz() //will not compile tries to assign general to more specific

verifyExtends<FooOrBar, FooOrBarOrBuz>() //compiles, FooOrBar extends FooOrBarOrBuz
//verifyExtends<FooOrBarOrBuz, FooOrBar>() //does not compile, FooOrBarOrBuz does not extend FooOrBar

The thing to remember is that {foo: string} | {bar: string} extends {foo: string} | {bar: string}| {baz: string} not the other way around.

Did you implement amIFooOrBar, great, let’s move on.

Subtyping in object types will feel familiar to OO developers. Roughly speaking, you can assign object with more properties to object with fewer properties:

type FooAndBar = {foo: string, bar: string} //more general
declare function genFooAndBar(): FooAndBar

type FooAndBarAndBaz = {foo: string, bar: string, baz: string} //more specific
declare function genFooAndBarAndBaz(): FooAndBarAndBaz

const fooAndBar: FooAndBar = genFooAndBarAndBaz()  //specific assigned to general is valid assignment
//const fooAndBarAndBuz: FooAndBarAndBaz = genFooAndBar() // will not compile, tries to assign general to specific

verifyExtends<FooAndBarAndBaz, FooAndBar>() //compiles, FooAndBarAndBaz extends FooAndBar
//verifyExtends<FooAndBar, FooAndBarAndBaz>() //does not compile, FooAndBar does not extend FooAndBarAndBaz

Subtyping gets more involved if you combine adding properties to objects and variants to union types. In TS subtyping extends to functions which makes things even more complex (leading to what I called compilation bloopers in Part 1). But I think the above examples cover the basic idea.

Now let’s revisit the above challenge. What will your function return in this call:

// challenge check:
// what does your function return when used on this value?
// NOTE this does compile, you can assign FooAndBar to FooOrBar, since 'and' implies 'or'
const whatIsThat = amIFooOrBar({foo: "foo", bar: "bar"}) 

This is just one of the many gotchas associated with subtyping.

Thunks and callbacks, never and unknown.

To finish this post I want to pick 4 concepts fundamental to TypeScript: variables, callbacks, never and unknown types and discuss how they relate in a somewhat more theoretical setting. I believe the relationship between these concepts is not commonly understood.

We have seen <T> () => T before, we called it a type hole _: <T>() => T. Now I am changing my mind and want to call it a generic thunk.
We can think about it as a ‘lazy’ value.
Instead of defining const t: T (which, incidentally, TS does not allow on the top level⁵) I can define a function that, when called, will return me that t. Basically thunks are variables you put the () after. A referentially transparent (no side-effects) <T> () => T thunk is morally equivalent to a variable of type T.

A thunk produces a value of type T. A generic callback <T> (_: T) => void consumes a value of type T. There is, clearly, some type of duality between thunks and callbacks.
Incidentally, many programming languages define a unit type often denoted as () instead of the C-style void. If this was the case for TS, we would have written: <T> T => () for the callback and <T> () => T for the thunk. You can get from one type to the other by reversing the arrow =>. These concepts become dual in the categorical sense. This post is not about Category Theory but this section has just a tiny bit of it.

In TS, the generic thunk <T> () => T type is equivalent to never.
You may remember that the type hole _(), was implemented by throwing an error (that is never in TS).
never assigns to everything but you cannot assign anything else to it. Well, except for the generic thunk:

//thunk assigned to never
const nevr : never = _()

export const __neverFn: () => never =  _

In other words <T> () => T and () => never can be assigned to each other, thus, I consider them equivalent.

If you replay the same argument with arrows reversed, you will establish equivalence between the generic callback <T> (_: T) => () and the unknown callback types:

declare function someUnknownCallback(t: unknown): void 
const overbar: <T>(_:T) => void =  someUnknownCallback

declare function someOverbar<T>(t:T): void
const unknownCallback: (_: unknown) => void = someOverbar

The never type is the TS’s bottom type (can be assigned to anything), while the unknown type is the TS’s top type (anything can be assigned to it). These concepts are also dual in the sense of reversing the direction of assignment.

Let’s think about referential transparency again. There are no interesting referentially transparent functions that return void. To do something meaningful, such a function would need to mutate some shared state or do some other effectful things. E.g. when coding in React, a callback could compute a new state (let me call it r: R) and invoke a state hook to make the change. I like to think about such a callback as having an imaginary type <T,R> (t: T) => R.

The duality between variables/thunks and callback is quite fascinating and has some depth.
Let’s fix the type variable T to, say, Person. Any type would do, I just want to remove the quantification (remove the genericity) to simplify my explanation.
JS / TS programs often use higher order functions that accept callbacks as parameters. Consider a callback that accepts a callback (f: (_: Person) => void) => void and computes the same value. The imaginary referentially transparent type for it could be

//TS-like pseudocode
<R> (f: (_: Person) => R) => R

As it turns out, this type is equivalent (isomorphic) to the thunk () => Person (or, ignoring side-effects, to just Person)!
They are not equivalent based on assignments, they are equivalent because one can be easily converted to the other.

It kinda makes sense for a dual of a dual to end up back where we started.
However, this equivalence is a bit stronger, in a sense that it holds for every fixed type T. It is also weaker, since what we get is only isomorphism⁶.

This equivalence is a special case of Yoneda Lemma in Category Theory⁷.

I can express this succinctly in TS (note a higher rank type is used) as:

//all of these compile
type Yoneda<T> = () => <R>(f: (_: T) => R) => R
type Thunk<T> = () => T

//Yoneda<T> is isomorphic to Thunk<T>
//here are functions defining the isomorphism:
const toYoneda = <T> (th: Thunk<T>): Yoneda<T> => {
   const res = () => <R> (f: (_: T) => R): R => f(th())
   return res
}

const fromYoneda = <T> (y: Yoneda<T>): Thunk<T> => {
    const res = (): T => y()(x => x)
    return res
 }

Programmers are divided into 2 camps when exploring this type of information: some consider it fascinating and important, some consider it a lot of useless nonsense. If you are still reading this series, chances are you are in the first camp.

Category Theory is very related to types and to programming in general, I found it only fitting to finish this installment with a note that discussed a little bit of it.
Bartosz Milewski’s CTFP book linked above starts with code examples in C++ and in Haskell. Bartosz gives up on C++ very fast. I think it would be possible to stay on a little longer by selecting TS instead of C++. Kudos to TS!

Next and the final Chapter

I will finish the series with some final thoughts and rants.
The last 2 installments got a little on an advanced side of things. One question I have been asking myself is: When should more advanced types be used in a TS project?

Here is the link: Part 6