Types as Proof

The Swift standard library has a collection called Repeated of an Element that’s repeated count times. Here’s a copy of its basic interface:

public struct Repeated<Element> {
  public let count: Int
  public let repeatedValue: Element

  internal init(_repeating repeatedValue: Element, count: Int) {
    precondition(count >= 0, "Repetition count should be non-negative")
    self.count = count
    self.repeatedValue = repeatedValue
  }
}

// Why a function instead of making a public `init`? I have no idea. 🤷🏻‍♂️
public func repeatElement<T>(_ element: T, count n: Int) -> Repeated<T> {
  return Repeated(_repeating: element, count: n)
}

You can’t repeat something a negative number of times; that doesn’t make any sense. So if you try to create a Repeated with a negative count, it will helpfully assert with a precondition.

Assertions like these can be very helpful. When assumptions are violated, unexpected things will happen: the program might exhibit incorrect, but hard to notice, behavior; or it might crash or deadlock without any clues about the cause.

Assertions help by (1) identifying which assumption was violated (Repetition count should be non-negative) and (2) isolating where the mistake occurred. Asserting early and often can be especially helpful: knowing the time and location of a mistake can be the most helpful information, but also be the most costly.

But no matter how many assertions you add, no matter how specific, no matter how helpful, you’re still left with runtime errors. You’ve made assumptions, and the inevitable mistakes can be hard to catch—even with assertions. Instead of assuming, let’s show our work and prove our logic.

Proof is provided via types.

In the case of Repeated, that’s easy. Negative numbers aren’t valid, so we can use a UInt to restrict the input to values that aren’t negative. Then the compiler can check your work and provide a compiler error if you’ve made a mistake:

error: negative integer '-5' overflows when stored into unsigned type 'UInt'
dump(repeatElement("A", count: -5))
                                ^

The Swift documentation recommends that you not use UInt this way. That’s because UInt isn’t an Int that’s limited to non-negative numbers: the upper half of UInt’s values can’t be represented by an Int. That makes conversions failable in both directions, complicating conversions between the two.

We could design our own type instead, providing a failable initializer that takes an Int and returns nil if the number is negative:

struct NonNegativeInt {
  var value: Int

  init?(_ int: Int) {
    guard int >= 0 else { return nil }
    value = int
  }
}

That makes it easy to convert back to an Int—every NonNegativeInt can be represented as an Int—reducing some of the friction.

Instead of the precondition from Repeated, NonNegativeInt has a failable init. Repeated could also have returned nil instead of using a precondition, but the assertion works better. Return nil when you don’t want to assume. Repeated should assume that you’d give it a non-negative count. NonNegativeInt shouldn’t assume that an incoming Int is non-negative.

This works well in practice because that Int comes from somewhere. It’s best to catch invalid values at the edges of your program, where they originate, and not at the point of use. If this number came from user input, we’d want to provide an error when the user tried to input a negative number. If it came from a JSON API, we’d want to fail during decoding because the server response wasn’t valid.

But I would make an ExpressibleByIntegerLiteral conformance use a precondition. You should assume that a programmer won’t use a negative number when assigning a literal (and they should have some coverage that will easily provide an error if they do).

extension NonNegativeInt: ExpressibleByIntegerLiteral {
    init(integerLiteral value: Int) {
        precondition(value >= 0, "NonNegativeInt must not be negative")
        self.init(value)!
    }
}

That’s not to say that you should model numbers this way (but I’m not saying that you shouldn’t either). This is meant as a familiar example to demonstrate a broader principle: preconditions can be replaced by types.

To apply this generally, it’s helpful to understand the Curry-Howard correspondence. Briefly stated, a correspondence exists between computer programs and logic: types correspond to propositions; functions to inferences; values to proofs; product types to conjunctions; sum types to disjunctions. You can use this correspondence to extend your reasoning from one to the other.

In propositional logic, you might say P → Q, meaning “if P then Q” (an inference with premise P and conclusion Q). If you know P (a proposition), then you can use P → Q to know Q (also a proposition). The process of applying P to P → Q to obtain Q is a proof.

According to the Curry-Howard correspondence, P → Q corresponds to a function (P) -> Q. If you have an instance of P, you can use (P) -> Q to get an instance of Q. You need a value of type P to execute the function, just as you need to know that P is true to make use of P → Q.

There’s an important aspect of this that I’ve only recently understood, thanks to The Little Typer: while types correspond to propositions, values correspond to proofs. If you have a value of a given type, you’ve proven the corresponding proposition. If a type is uninhabited, then it can never be proven. (Never → Q will never prove Q and (Never) -> Q can never be used to get an instance of Q.)

Assertions are assumptions because they’re not stated as premises. Repeated says Element ∧ Int → Repeated (if you have an Element and an Int, then you can get a Repeated). But that’s not correct: You can’t get a Repeated from any Int; it’s assumed that Int will be non-negative. Element ∧ UInt → Repeated fixes the premise, removing the need to assume.

Assertions will alert us when assumptions are invalid. But instead of assuming, we can use a type to create a premise that will let us prove our logic. Compilers can use this to catch our mistakes, eliminating runtime errors.

It’s not always pragmatic to do this, as we’ve seen with UInt. But we have a general principle. Let’s consider a more practical application of this idea.

Consider an iOS app with an in-app purchase to unlock additional features, such as in-app search. Ordinarily you might represent that using a Bool:

// Returns `false` if the in-app purchase doesn't exist or is invalid
func hasPremiumFeatures() -> Bool { … }

Before you launch any premium features, you need to remember to check that flag. Unfortunately, forgetting is easy—especially when you consider the many ways a feature might be launched (buttons, deep links, shortcuts, Siri actions, etc.). If you mistakenly allow basic users to access premium features via any of these methods, then you’ve undermined your business model.

You can add an assertion to catch these mistakes. But now you’ve replaced errant behavior with a crash—one that might not tell you the source of the bug.

final class PremiumViewController: UIViewController {
  init(user: User) {
    precondition(hasPremiumFeatures())
    …
  }
}

Instead, we can replace this boolean flag with a type that represents the presence of premium features. This type is proof of the in-app purchase. It doesn’t need to carry any information; it only needs to limit your ability to create a value of that type.

struct HasPremiumFeatures {
  // Returns `nil` if the in-app purchase doesn't exist or is invalid
  // You might want to pass in data here. Or maybe you want to decode a JSON
  // model but replace a boolean property with a type like this. If its `init`
  // is marked `private` so that it can only be created via JSON decoding, then
  // you have a way to provide proof.
  init?() { … }
}

Now your view controller can list HasPremiumFeatures as an input. It doesn’t need to do anything with it. But requiring a HasPremiumFeatures adds a premise that states that you can only create this view controller if you have premium features.

final class PremiumViewController: UIViewController {
  // Add a property to ensure that any added `init`s also require this
  let hasPremiumFeatures: HasPremiumFeatures

  init(hasPremiumFeatures: HasPremiumFeatures) {
    self.hasPremiumFeatures = hasPremiumFeatures
    …
  }
}

This should feel somewhat familiar: having a T? and another type that requires a T is a common occurrence in languages like Swift. This is exactly why Optional types are important: requiring a non-null T replaces runtime errors with compile-time errors by replacing an assumption with proof. But we can use this more generally to move other assumptions into the type system.

Many premises can’t be expressed with types in Swift because the type system is limited.¹ But there’s a lot that you can prove in Swift this way—even it it's just a single boolean like we've done here. Next time you write a precondition, stop and consider whether you can use a type instead.