Type Driven Development: Property Tests

Part 11 – Property Tests

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

We’ve got more than enough type knowledge to build total functions. Type safety is a spectrum; is there a way to determine how total our functions are? A few. One particular way is to utilize Property Tests. You write a single unit test, it generates 100 random inputs. If one of those inputs fails, it’ll give you the random seed so you can test the exact sequence of inputs yourself (e.g. fast-check, jsverify):

type FormatName = (name:string) => stringCode language: JavaScript (javascript)

How could formatting a string fail? Let’s write 1 property test w/100 random strings to see:

forAll(string(), name => {
  expect(() => formatName(name)).not.toThrow()
})Code language: JavaScript (javascript)

It failed; logs show an empty string ” and a blank string ‘ ‘ made it fail. We can either fix this code:

name.trim()[0].toUpperCase() + name.trim().slice(1)Code language: CSS (css)

… or just fix the types:

type FormatName = (name:NonEmptyNorBlankString) => stringCode language: JavaScript (javascript)

Discriminated Unions + TypeState can help make Impossible Situations Impossible, but Property Tests beyond just the compiler can help prove it:

type State
  = { tag: "Loading" }
  | { tag: "Success"; data: Data }
  | { tag: "Failure"; error: string }Code language: JavaScript (javascript)

The DU + compiler prevents this impossible state:

{ loading: true, data: user, error: "bad" }Code language: CSS (css)

But not that your React useReducer goes from “Loading” to “Success” when you get data. Here be dragons and race conditions 😄!

Valid transitions:

Loading -> Success
Loading -> Error
Loading -> Error -> Retry -> Success
Loading -> Cancel -> Error

We can then generate random sequences like the above with just 1 test to ensure our state transition function’s like we’d expect:

test("random action sequences result in valid transitions", () => {
  // generate a random action sequence
  forAll(randomActionSequence(), sequence => {
    // loop through that sequence, then transition to each state
    forEach(sequence, ([action, previous]) => {
      // get the next state
      const next = reducer(previous, action)
      // see if you're actually allowed to transition to that state
      expect(
        isAllowedTransition(previous, action, next)
      ).toBe(true)
    })
  })Code language: PHP (php)

Again you’re left with a choice if it breaks; do you improve the code, or narrow your type to prevent invalid transitions? Up to you!

Types can prevent bad values from ever existing. You/your team will reach a point where your types may hurt your brain, instead relying on code to preserve the truth types cannot. Property Tests can help ensure the code does that.