Total programming in Swift

Edit: I was interviewed for the Corecursive podcast on this very topic. You can find the podcast episode here along with a great selection of other interviews https://corecursive.com/007-total-programming-using-swift-with-andre-videla

Swift is a very nice language because it tries to make the programmer do the right thing from the very beginning. One of the good things it encourages is totality.

What it totality ?

A total program is a program that will never get stuck, crash or run into an infinite loop. It will always terminate correctly in a finite amount of time. If your program is total and is well-typed, then a situation where it crashes or gets stuck cannot exist¹. There are many ways in which a program can be non-total. Here are a few examples:

• Getting stuck because of a deadlock or an infinite loop
• An edge case is not handled and will crash the program
• A malformed input puts the program in a corrupt state

Thus, totality embodies the phrase that “well typed programs cannot go wrong”² .

This property is extremely useful in day-to-day programming because is alleviates (but does not eliminate) the need for tests, it increases the confidence you can have in the code and it allows to reason about your codebase as small trustworthy chunks. Most programs in use are not total, for example, most of them are meant to be run forever (web servers, mobile apps, deamons). But even if the overall program isn’t total it is useful to have parts of it that are total. Though I will talk about “total programs”, in practice those will be “total functions”, therefore I will use both words interchangably.

In this post I will present how null pointers and unchecked exceptions work against totality, then I will show how Swift encourages totality by getting around those two problems. After that we will see how Swift’s promises of totality can be silently broken using the ! operator in different contexts and will finish with some example of how to write simple and safe code while avoiding !. Though the subject of totality is deeply linked with non-termination I will not talk about it.

(Footnote 1: This is all good and well but at no point does Swift check if your program is total. It merely happens to encourage practices that, almost by accident, makes programs total. There are many reasons why Swift does not check for totality, but the most compelling one is that it’s mathematically impossible.
Indeed, checking for totality means checking that a program will always terminate (no infinite loops), and will terminate in a “good” state (no crash). The termination problem is more generally known as the “Halting Problem”,it was popularised and proven impossible to solve by Alan Turing using his Turing machines. There exist programming languages which have a limited form of termination checking like Idris or Agda, but given an arbitrary program, they cannot decide whether it terminate or not. And so, they will be unable to tell whether the program is total or not.)

(Footnote 2: The original source of this phrase comes from this paper from Milner. The context of this statement is that there exists a soundness proof for this particular type system, and therefore, any well typed expression is sound.)

Null references

The null reference finds its origins in low-level languages where the programmer manipulates pointers to values in memory³. Such languages make heavy use of pointers to access addresses in memory which hold all the data structures that are used in the program.

For example, in a Linked List it is common to represent each node as a pair of pointers: a pointer to the value currently held and a pointer to the next node in the list.

This raises the question of how to represent the final element of the list? One possibility is to have the last element of the list be a special node with no second pointer. This makes the Linked List API more cumbersome to use: now every pointer to a list node must be tested and cast into either a “middle node”, or a “final node” which does not have a “tail pointer”.

A List with a“middle node”(square) and a “final node”(circle)

Moreover, that makes adding elements at the end of the list a bit more cumbersome too because you would have to create a middle node, put the value of the last node in the new middle node, make the predecessor of the last node point to the new middle node, replace the value in the last node by the new value, make the new middle node point the the last node.

Another way to implement the last element is to have the last pointer be “dangling” and not point to anything. It could for example point to a special reserved value (0 for example) which is uninitialized in memory; since all such “dangling” pointers are the same we can easily compare them. Because we use such pointers quite commonly, we give it a name and call it null.

List ending with a pointer to Null

We can now add elements at the end of the list by simply replacing the final null pointer by a pointer to the new last element, and set the last element’s tail pointer to null.
That makes our LinkedList API simpler and more elegant, at the price of safety. Indeed, dereferencing such a pointer will (in the general case) crash your program since you are accessing uninitialized memory.

Null references carried over to other programming languages like Java, C# and others in order to represent data structures like Linked List in exactly the same way as C. In those languages, pointers are not first class citizen anymore but we still can have a NullPointerException or NullReferenceException when trying to use a reference without realising that it is null.

(Footnote 3: The null pointer has been called “The billion dollar mistake” by Tony Hoare who introduced null references in Algol W in 1965. I encourage you to listen to his talk about the null reference here https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare)

The Optional Type

Swift does not have null references. Instead it makes use of its type system to represent things like missing values, or references that can be invalid. In both those cases the type Optional<T> is used. It does not represent “The null pointer” itself because it is not a reference⁴, rather, it is a value from an enum⁵:

enum Optional<T> {
    case some(T)
    case none
}

This type signals that an optional carries a value of type T in a some or it carries nothing and has value none

We can now use our Optional type to model things that previously required a null pointer. The difference is that the type checker will require us to handle both the case where a value is found (some) and when a value is missing (none). It also serves as accurate documentation, explicitly stating that a value might go missing.

(Footnote 4: The none case, or nil is _also_ used to model null pointers. For example in the case of a weak reference that might be deallocated at any point, the case where the reference is deallocated and no longer valid is represented using nil)

(Footnote 5: Optionals are implemented using enums. Enums are Algebraic Data Type they allow us to combine existing types, including generics, in order to build complex structures like trees, lists, state or simple enumerations. All enum values are immutable.)

About Swift notation

Swift has a lot of syntax sugar for handling optionals. Here is a small list of shorthands that we will use:

• An optional value like Optional<String> will be abridged String?
• We can write nil instead of none ⁶
• We can check if an optional value contains something by using a special if-statement: if let … here is an example:

let present: String? = "someString"
let absent: String? = nil
if let message = absent {
    // if absent contained a value it would have been bound to the
    // "message" identifier. But in this case there is nothing in
    // "absent" therefore this branch will not be taken
} else {
    //this branch will be taken since absent = nil
}
if let message = present {
    // branch taken
    // we can use "message" and it will have the value "someString"
}

(Footnote 6: the nil keyword might be confusing to people coming from Objective-C or Go. Indeed those languages use nil to represent the null pointer but in Swift it’s just syntax sugar for the value none.)

Linked Lists revisited

We’ve seen the example of the linked list for a use of null pointers. We could imagine making use of nil to represent linked list in the same way than before:

//We have to use a class here and not a struct because structs 
//cannot be recursive
class Node<Elem> { 
    let element: Elem
    let tail: Node<Elem>? 
}

And use it like this

func countList<Elem>(_ list: Node<Elem>) -> Int {
    if let rest = list.tail {
        return 1 + count(rest)
    } else {
        return 1
    }
}

But there is a huge problem with this function: It cannot accept empty lists. Worse, empty lists are not even representable! When using null pointer this is not a problem because an empty list is a null pointer to a Node. You can translate this but it become quite unnatural quickly:

// Here we expect a "Node<E>?" because the
// empty list is represented as nil
func countList<Elem>(_ list: Node<Elem>?) -> Int {
    if let nonEmptyList = list { 
        return 1 + countList(nonEmptyList.tail)
    } else {
        return 0
    }
}

You can alleviate that by using a typealias

typealias List<Elem> = Node<Elem>?

but clearly we are dealing with one level of indirection too many. Types are supposed to help us and here they seem to obfuscate important information from the user. We want to clearly indicate that a list is either empty, or contains an element and the rest of the list. Passing nil as argument does not communicate that.

Algebraic data types

Algebraic data types (abridged ADT) allows us to create new types from other types by combining them in two ways: Sums and products. We won’t dive in the theory of it but it’s useful to keep in mind that when someone says “a sum type” they mean “combining types using enums” and when they say “a product type” they mean “combining types using a struct”. The work “sum” encapsulate the idea of “choice” between values and “product” refers to putting values alongside other values.

We can actually do much better than our optional Linked Lists using ADTs. Indeed, we can define an enum which has two cases: Either it carries a value and the rest of the list or it carries nothing.

// See footnote 7
enum List<Elem> { 
    //List that contains nothing
    case Empty
    //List that contains an element and the rest of the list    
    case Node(Elem, List<Elem>) 
}

This makes the use of lists much more streamlined:

func count<E>(list: List<E>) -> Int {
    // See footnote 8
    switch list {
    case .empty: return 0
    case let .node(elem, rest): return 1 + count(list: rest)
    } 
}

We’ve been able to completely eliminate the need for optionals, we simplified the API (no more optional wrapping) and we made this clear in the type: A list is either empty, or a node which contains a value and a list.

(Footnote 7: Node is typically called Cons and Empty is typically called Nil. This convention from LISP in which you would build lists by using the cons (for constructor) function to pair up elements and lists. The first element of the list would be called car and the rest is called cdr. In more recent years it is common to refer to those two as head and tail.)

(Footnote 8: Note the use of the switch statement. Switches are very useful to destructure data safely. Swift will enforce that your switch is exhaustive and does not leave out cases. If you do not want to handle all cases you case insert a catch-all case with default or case _ . Switch statements encourage the programmer to write total program by checking it’s exhaustiveness and will refuse to compile if cases are missing.)

Error Handling

Exceptions also have their roots in low level programming. The first instance where you can find “exception-like” behaviour is deep inside the implementation of your CPU.

CPUs have a mechanism to interrupt their current computation if something unexpected comes up. This mechanism, called interruptions, is ubiquitous in cpu design and implementation. They are useful for many things like handling IO, signaling a hardware errors, communicating with the software running on the CPU (like the scheduler) and more.

Encountering a null reference will throw an exception

Exceptions in programming languages are a bit like interruptions, they interrupt the current flow of execution and expect that something is done in order to handle the error. If the exception is not handled it will propagate until it’s handled, otherwise the program is killed.

This is fine in principle but is a huge problem when trying to write total programs. Indeed, if any part of your code is able to throw an exception and you are not aware of it, or not able to handle it correctly, then your program will crash. This breaks totality since a well typed program can crash because of an exception.

When writing code that is total you should be able to trust every bit of information available to you. That includes knowing if the functions you call can throw exceptions, and if they do, manage the error accordingly. If you cannot tell that your program can crash, then you cannot be sure that your program is total.

Checked exceptions

One way to go back from untrustworthy exceptions to totality is to enforce that every exception that is possibly thrown is handled. That implies that the compiler has to know in advance which exceptions a pice of code can throw and ensure that the caller handles the potential errors. Java for example has checked exceptions in the form of the Exception class. Any exception that is thrown and extends Exception has to get caught and handled. Unfortunately Java also has a RuntimeException class which bypasses the exception check. That means that methods that are not marked as “throwable” can still throw exceptions and crash.

Swift’s error handling model does not make use of exceptions in the same way than other programming languages do, even though it borrows a similar syntax⁹. Functions that can emit errors have to be marked as “throws” in their type signature¹⁰

// state change that can fail
func open(door: Door) throws -> Door 

If you call a function that can throw you have to handle it in a do/ try/ catch block (You can also use try? and try! we will talk about them later)

do { 
    let openedDoor = try open(door: slidingDoor)
} catch Jammed { 
    print(“door is jammed”)
} catch error {
    print(“unknown error”)
}

If the user writes

let openDoor = open(door: slidingDoor) // no try

the compiler will emit an error suggesting that the error should be caught and will not compile.

(Footnote 9: The error handling model in swift does not work in the same way that other programming language implement exceptions. In particular, throwing an error does not causes the unwinding of the call stack. Rather they signal that the function can return one of two things: either a value, or an error. In essence, this is analogous to returning a generic Result Type that you can find in other languages like Scala or Rust. Note that Swift does not have a canonical Result type, most libraries implement their own result type.)

(Footnote 10: Currently functions and methods marked as throws do not disclose which type of error they might emit. The subject of “Typed throws” still stirs a lot of discussion among the users of the Swift-evolution mailing list.)

Why “!” is pure evil

Even though Swift has pretty reasonable defaults and very useful abstractions to make use of the powerful type system, it also is equipped with a number of escape hatches that are to be used carefully. And most of them are, for example unsafe raw pointer manipulation¹¹ or calls to fatalError.

But one of those escape hatches stands out because it is extremely extremely dangerous and easy to use: It is the ! operator.

(Footnote 11: Even though raw pointer manipulation is possible in Swift, its use is rare and niche. You will mostly find in low level libraries which interact with C a lot. Most users will not write or read such code)

Optional Unwrapping

In the case of optionals, the ! operator allows the programmer to convert an optional value into a non-optional value (going from T? to T) by extracting the value if it’s present, and crashing if it’s absent. Swift does not issue any message when you call a function that might crash because of !. For example, given this function:

// Safe division by 0, if we divide by 0 we return "nil"
func divide(_ n: Int, by divisor: Int) -> Int? {
    if divisor != 0 {
        return n / d
    } else { 
        return nil 
    }
}

Can you tell why this compiles

func complexCalculation(value: Int) -> Int { 
    return 3 * value + divide(17, by: value + 30)! * 42
}

and not this

func complexCalculation(value: Int) -> Int { 
    return 3 * value + divide(17, by: value + 30) * 42
}

As a hint I will give you the error message: value of optional type ‘Int?’ not unwrapped

That’s right, the function divide might return nil so we have to handle the case where the division fails. If it returns nil then it cannot be added or multiplied. Unfortunately, the first function hides this property using ! and assumes that divide will never return nil. In doing so it makes any program that relies on complexCalculation unsafe because it might crash with some input and the possibility of a crash is not visible in its type.

Ignoring possible errors

A similar situation exists with throwable functions. If the users writes try! in front of a throwable function then Swift will not require the function to be wrapped in a do/ try/ catch block and will crash if it returns an error.

func openFile(path: String) throws -> FileHandle
func openAndRead() { 
    let file = try! openFile(path: “test.txt”)
    let stream = try! file.read()
}

Swift will happily compile this code and crash at runtime if the file “text.txt” is not found or if the program does not have the rights to open such a file.

Hiding the fact that your functions can crash makes your program typecheck while breaking the assumption that “well typed programs cannot go wrong”

Alternatives to “!”

Most of the time, ! operators are used in order to avoid repetitive checks and make the assumption that nil or errors should not even occur. But there exists ways to keep the code clear and clean without compromising its safety. Moreover, if your code needs a ! because you can provably ensure that it will not encouter a nil or an error, then you can probably update your type signatures such that you can avoid the use of !.

Optionals

A problem many people starting out with optionals will encounter is that they seem to spread throughout your codebase. This is simply a product of inexperience with the new paradigm that programming with optional brings. Indeed, previous experiences has taught those programmers to actively check for null references, but optional types do not require such cumbersome and “old fashioned” practices like “manually checking if the value is present”. Instead, operations on optional can be carried out normally provided that they are “lifted”¹² using functions like map or flatmap¹³.

for example instead of writing:

// transfrom string into JSON, return nil if string is unparsable
func parseJSON(from string: String) -> JSON? { … }
// parse a possibly missing json into a possibly missing user
// unfortunately passing nil here would not make any sense would it?
func parseUser(json: JSON?) -> User? {
    if let json = json { 
        //parse json
    } else {
        return nil
    }
}
// combine everything
let parsedUser: User? = parseUser(parseJSON(from: userInput))

write

// parse a JSON into a user, if the JSON is not a parsable user 
// then return nil
func parseUser(json: JSON) -> User? {
     //parse json
}
// combine everything
let parsedUser: User? = userInput.map(parseJSON).flatMap(parseUser)

This seems like a small change but it really helps simplify your function signatures and prevents the proliferation of optionals and if let … checks. Whatsmore, there would be no point to optionals if all they did was replace if value != nil by if let ….

(Footnote 12: Lifting refers to taking an existing function and change it such that it changes its argument and its return type to something more general. In the case of optional, map transforms a function with a signature of T -> S to T? -> S? and flatmap transforms a function with signature of T -> S? to T? -> S?)

Error Handling

When dealing with throwable functions it often happens that there is nothing to do when the error occurs except abort what we were doing. Let’s reuse the parseJSON example. Imagine you want to read a json file and parse it as a User. But reading the file can throw:

// read the content of a file and put it in a String
func readFile(filepath: String) throws -> String { … }
// The function we want to write
// how should the possibility for errors expressed?
func readJSON(filepath: String) -> User /* error type? */ { … }

readJOSN will read a file and attempts to parse its content as a User but there should be a way to signal to the caller that this function can fail. Given this situation, what’s the most reasonable thing to do in case of error for readJSON? Probably either report the error to the caller, or ignore the error.
If we want to ignore it, here is the signature we are looking for:

func readJSON(filepath: String) -> User? { … }

This function combines readFile, parseJSON and parseUser and returns the user contained in the file. If anything goes wrong, the user is not returned and the function returns nil instead. Let’s see how we can implement it

func readJSON(filepath: String) -> User? {
    do {
        let content = try readFile(filepath: filepath)
        return parseJSON(content).flatMap(parseUser)
    } catch {
        return nil
    }
}

this implementation seems correct, we’ve handled all the possible error by simply converting them into a nil. But what a ceremony all that was! 4 lines out of 8 are dedicated to ignoring an error and returning nil instead. Here is a another way:

func readJSON(filepath: String) -> User? {
    return (try? readFile(filepath: filepath))
        .flatMap(parseJson)
        .flatMap(parseUser)
}

In this example we’ve used the try? keyword which does exactly what our previous implementation did: It will return nil if an error is encountered, otherwise it will return normally. flatMap allows us to combine our parseJSON and parseUser function in sequence while not worrying about the nil case.
Another nice effect of writing things like this is that it is easy to see what happens and in which order:

1. attempts to read a file
2. attempts to parse the file as JSON
3. attempts to parse the JSON as User

And the type signature communicates that “if anything goes wrong, this function returns nil”.

We’ve been able to make our program quite a bit simpler while keeping its relevant type information. But this type signature is the product of a choice we made. Indeed, we decided to remove any mention to the possible ways reading an file can fail and in doing so have hidden any way to diagnose the error. That might be what you want, but maybe you want to keep this information around in order to help the users of this function understand why a failure happened. Was is a file handle problem? or was is a parsing error? In this case you might want to update your function like this:

// This time we both throw and return an optional
func readJSON(filepath: String) throws -> User? {
    return try parseJSON(from: readFile(filepath: filepath))
        .flatMap(parseUser)
}

With this configuration the caller can infer that a nil result and a thrown error mean different things. Specifically, nil means that the parsing was unsuccessful, and error means that there was a problem with the file.

The possiblities here are infinite, we could make the parse functions throw and have the user catch all the possible parseJSON and parseUser errors, we could make use of a Result type, we could encapsulate all errors in a custom ReadJSONError type, etc. And all those variation keep our precious type information while communicating differently about what the code does.

Conclusion

Swift is not a total language, and will never be. Nonetheless,the Swift compiler gives us more confidence that a compiled program will behave nicely and encourages programmers to write program that are total by enforcing some very simple rules (catch errors, check for nil, make all switch statements exhaustive, etc.).
Unfortunately, Swift also has one escape hatch ! that is a little bit too easy to use and that throws away all efforts to make programs total. Maybe in the future there will be ways to selectively disable operators like ! in order to work in a safer environment and advertise a crash-free experience. Until then we can only rely on linter tools.

Finally, I can only encourage you to write safer code, disclose when you might crash and make use of the awesome type system. What’s truely amazing with what I’ve shown is that most of it is a product of the powerful type system. Swift does not have a special “nil checking” phase in the compiler. Optionals are juste like any other type, and you can make up precise types like those which communicate very important behaviours about your code.

This post has been inspired by the book Type Driven Developpement with Idris by Edin Brady which I recently finished. The book presents what it’s like to program in Idris, a pure, total, dependently typed programming language. I encourage anyone to take a look at Idris, there are lots of lessons to learn from it even if it is a completely different experience than using more mainstream programming languages.