Thread by @YuriyBogomolov

Welcome to ninth episode of #monadicmonday! Today I would like to return to the roots of this series and provide you with a few "take and go" recepies for type-level programming in TypeScript.

Let's start with the basics. Type-level programming means that we express statements using types, and ask compiler to check them. In TypeScript, we use conditional types to infer our statements to be either `never` (bottom type) or some meaningful type.

The first useful operation is type-level `If` operator, which can be expressed like so:

Let's write some tests for it! First of all, we need a way to run type-level assertions. We can use a specialized tool, `dtslint`, from Microsoft, but its setup is a bit painful, so let's stick with something simple like `jest`.

We start with an `assertType` function, which will compile only if its parameter is not `never`:

Our test for `If` will look like this:

Practically, I find myself mostly using checks against `never`, so let's define `IfDef` type operator and write tests for it:

Another useful type operation is `OrElse`, which falls back to its second argument if the first is `never`:

Now let's define something more interesting. Say, let's check if two types intersect each other:

Another great type operation I often use is `AtLeastOne`. It transforms a partial type into a union of types with one required field from the whole set:

Finally, let's prohibit type from being widened:

Now I would like to show you how to use these type-level operations in your code. For example, you're writing a function which requires its arguments to never intersect:

And now let's have some type-level fun! As you (probably) know, TypeScript's type system is close to be Turing-complete:
github.com/Microsoft/Type…
So we can play a bit with it and see where it may lead us :)

Since TS@2.0 a lot happened to its inference engine, so it's hard to express recursive types. However, we still can, for example, describe a type-level list and reverse it. Or define a type-level Peano numbers. Let's dive in!

First of all, we need some Boolean values on type level – they are bread and butter of type-level checks:

Next, let's write a definition of a heterogeneous list, which is either empty or consists of a head and a tail:

Next, we'll need some "functions" to create and manipulate our lists:

Having these, we can finally write the `Reverse` type. To reverse a list, we take its head and append it to a reversed tail:

Using the exact same technique, you can define type-level Peano numbers:

And even combine these two types:

Curcious reader may find familiar patterns – for example, `Nat` definition is almost the same we used in the third episode about recursion schemes:

https://twitter.com/YuriyBogomolov/status/1117723946005213185

If we had proper recursive types in TypeScript, we could define recursion schemes on the type level. However, I see little to none practical day-to-day usage of such possiblity.

As a final note, I would like to reference a module with some neat (and practically useful!) type-level operations from @GiulioCanti: github.com/gcanti/typelev…

@GiulioCanti Another great resource I've used during preparation of this episode is the following blog post in Japanese from @ryotakameoka:
ryota-ka.hatenablog.com/entry/2017/12/…

@GiulioCanti @ryotakameoka That's all, folks. Hope you liked this episode! And stay tuned for May's compilation and next episodes ;)

As usual, all code examples are available at github.com/YBogomolov/mon…