Too Much Power Will Kill You (Every Time)

Posted on April 3, 2021 by Marko Dimjašević

You are a programmer and one of the greatest struggles you face every day is confronting yourself from yesterday. You have to deal with your reflection from the past, when everything made perfect sense, but today not so much anymore. An abstraction developed seemed like a perfect fit for the problem at hand, doing exactly what was needed, but perhaps without realizing it is doing much more than this. It was tempting to use this power and at the time it appeared justified. Today there is a bug,

"And you won't understand why
You'd give your life
You'd sell your soul
But here it comes again,
Too much power will kill you every time."

For a while I used to be an imperative programmer. In the imperative programming world, type systems do not play that important role. As a consequence, if one attempts to understand what a function taking a unit value and returning a unit value does just by looking at its type signature, they might not get far. Sure, it is an identity function, but it is allowed to do all kinds of side effects too. In the imperative programming world, this function can print to the console, delete records in a database, fetch data over the network, and it can do anything else that comes to your mind. The only chance of understanding what such a function really does is to read it completely, and recursively do the same for every function it calls.

For three years now I have been a functional programmer in Haskell. In a typed functional programming world with effects and function totality, type systems play an important role. As a consequence, if one attempts to understand what a function taking a unit value and returning a unit value does just by looking at its type signature, they can safely conclude it can only return a unit value and do nothing else. At first, that seems like a big reasoning win over the imperative programming world. However, in Haskell the IO monad is so pervasive that almost every effectful function is expressed directly or indirectly (via the MonadIO class) in the IO monad. In such a functional programming world, this function can print to the console, delete records in a database, fetch data over the network, and it can do anything else that comes to your mind. The only chance of understanding what such a function really does is to read it completely, and recursively do the same for every function it calls.

Put differently, the IO monad in Haskell is a glorified version of the identity monad from the imperative programming world. The IO monad is all too powerful in what it can do, thereby leaving us programmers powerless in knowing what it does and what it cannot do. Are not type systems in the functional programming world supposed to mend this mess of inability to reason via types? Do you feel like you were fooled into the typed functional programming world, only to realise you ended up in the same powerless situation that arose due to too powerful tools? What to do? Should one give up on typed functional programming because it has not delivered on the promise?

A solution is to use a type system (e.g., Haskell’s type system) more effectively, by using algebraic effects. It is true that every Haskell program has to eventually be run in the IO monad, but that doesn’t mean it should be written in the IO monad. Instead of writing it in the IO monad, a function can declare in its type signature what effects it allows. A caller function has to either handle these effects or declare them to be allowed in it too. That is to say, the meaning (the semantics) of an effect as provided by a handler is separate from the effect’s syntax (this is in contrast to functions that have their syntax and semantics coupled in the IO monad). Having a clear separation of effects and their handlers can also be looked at from a programming language perspective: an effect corresponds to the syntax of an embedded domain-specific language (eDSL), and its handler corresponds to an interpreter that provides a meaning to constructs in the embedded language.

To explore expressing a program via effects, I have been implementing a simple web game. Its core of starting a new game, updating a state and making a move has nothing to do with the IO monad, and it has everything to do with compositions of tiny orthogonal eDSLs. Each eDSL (effect) gives a way to abstractly express certain operations. It is their interpreters (handlers), be it in testing or in actually running the game, that provide semantics. To understand the extent of what a function can do to the world, it is enough to look at the function’s type signature and see what combination of eDSLs it is written in. For example, even though this is a web game, the core that provides an interface to the game’s logic is oblivious to anything web and therefore cannot return an erroneous HTTP response: it knows nothing about HTTP requests in the first place!

It might be of interest to highlight some technical implementation details. The game’s web server part is implemented in the Servant framework. It implements the Web Application Interface. A web API that the game implements comes with an automatically derived documentation from source code thanks to support from Servant, which means the documentation is always up-to-date. Effects are implemented via the Polysemy library and I have my own implementation of an atomic state monad to support updating the state in concurrent software. The code is structured in layers, where a layer has access only to functionality provided by itself or by lower-level layers. This allows for ease of testing and maintenance, and swapping a dependency library.

There is still a lot to be added to the game (e.g., a time effect and more tests for the web API), but the server is fully functional and can be used to play the game to completion. In case you are interested, its source code is available online.