Type Driven Development: Total Function

Part 9 – Total Function

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 safety is a spectrum. A gradual type system widens the spectrum in a good & bad way; u have flexibility to discover your domain as it emerges w/less strict types + integrate w/less typed & legacy systems. That has a cost in safety. Sometimes u can narrow what’s allowed through types, then expand to other possibilities as you learn more. Whatever you choose, aim to design Total Functions; every input returns a sensible value.

Most functions we create are called Partial Functions; functions that throw/crash, or return nonsensical inputs for some inputs.

type Divide = (a:number, b:number) => numberCode language: JavaScript (javascript)

Divide looks like a normal function; notice I only provided the type signature. From that you can figure out how the function works:

divide(12, 6) // 2
divide(2, 1) // 2Code language: JavaScript (javascript)

What about 2 / 0? That’s infinity. Technically it’s a number type, but is that what I want? What about 0 / 0? That’s NaN. While it’s called “NOT a number”, it’s also technically a number. Perhaps I just want numbers I can show the user? That means division can fail, so let’s fix the type:

type Divide = (…, …) => Result

divide = (a, b) => {
  let n = a / b
  if(nIsAGoodInteger(n)) {
    return ok(n)
  } else {
    return err(…)
  }Code language: JavaScript (javascript)

Now it’s more clear; infinity, negative infinity, & NaN will cause an error. But this is awkward to use; math requires error checking now? Blech… what if we ensure the inputs are good instead?

type Divide = (a:number, b:PositiveInteger) => numberCode language: JavaScript (javascript)

Much easier to work w/ + expected outputs. More total.

What about fetch? Many would say:

type fetch = (url:string) => Promise<Response>Code language: JavaScript (javascript)

but technically it can also crash; u have no internet, u provide a bad URL, JSON fails to parse, blah blah blah. A more total signature would be:

type safeFetch = <T>(url:string) => 
  ResultAsync<T, FetchError>Code language: HTML, XML (xml)

We “expect” some type to be returned from our service; that implies a Schema is involved. It’s not a Result, but a ResultAsync, which implies a Promise. The error is specifically a FetchError type. The name has “safe” in it, implying no exceptions thrown. All that from just reading the type signature. More total.

Partial functions have type signatures that lie to you. They say “Oh yeah I return a Promise<T>”, but all kinds of bad things happen the type signature doesn’t tell you about. The ResultAsync<T, FetchError> is extremely clear & thorough.

Once u start composing these functions together to make programs, that makes your code more total. “when it compiles it works” is more likely to be true. Your app’s type signature, whether UI or API, is more likely to be total.

type AWSLambda = (event:APIGatewayProxyEvent) =>
  ResultAsync<HttpResponse, never>Code language: JavaScript (javascript)