Correct Behavior Through Type Safety

Swift has brought a much stronger type system to Cocoa development, which helps catch more bugs at compile-time, before they ship and affect real users. But it’s not enough to bring Objective-C patterns to Swift, sprinkle in a few types, and call it done. Justin Spahr-Summers, core contributor to Carthage, ReactiveCocoa & Mantle, explains how types can be used to ensure correctness, how to prevent the existence of invalid states, and why unit tests just aren’t enough. Along the way, he’ll dive into some specific approaches to correctness that will take advantage of Swift’s strong type system.

---

Introduction (0:00)

Today I want to talk about some of the great things you can do with the new and improved type system that we have in Swift, and what it brings to Cocoa development. For those of you who are used to the dynamic nature of Objective-C, the static type system of Swift might actually seem like kind of a setback, and more akin to languages like Java or C++. But I believe that Swift’s type system brings some much-needed safety to Cocoa development by helping us catch more bugs at compile time, before they actually ship to real-world users.

Specifically, static types allow us to prove the correctness about certain things in our programs, and prevent many kinds of invalid states from even occurring in the first place. I will demonstrate some of our techniques for preventing those kinds of errors, and show why testing alone is not good enough to prevent them either.

When I’m not doing Cocoa development, I like to explore functional programming languages like Haskell, Elm, and Idris. I’ve found that really helpful for learning new concepts and expanding my mind.

Types Prevent Errors (1:17)

What are types useful for? Why do we care about having type systems at all? As I mentioned, types help prevent errors before they ship, before they can happen at runtime. But they do this by restricting what you can do. In their restrictions, they actually help prevent certain invalid cases. For example, NSArray is more restricted than NSMutableArray. There are fewer things that you can do with an NSArray than NSMutableArray. It doesn’t matter if it’s actually mutable under the hood. If you have a variable of type NSArray, then there is a limited set of things you can do.

That restriction helps prevent errors, because mutation introduces a whole new category of things you can do and possible error states that you can encounter, like race conditions or inconsistent updates. By restricting the interface to just immutable types, you can prevent some errors that would be possible with the larger mutable variant.

Swift’s optional type Optional<T> is another great example of this. By restricting how you can use this value, or how you can access the value inside the optional, it can prevent certain errors like accidentally using nil where you don’t expect it. And, it doesn’t actually prevent you from doing anything new. In restricting and making you check for nil, it’s making you think about certain kinds of errors that would otherwise occur.

Arrays in Swift are another good example. They restrict the things you can insert to the type that the array is parameterized over. By restricting the type in this way, they prevent you from using the wrong object and crashing. By forcing the reader and the writer of this array to agree on the type, we can prevent errors.

Types = Proofs (3:14)

The more general extrapolation of this idea is known as the Curry–Howard correspondence. The informal way to say this is that types are equivalent to logical proofs. Any well-typed program can be represented as a logical proof, and vice versa. What this means practically is that each function must prove its correctness to the compiler. In doing so, there are some other corollaries that can come out of that. Your program has to type check, or the proof has to be internally consistent.

Examples (3:42)

Let’s go through some examples. This is more abstract, but in order for a function from type A to type B to compile, you have to prove to the compiler that such a transformation is actually valid. This proof consists of writing a well-typed function definition. Here’s one proof for this proposition. This is a function from Double to Int, and the integer result proves that we don’t have a fractional component anymore. Just by nature of having an integer, you’ve proved that you don’t have any decimal point.

func toInteger(num: Double) -> Int {
	let result = round(num)
	return Int(result)
}

There are a few valid implementations for this type signature, but in all cases, executing this function proves to the compiler that you now have an integer value. If you were to compare this with a language like Ruby or something else without any static types at all, the result doesn’t actually prove anything. You would hope that this function is giving you an integer, but there’s really no guarantee because it’s not encoded anywhere. By contrast, the amount that we can prove with a function like this is not a whole lot.

In a function from String to String, you still have to prove that you have a string result, but there are many ways to implement this function that may be incorrect or may not do anything at all. For example, here’s a perfectly valid implementation of a function of this type that neither proves anything nor gives much useful information.

func identity(s: String) -> String {
	return s
}

Use Types to Prove Correctness (5:10)

What I’m trying to get at here is that we can use types to prove correctness, because types are just proofs. They help us prove certain properties about our program. If you have an instance of a given type after executing some function, that proves that you have performed some logically-valid transformation to obtain it. So if you have an integer, that proves that you did something to either reduce down a double, or parse a string. You can now prove that you have an integral value.

If you have a variable of type NSData, what can you say about it? You basically can’t say anything, except that it has bytes of a certain length. It doesn’t tell you anything about the contents of that data. Still, at least it’s slightly better than a variable type id or AnyObject in Swift, which tells you even less.

On the other hand, a value of type NSString, or string in Swift, proves that you now have characters and not just bytes. That’s one level upward, and it means you’ve validated this as a unicode string. We’ve proven a bit more. You can go even further, with an NSURL proving that you have parsed a string into a URL. It’s no longer a string or a bucket of bytes, but something more.

These concepts extend to any kind of validation. JSON parsing is really just a glorified validation of the type system. It means that you’ve validated this raw string into some collection of objects, like dictionaries or arrays, and then validated those further into model objects that you understand. In parsing JSON, you’re proving that you now have objects from your model layer.

What about Tests? (6:57)

Why we can’t prove these things with tests instead of types? Tests can certainly help improve correctness, and I’m certainly not advising anyone to stop writing tests. But, they’re not a complete replacement for powerful types. In science, hypotheses can never be proven. They can only be supported by the available evidence, or disproven if the evidence is contradictory. But you can never prove a positive statement - if you have a hypothesis, you can’t prove it.

Tests have a similar issue. Fundamentally, a passing test is just one piece of evidence that your behavior is correct. Although a test can disprove the correctness by failing, it can never actually prove it by succeeding. It’s just supporting evidence. On the other hand, types actually are proofs by what I mentioned before, the Curry–Howard correspondence. Whatever assertions you have encoded into your program’s types, those will be proven or disproven at compile time by the type checker. If you’ve compiled and passed type-checking, that means that you have proof of a valid program, insofar as you have encoded things in your type system correctly.

Caveats (8:22)

Types are not without its limitations. There are certain things that you can’t do with types that you can do with tests. The types in your program can contain errors as well. It’s significantly less likely, but it’s still possible, just like making an error if you’re doing a logical proof in math class. The compiler can catch accidental mistakes fairly well, but it can’t help you fix an incorrect, but nonetheless, valid or compilable classification.

Types also can’t represent everything. Side effects are an especially nefarious example of this. It’s impossible to tell just from the types whether invoking one function multiple times will give you the same result. There’s no way to encode that in Swift. In some languages there is, but not in Swift. Tests are better for verifying that sort of thing.

Finally, tests might be just good enough for your use case, whatever it happens to be. For example, it might be easier to test that network requests hit the cache than it is to guarantee that property in the type system. Using tests is sometimes better than, or easier to accomplish things with, than by encoding this information in the types.

Phantom Types (9:36)

There is even more you can do with types that you might not have expected. I hope we can agree that generics on arrays are overall a good thing that help prevent errors. But there are some more advanced techniques that can really take it to the next level. One example that I really like is phantom types, from objc.io’s Functional Snippet #13.

In this example, we have a FileHandle struct that is parameterized over type A. We call type A a phantom type because it’s never actually used in the implementation of that structure. In the entire structure’s definition, you can see that A is never used. But even though it’s never referenced in that implementation, we can still use it for type-checking. We have Read and Write enums, and when we use these in a function type signature, we can guarantee at compile time that, for example, we have a FileHandle for reading.

struct FileHandle<A> {
	let handle: NSFileHandle
}

enum Read {}
enum Write {}

func openForReading(path: String) -> FileHandle<Read>
func openForWriting(path: String) -> FileHandle<Write>
func readDataToEndOfFile(handle: FileHandle<Read>) -> NSData

Simply by returning a FileHandle for reading, we have to pass it to all the other functions that use that same type. We can’t just throw out the read and try to replace it with the write. So, it can only be passed to functions that match that type.

Case Study: Errors in ReactiveCocoa (10:58)

Here is a more in-depth example that might demonstrate another use for types. This example comes from the library ReactiveCocoa, which is for functional reactive programming in Swift and Objective-C. It uses streams of events known as signals.

Signals (11:18)

I’ll give you a really really quick breakdown of signals. In ReactiveCocoa, signals must obey these semantics. You can send any number of next events, which are events that carry a value. Optionally, you can terminate it with an error or with a successful completion. In Objective-C, RACSignal * is the type of a signal, which tells us absolutely nothing about how those events are going to proceed. We don’t know what’s going to come in the next events, and we don’t know if it’s going to error or complete.

Property Binding in RAC 2 (12:07)

In this example, this is how you would bind to a property in ReactiveCocoa 2.0, Objective-C API. we’re just saying that whenever the model changes, we want to fetch an image from the network and then bind that to our UIImageView. Unfortunately, this example isn’t safe if this fetchImage signal sends an error. Suddenly the error reaches this property binding, and ReactiveCocoa will throw an assertion, or throw an exception.

RAC(self.imageView, image) = [RACObserve(self, model)
	flattenMap:^ RACSignal * (Model *model) {
		return [model fetchImage];
	}];

//  Received error from RACSignal in binding for key
// 	path "image" on UIImageView:
//  Error Domain=NSURLErrorDomain Code=-1 "Operation
// 	could not be completed."

Because this error occurs at runtime, it’s hard to look at that original sample and know that it’s problematic. In testing, the image fetch may never fail, and so you could ship this bug to users and never really realize that this could be a potential problem. Now, you might argue that this is a problem with the ReactiveCocoa framework, but the framework can’t really know what the right answer for your particular program is. Ignoring the error could be dangerous. Meanwhile, terminating the program could also be incorrect, but the program really just has no way of knowing.

Solution: Types! (13:10)

Now that we can use Swift, this problem can be avoided by capturing more information in the type system. In ReactiveCocoa 3.0, this is the new signal type Signal<T, Error> which says that it will send values of type T, and may send an error of that type.

How does this help with the property binding stuff? Well, we introduced another thing as well called NoError. It’s very similar to the FileHandle example that I showed before. This type doesn’t have any constructors, so you can never actually create an instance of NoError. You could only refer to it in type signatures. But because you can never create it, if you use this in a signal’s type, you’re guaranteeing that that signal can never send that error. This is because it’s impossible to construct that error in the first place. So, here’s how it’s actually used.

func <~ <T> (property: MutableProperty<T>, signal: Signal<T, NoError>)
func <~ <T> (property: MutableProperty<T>, producer: SignalProducer<T, NoError>)

These are binding operators in ReactiveCocoa 3.0. These custom operators are doing the same thing that you saw before, and you can see that they expect a signal of type NoError. If we were to naively reimplement the Objective-C binding example in Swift, this is what it might look like at first glance.

class Model {
	func fetchImage() -> SignalProducer<UIImage, NSError>
}

self.imageProperty <~ self.modelProperty.producer
	// TYPE ERROR: NSError is incompatible with NoError
	|> flatMap(.Latest) { model in
		return model.fetchImage()
	}

We have our Model object, and this fetchImage method still exists. It returns a signal producer, and it will send us a UIImage or an NSError. This NSError might represent something like the network request failing or an NSURL connection failure. We bind our image property to the results of fetching the latest image.

However, instead of asserting at runtime, like the Objective-C version, this will actually fail at compile time with a type error. Because fetchImage returns a producer which may send NSError, it’s incompatible with the property binding operator that expects NoError. We can now statically say that this is invalid, that there’s an error which might go unhandled here. We can prevent that at compile time, and force the user to think about what their error-handling behavior should be.

Here’s an example of that choice. We are choosing to ignore errors. But in the same way that optionals make you think about nil, this makes users think about the error handling. So even though errors are ignored, it’s now a very explicit decision that I’ve made and not just something that happens implicitly. Just like that, we’ve added additional safety to these APIs by including more information in the type system. This is something that you can’t catch with tests, but something that powerful types can help prove or disprove.

class Model {
	func fetchImage() -> SignalProducer<UIImage, NSError>
}

self.imageProperty <~ self.modelProperty.producer
	|> flatMap(.Latest) { model in
		return model.fetchImage()
			// Ignore any error event
			|> catch { error in .empty }
	}

Typed Errors vs. Throws (15:58)

If you’ve been following along with WWDC, you might know that Swift 2.0 introduces exceptions or error handling. Although it’s great to finally have first class error handling in the language, I think it’s still limiting. The main problem here is that Swift doesn’t provide any of this type information with its exceptions. Everything is just an error type protocol. Consequently, we have no way to prove or disprove what kinds of errors some code might sign.

If you have a closure that says it’s going to throw something, you don’t know anything about what it’s going to throw. It could throw absolutely anything. You then either have to handle absolutely everything, or let some things go unhandled without you knowing. With Swift’s built-in error handling, ReactiveCocoa would be back at the same problem we had in Objective-C, where there’s really no way to know if an error could or could not occur in property binding. That’s why RAC has its parameterized error type, and that’s why I believe that Swift should add more type information with theirs.

Types Can Also Describe Effects (17:07)

In addition to adding safety to some operations like this, types can also describe certain forms of “un-saftey”, dangerous things like side effects. The canonical example Haskell’s IO monad, which means that you have side effects. You can put a value into this IO bo, perform side effects using it, and transform that value in any number of ways. But the interesting bit is that you can never get it back out. So if you see IO, you have a strong suggestion that there are side effects there. If you don’t see IO, that’s even better, because you have proof that there are no side effects.

This is again very similar to Swift’s optional type, which suggests that a value may not exist. If you see optional, that’s a hint that the value might not be present. On the other hand, if you don’t see an optional, you have proof that the value does exist. Unlike Objective-C, where you’re really not sure anywhere in the program, Swift lets you prove whether a value is there.

To go back to ReactiveCocoa for a really quick second, many of the benefits of the IO type also apply to signals and signal producers. You can put values into a signal, you can perform time-based operations, or time-based side effects with it, and you can apply transformations. Just like IO, it’s difficult to get the values back out, because tagging a value with a signal or signal producer saying that it is one of those things indicates that there’s now a time or side effect element. You have to do something to explicitly acknowledge that.

Example: Types for Concurrency (19:18)

I’d like to finish with one last example, using types to describe concurrency. How many times have you done something like this? This is a really contrived example, obviously, but if you’ve written complex code where this sort of thing happens, I’m sure there have been times where you called some UIKit or AppKit code on a background thread.

dispatch_async(someBackgroundQueue) {
	// Oops!
	self.textField.text = "foobar"
}

What if we had some way to prevent this problem from ever occurring, statically, at compile time? I’ve come up with a type called UIAction, which will represent the action that needs to be performed on the main thread. We can instantiate it with any kind of block, and that block will represent our UI work.

struct UIAction<T> {
	init(_ action: () -> T)

	func enqueue()
	func enqueue(handler: T -> ())

	func map<U>(f: T -> U) -> UIAction<U>
	func flatMap<U>(f: T -> UIAction<U>) -> UIAction<U>
}

We can transform that with map and flatMap so that it stays within this type. Eventually, the only way to actually get it to run is this enqueue method, which forces it to run on the main thread. Once you see UIAction, you know that this is going to be run on the main thread. We have guaranteed statically that it can only be run on the main thread, and there is no other way to do it.

Hypothetically, we could use this in some UIKit extensions, like on UITextField. Again, this allows you to guarantee that the text is set on the main thread and not in the background. Even if you call this method on the background thread, you still get back an action that guarantees it’ll run on the main thread.

extension UITextField {
	/// Sets the receiver's text to the given string
	/// when the returned action is executed.
	func jss_setText(text: String) -> UIAction<()>
}

This is just an example, and isn’t production-ready. But imagine if all of AppKit or UIKit were written this way officially - it would become impossible to accidentally use them on a background thread. More powerful types can prevent all kinds of errors.

Slides for this talk may also be found on Justin’s GitHub.