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

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

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

  • 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 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

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

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

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

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

// 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

func openFile(path: String) throws -> FileHandlefunc 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 “!”

Optionals

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

// 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

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.

iOS developer, functional enthusiast, gamer.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store