Matt Diephouse

Eliminating Impossible States with Never

18 July 2018

Swift has a very useful type called Never in the standard library. It’s defined very simply:

public enum Never {}

That might seem strange. What kind of enum has no cases?

This is an example of an uninhabited type—a type that doesn’t have any valid values. There’s no way to create a Never value. That’s a useful property for proving things in the type system. Uninhabited types let us make things impossible.

When it was introduced in SE-0102, Never was framed as a useful return value for functions. Before then, Swift functions that never returned, like fatalError, were marked with a @noreturn attribute. By declaring fatalError to return Never instead, you’ve proven that it never returns. Since there’s no way to create a Never, there’s no way to return one—so you’ve proven that the function can never return.

public func fatalError(
  _ message: @autoclosure () -> String = String(),
  file: StaticString = #file, line: UInt = #line
) -> Never {
  …
}

This isn’t the only place that uninhabited types like Never are useful.

Types help us by restricting the number of possible values. The clearest example of this may be the Result type:

enum Result<Value, Error> {
  case success(Value)
  case failure(Error)
}

Without Result, asynchronous, failable APIs look like this:

func run(completion: @escaping (Value?, Error?) -> ()) { … }

This API is susceptible to bugs because two impossible states can be represented by the types. There should never be (1) both a value and an error or (2) neither a value nor an error. But since it’s possible to represent those in the types, the run function and its caller can both make that mistake.

run { value, error in
    switch (value, error) {
    case let (value?, nil):
        handleSuccess(value)
    case let (nil, error?):
        handleError(error)
    case (_?, _?):
        fatalError("Can't have both a value and an error")
    case (nil, nil):
        fatalError("Can't have neither a value nor an error")
    }
}

Result eliminates those impossible states. By making the impossible states impossible, potential bugs are eliminated.

run { result in
  // With `Result`, no `fatalError`s are necessary.
  // We've made those impossible states impossible.
  switch result {
  case let .success(value):
    handleSuccess(value)
  case let .failure(error):
    handleError(error)
  }
}

Uninhabited types let us go a step further. We can mark cases of an enum as impossible, essentially erasing them from the type:

// This can't fail because you can't create a `Never` to use
// for a `.failure`
// This is basically equivalent to declaring `value` as an `Int`
let value: Result<Int, Never> = …

switch value {
  case let .success(value):
    …
  // A failure case isn't required because it's impossible
  // This is actual working Swift code
}

// This always fails because you can't create a `Never` to use
// for a `.success`
// This is basically equivalent to declaring `error` as an `Error`
let error: Result<Never, Error> = …

switch error {
  // A success case isn't required because it's impossible
  case let .failure(error):
    …
}

That doesn’t make much sense if you’re just declaring local variables with Result: you could just declare your Int or Error directly. But it becomes important once you start using associatedtypes, generics, or a type that adds effects (e.g. an FRP observable).

Take this Elm-inspired description of a UI, e.g.:

// Something approximating The Elm Architecture
// `View`s have `Message`s that can be sent back to the `Component`
protocol Component {
  associatedtype Message
  mutating func update(_: Message) -> Command?
  nonmutating func render() -> View<Message>
}

// You can create a `Button<String>`,
// but you can't create a `Button<Never>`
// because you couldn't set its action
struct Button<Message> {
  var action: Message
  var title: String
}

// You can create a `View<String>.button`,
// but you can't create a `View<Never>.button`
// because you can't create a `Button<Never>`
enum View<Message> {
  case button(Button<Message>)
  case text(String)
}

Using Never, we can prove that some views aren’t interactive, i.e. that they contain no buttons. A View<Never> can’t contain a Button, or any other type of view with an action, because those views can’t be created. That means we can restrict portions of our view hierarchy to non-interactive views.

Let’s say, for instance, that we’ve created a document viewer. We want to render documents to views, but those views should always be static—users shouldn’t be allowed to create buttons. We can enforce that by rendering documents to a View<Never>:

// Our spec says that documents should never contain interactive
// elements. Returning `View<Never>` here proves this in the type
// system. It's impossible to accidentally return a `Button` now.
func render(_ document: Document) -> View<Never> { … }

We may also want to export documents to HTML. We decide that writing a second renderer would be difficult, but it’s not so bad to convert each View to an HTML type. Ordinarily, you might write this generically over the message type:

func export<Message>(_ view: View<Message>) -> HTML {
  switch view {
  case .button:
    // `fatalError`, like `!`, means you haven't
    // proven something in the type system
    fatalError("Documents can’t contain buttons.")
  case let .text(text):
    return HTML.text(text)
  }
}

Unfortunately, while we know that we’re exporting documents and that documents never contain buttons, we haven’t proven that, so the compiler doesn’t know. We have an impossible state that can be represented in the types, so we have to resort to fatalError.

We can prove that we’ll never try to export a button by using Never again:

func export(_ view: View<Never>) -> HTML {
  switch view {
  case let .text(text):
    return HTML.text(text)
  }
}

By using Never, we can completely get rid of the case .button! The Swift compiler knows that you can never create a View<Never>.button, so you’re not required to include that case in your switch. Now someone can’t accidentally call export on an interactive view.

One problem remains: we’ll want to use our rendered document, a View<Never>, inside a View<Message>. This can be done by using another switch statement like the one above above:

extension View where Message == Never {
  func promote<M>(to _: M.self) -> View<M> {
    switch self {
    case let .text(text)
      return .text(text)
    }
  }
}

We only need to unwrap and rewrap our elements to be in the right View type. And we don’t need to include a case button.

Now we can fully render our UI:

func render(_ document: Document) -> View<Never> { … }

extension View where Message == Never {
  func promote<M>(to _: M.self) -> View<M> { … }
}

func render(_ state: State) -> View<Message> {
  return View.stack([
    render(state.document).promote(to: Message.self),
    .button("Export", Message.export),
  ])
}

Never let us eliminate impossible states:

  1. render(_: Document) can’t return interactive elements.
  2. export(_: View<Never>) doesn’t need to handle interactive documents.
  3. You can’t accidentally call export with an interactive view

This same approach can also be used with a protocol’s associatedtype—fulfilling the protocol, but eliminating impossibilities within specific types that conform to it.

Types are useful because they restrict possible values. Never can help us by eliminating some of those values, restricting the possible values even further. Proving that they’re impossible in the type system gives us confidence in the code that we write.