Introduction to Type-Level programming in TypeScript

Fernando Silva

Fernando Silva

fersilvaa16fersilva16
Woovi Logo

Software engineer

Overview

  • What are Types?
  • Primitive types
  • Literal types
  • Data structures
  • Union types
  • Intersection types
  • Special types
  • Conditional types
  • Infer types
  • Template literal types
  • Examples
  • Real use cases

What are types?

  • Just sets
  • Set theory
Sets

Primitive types

  • Built-in types
  • number
  • string
  • boolean
  • symbol
  • bigint
  • undefined
  • null

Literal types

  • The exact types
  • "apple"
  • 1
  • true
Literals

Data structures

  • Objects: { a: string }
  • Records: { [key: string]: string }
  • Tuples: [string, number]
  • Array: string[]

Union types

  • Join types together
  • a | b
Union

Intersection types

  • What belongs to both types
  • a & b
Intersection
Intersection object

Special types

  • unknown
  • never
  • any

Unknown type

  • Contains every type
  • a | unknown = unknown
  • a & unknown = a
Unknown

Never type

  • Empty set
  • string & number
  • a | never = a
  • a & never = never
  • const crash = (): never => process.exit(1);
Never

Any type

  • Doesn't fit in the set theory
  • Both supertype and subtype of every other type
  • Bad practice
  • a & any = any
  • a | any = any
Any

Conditional types

  • extends
  • "Hello" extends string ? true : false

Infer types

  • { a: string } extends { a: infer V } ? V : never

Template literal types

  • type T = `$0 (${number})`

Examples

Naturals

type Zero = 'Zero';
type Suc<N extends Nat> = `Suc<${N}>`;
type Nat = Zero | Suc<any>;
type Add<X extends Nat, Y extends Nat> = Y extends Zero
  ? X
  : Y extends Suc<infer YP>
  ? Add<Suc<X>, YP>
  : Zero;
type a1 = Add<Suc<Zero>, Suc<Zero>>;
//   ^? type a1 = "Suc<Suc<Zero>>" -> 3
type Sub<X extends Nat, Y extends Nat> = X extends Suc<infer XP>
  ? Y extends Suc<infer YP>
    ? Sub<XP, YP>
    : X
  : Zero;
type s1 = Sub<Suc<Suc<Zero>>, Suc<Zero>>;
//   ^? type s1 = "Suc<Zero>" -> 1
type Mult<X extends Nat, Y extends Nat> = Y extends Suc<infer YP>
  ? Add<X, Mult<X, YP>>
  : Zero;
type m1 = Mult<Suc<Suc<Zero>>, Suc<Suc<Zero>>>;
//   ^? type m1 = "Suc<Suc<Suc<Suc<Zero>>>>" -> 4
type _Div<
  X extends Nat,
  Y extends Nat,
  Q extends Nat,
  R extends Nat
> = X extends Suc<infer XP>
  ? R extends Suc<infer RP>
    ? _Div<XP, Y, Q, RP>
    : _Div<XP, Y, Suc<Q>, Y>
  : Q;
type Div<X extends Nat, Y extends Nat> = Y extends Suc<infer YP>
  ? _Div<X, YP, Zero, YP>
  : Zero;
type d1 = Div<Suc<Suc<Suc<Suc<Suc<Suc<Zero>>>>>>, Suc<Suc<Zero>>>;
//   ^? type d1 = "Suc<Suc<Suc<Zero>>>" -> 3

Nat definition

T function options

type TemplateOptions<S extends string> =
  S extends `${string}{${infer K}}${infer R}` ? TemplateOptions<R> | K : never;
type t1 = TemplateOptions<'Translation {count} {anotherKey}'>;
//   ^? type t1 = "count" | "anotherKey"

Naturals

type Zero = 'Zero';
type Suc<N extends Nat> = `Suc<${N}>`;
type Nat = Zero | Suc<any>;
type Add<X extends Nat, Y extends Nat> = Y extends Zero
  ? X
  : Y extends Suc<infer YP>
  ? Add<Suc<X>, YP>
  : Zero;
type a1 = Add<Suc<Zero>, Suc<Zero>>;
//   ^? type a1 = "Suc<Suc<Zero>>" -> 3
type Sub<X extends Nat, Y extends Nat> = X extends Suc<infer XP>
  ? Y extends Suc<infer YP>
    ? Sub<XP, YP>
    : X
  : Zero;
type s1 = Sub<Suc<Suc<Zero>>, Suc<Zero>>;
//   ^? type s1 = "Suc<Zero>" -> 1
type Mult<X extends Nat, Y extends Nat> = Y extends Suc<infer YP>
  ? Add<X, Mult<X, YP>>
  : Zero;
type m1 = Mult<Suc<Suc<Zero>>, Suc<Suc<Zero>>>;
//   ^? type m1 = "Suc<Suc<Suc<Suc<Zero>>>>" -> 4
type _Div<
  X extends Nat,
  Y extends Nat,
  Q extends Nat,
  R extends Nat
> = X extends Suc<infer XP>
  ? R extends Suc<infer RP>
    ? _Div<XP, Y, Q, RP>
    : _Div<XP, Y, Suc<Q>, Y>
  : Q;
type Div<X extends Nat, Y extends Nat> = Y extends Suc<infer YP>
  ? _Div<X, YP, Zero, YP>
  : Zero;
type d1 = Div<Suc<Suc<Suc<Suc<Suc<Suc<Zero>>>>>>, Suc<Suc<Zero>>>;
//   ^? type d1 = "Suc<Suc<Suc<Zero>>>" -> 3

Nat definition

Lambda Calculus

Lambda Calculus parser and interpreter made in TypeScript's type system

https://github.com/fersilva16/lcts

Real use cases

  • Almost none
  • For production: Keep it simple

Thanks

We are hiring!

woovi.com/jobs