Machine-checked explicit state: An arrow in the heart of complex web apps

by Michael Bernstein on June 21, 2017

And how the Elm Architecture implements it

The most interesting work in front-end programming in the last few years has been aimed at solving the problems that arise when programs with a lot of UI and state reach a level of complexity where making reasonable changes is challenging and time prohibitive. The Elm programming language and its associated “Elm architecture” takes an extremely compelling and encouraging approach to solving this problem.

In this essay I’ll describe what “Machine-checked explicit state” means and discuss why I think Elm’s implementation of this idea is a step in the right direction toward finally conquering the beast that is stateful UI programming.

What is machine-checked explicit state?

It’s a bit of a mouthful, and it’s really just two-ish ideas smooshed together. Let’s start at the beginning:

State in this context is anything that needs to change in order to make stuff happen inside your application. Here’s an illustration of two states of a web application, with a few obvious changes taking place between the two:

Like the old kid’s game : What has changed?

Like the old kid’s game : What has changed?

On the left, we have three “pieces” of state — a red star, a green pentagon, and a blue triangle. These are purposefully abstract, but they could represent anything: some numbers your users care about, chat messages, etc. On the right, we have three pieces of state as well, with some obvious changes made to two of them: some numbers got incremented, or chat messages got edited, or time just went by. What made the application transition from one state to another? Usually, it’s some kind of external input — maybe time, a user’s click, form input, etc. In other words, state is the stuff that changes.

Explicit state is state that has to be entered into a bookkeeping system of sorts in order to be of any use to the application. In the Elm architecture, State has to be represented in code, in a very specific way, for it to be available in your application to your users. More about that below. What explicit **adds to the equation here can be defined easily by what it excludes: **state that is implicit. This is the stuff that accretes over time and makes applications challenging to change. With Elm, there’s no place to “hide” state in your application that aren’t threaded through the type checker. No more wild goose chases to see how you ended up where you ended up. If you want to know how a change to state anywhere was made, you should now know exactly where to look. As an aside,* *Elm’s debugging system, which hooks into this state, is one fabulous example of the what all state being explicit enables.

Finally,** machine-checked *means that your homework is handled for you by the bookkeeping system mentioned earlier. We call this bookkeeper the *type checker. Elm’s type checker acts as our assistant, making sure that changes that we expect to be propagated throughout our application are properly accounted for. If you want to add state to an Elm program, you (roughly) have to:

  • Add your piece of state to a Model

  • Craft a message that can change this specific state with your Update function

  • Expose the state visually in your View

This might seem like a lot. Does this mean that you have to update things in three different places in your Elm program in order to make even simple changes to how state changes? Yes, typically you do. Does the compiler let you forget that last one you forgot because, like me, you’re human? No, it does not! So machine-checked means that you pay up front for the guarantee later on of being reminded when you need to be about things that are important. Here’s a visualization:

Hmm..what’s missing?Hmm..what’s missing?

In my Elm program, if I make a change to my model, and then go ahead and try to represent that in my view, but do not appropriately bookkeep for the type of message that will make the changes visible in my view, the type checker will stop me. It will tell me that I haven’t created the necessary message in the necessary place in order to implement this change. It won’t compile a usable .js file for my project, and I’ll need to stop, slow down, and check it out. While this may seem trivial (it’s just fancy bookkeeping after all), constantly having this mechanical ally to rely on makes the act of stateful web programming considerably easier and more consistent.

The Elm Architecture: How it fits in

Here’s the bare-minimum representation of the Elm architecture as it is shown in the Elm documentation:


type alias Model = { ... }


type Msg = Reset | ...

update : Msg -> Model -> Model
update msg model =
  case msg of
    Reset -> ...


view : Model -> Html Msg
view model =

Here’s one way to read it:

  • The model is a data structure that describes the state of your application

  • To change your state, you can use the update function, which takes a message and a model and returns a model

  • The view of your application is a function which takes your model and returns HTML

I’m typing this out here, below the explanation above, so that the bones of the architecture can sink in. You can see here that there is nowhere to “shove” phantom state that isn’t under the control of the bookkeeper or type checker.

It’s my contention that this creeping, implicit state is at the heart of the complexity of many front-end applications, and the Elm architecture hobbles this complexity by demanding that all state be explicit and machine-checked.

Why this matters

The underlying “platform” of the web, with everything from audio to video to networking to extremely fast performance in general, has up until this point lacked a mature architecture to allow developers to cleanly map user interactions to changes in underlying data models.

While people have undoubtedly created amazing applications with this platform, there is still a lot of room for a framework that describes precisely how the creeping complexity of state + UI can be tamed. It’s my opinion that the Elm architecture, while far from perfect, is the most encouraging and exciting step in this direction, and that has everything to do with the advantages of machine-check explicit state as they are described here.

Does this sound awesome? It is! The Elm community is very welcoming — give the language a chance!

Special thanks to Luke Westby for reviewing this article.