Type Driven Development: Type Proofs

Part 12 – Type Proofs

This is a series of posts I’m writing about using types as another tool in software development, Continuous Delivery, & keeping LLM’s honest. They’re also a design & refactoring tool, a communication tool, and reduce how many tests you have to write.

Parts

1. Part 1 – Branded Types
2. Part 2 – Product Types
3. Part 3 – Union & Discriminated Unions
4. Part 4 – Non-Empty Collections
5. Part 5 – Indexed Types
6. Part 6 – unknown vs any
7. Part 7 – Result
8. Part 8 – Schema
9. Part 9 – Total Function
10. Part 10 – Errors as Values
11. Part 11 – Property Tests
12. Part 12 – Type Proofs
13. Part 13 – Exhaustiveness Checking
14. Part 14 – Parse, Don’t Validate
15. Part 15 – Anti-Corruption Layer
16. Part 16 – Opaque Types
17. Part 17 – Maybe
18. Part 18 – Smart Constructors
19. Part 19 – Pipeline
20. Part 20 – Railway Oriented Programming
21. Part 21 – Typestate
22. Part 22 – Capabilities
23. Part 23 – Immutability
24. Part 24 – Making Impossible States Impossible
25. Part 25 – Type Driven Development: How to do it
26. Part 26 – Final Thoughts

Type Proofs allow you to write functions in the type system that assert something is true. Where the type system doesn’t allow u to easily express something like u could in say Scala or Haskell instead TypeScript provides the ability to write your functions to express those facts.

type Assert = T
type Cow = false
// ❌ below line does not compile
type _CowIsTrue = AssertCode language: JavaScript (javascript)

The Assert is a type-level assertion. They’re like unit-test assertions expect(thing).toBe(true), much like Vitest’s type level tests expectTypeOf/assertType. The difference is u can build your own from these low-level Conditional & Map types.

Let’s say u want to create the > and < symbols as types so you can prove an Array or Tuple is in the right order. Let’s make >:

type GreaterThan<
  A extends number, 
  B extends number, 
  Acc extends unknown[] = []
> =
  Acc['length'] extends A ? false :
  Acc['length'] extends B ? true :
  GreaterThan<A, B, [...Acc, 0]>Code language: JavaScript (javascript)

Ok, recursive weird looking 😜. But like runtime functions, you can create new type functions from other type functions:

// swap B and A for GreaterThan
type LessThan<
  A extends number, 
  B extends number> =
    GreaterThan<B, A>Code language: HTML, XML (xml)

Finally, we’ll create an assert to say if the type is true or not:

type Assert<_ extends true> = voidCode language: JavaScript (javascript)

Now we can write type-level tests:

type Eight = 8
type Nine = 9
// ❌ does not compile
type _nope = Assert<GreaterThan<Eight, Nine>>
// ✅ compiles
type _yup = Assert<GreaterThan<Nine, Eight>>Code language: JavaScript (javascript)

Baller.

Caveat: Type Proofs can also mean using @ts-expect-error to practice Type Driven Development. More confusing, you can use the type-level functions above in addition to @ts-expect-error to write type test suites.

Type Proofs can also just be helpful types to help in development. You’ve may have used the native ones like Partial<T> and ReadOnly<T>. You can also build your own. Want all permutations of AWS regions, us-east-2 and us-west-1?

type Regions
  = [ 'us-east-2', 'us-west-1' ]
  | [ 'us-west-1', 'us-east-2' ]Code language: JavaScript (javascript)

Imagine if you added a 3rd region like eu-west-2; now you have 6 unions w/3 items in the tuple; I ain’t writing that by hand. Instead, build a Permutations type, then go:

type AWSRegions = ['us-east-2', 'us-west-1', 'eu-west-2']
type Regions = Permutations<AWSRegions>Code language: JavaScript (javascript)

Type Proofs help assert your types are doing what you think they are w/additional checks; e.g. ensuring you can only add Money<'USD'> to Money<'USD'>, but fails for Money<'EU'>, that functions were called in the right order for Type State, & evidence logic worked with Phantom Types. They also create helper functions to make more advanced types + custom compiler errors. They don’t compile into your code so don’t affect file size.