Type-Driven Development with Swift

I recently started reading Type-Driven Development with Idris, by Edwin Brady. It’s been enlightening to learn about Idris’s dependent types; I highly recommend it. I've found the book to be very approachable.

In Type-Driven Development, as presented in the book, you focus on the types of your functions before implementing them. After the types compile, you go back and write the actual code. This gives you a proven foundation for your code. (Proven because types are proofs.)

Idris does this with holes, which fill in for an expression that you haven't written yet.

module Main

main : IO ()
main = putStrLn ?greeting

?greeting is a stand-in for the value that’s going to be printed. Idris will report the type of the hole. In this case, ?greeting is a String.

Swift doesn't have holes (maybe it should??), but I’ve found myself using a very similar technique with fatalError. I can figure out my types and then fill in the implementations. This is particularly useful when I’m unsure how to represent a concept in the type system.

enum Result<T, E: Error> {
    case success(T)
    case error(E)

    func andThen<U>(_ action: (T) -> Result<U, E>) -> Result<U, E> {
      // I can work out the types before I write this
      fatalError()
    }
}

let x = Result  // Oops! `T` and `E` can't be inferred.
    .success(3) // I can figure this out before implementing `andThen`.
    .andThen { value in
        return .success("foo")
    }

This works at the top level of your program. But it can also work as you implement a given function:

extension Result {
    func andThen<U>(_ action: (T) -> Result<U, E>) -> Result<U, E> {
        switch self {
        case let .success(value):
            return action(value)
        case .failure:
            // I can come back to this after finishing the `.success` case
            fatalError()
        }
    }
}

This has been a very handy tool for me in the past month. Type inference can be hard to predict, and this lets me work through an API without spending the time implement it.