Launching missiles with Haskell

Haskell advocates are fond of saying that a Haskell function cannot launch missiles without you knowing it. Pure functions have no side effects, so they can only do what they purport to do. In a language that does not enforce functional purity, calling a function could have arbitrary side effects, including launching missiles. But this cannot happen in Haskell.

The difference between pure functional languages and traditional imperative languages is not quite that simple in practice.

Programming with pure functions is conceptually easy but can be awkward in practice. You could just pass each function the state of the world before the call, and it returns the state of the world after the call. It’s unrealistic to pass a program’s entire state as an argument each time, so you’d like to pass just that state that you need to, and have a convenient way of doing so. You’d also like the compiler to verify that you’re only passing around a limited slice of the world. That’s where monads come in.

Suppose you want a function to compute square roots and log its calls. Your square root function would have to take two arguments: the number to find the root of, and the state of the log before the function call. It would also return two arguments: the square root, and the updated log. This is a pain, and it makes function composition difficult.

Monads provide a sort of side-band for passing state around, things like our function call log. You’re still passing around the log, but you can do it implicitly using monads. This makes it easier to call and compose two functions that do logging. It also lets the compiler check that you’re passing around a log but not arbitrary state. A function that updates a log, for example, can effect the state of the log, but it can’t do anything else. It can’t launch missiles.

Once monads get large and complicated, it’s hard to know what side effects they hide. Maybe they can launch missiles after all. You can only be sure by studying the source code. Now how do you know that calling a C function, for example, doesn’t launch missiles? You study the source code. In that sense Haskell and C aren’t entirely different.

The Haskell compiler does give you assurances that a C compiler does not. But ultimately you have to study source code to know what a function does and does not do.

Related post: Monads are hard because …

7 thoughts on “Launching missiles with Haskell

  1. I guess the main difference is that in C you *always* have to study the source code, while in Haskell you only have to do so if the function uses a large and complex monad (one that might have a “launch missile” button inside it).

  2. In the production Haskell codebases I’ve worked on, it’s always completely clear which monads any given function is in, and it’s standard to only give functions access to the monads that they actually need. Monad transformers make doing this pretty easy, so if your function only needs DB access you say so in the type, and don’t need to worry about it performing arbitrary IO. This is very far away from how things are in C.

  3. The primary function of a function should be described in what it cannot do.
    Thus no access to the ‘Red Button’

  4. Eric: The problem with underhanded C is primarily the “underhanded” part, then the C part.

    There’s no question that the Haskell compiler gives you information that the C compiler does not, automating part of the process of understanding what a piece of code does and does not do. But I think this has been exaggerated. Haskell code is not always as clear as it could be, nor is C always as opaque as it could be.

  5. If your code might launch missiles, it is probably the best to formally verify it – either with pen and paper, or with a language that can do this (Agda, Coq, Minlog, Isabelle, NuPRL, etc.).

Comments are closed.