What do Haskellers have against exhaustiveness?

One of my favorite features of the Hindley-Milner type system is the built-in exhaustiveness checking that is applied to pattern matches. I like this feature enough that it is the focus of the only worked-out example I give in my talk about OCaml at Jane Street.

Why is exhaustivenss checking so important? You can slog through my talk if you want to hear a fuller account, but the basic point is that case analysis is one of the most common things one does in any program, and anything that can statically check important properties of your case analysis is really helpful. Moreover, exhaustiveness checking serves as a kind of refactoring tool. Whenever you expand the possibilities in a type, the compiler will point you to the places where you forgot to handle the new cases you just created. It is, from the perspective of someone who has programmed in ML for a living for some years now, an enormously useful feature.

So I was quite taken aback when one of our interns here (who will remain nameless, in case I've horribly misconstrued his words) pointed out to me that Haskell by default doesn't even warn the programmer about inexhaustive pattern-matches. In particular, if you save the following code into a file called 'foo.hs':

foo (Just x) = x + 1
main = print (foo Nothing)

and the compile it, the compiler won't make a peep. But when you run it, you will of course get a runtime error:

bash-3.2$ ghc -o haskell-foo foo.hs
bash-3.2$ ./haskell-foo 
haskell-foo: foo.hs:1:0-19: Non-exhaustive patterns in function foo

If you try something similar in OCaml:

let foo (Some x) = x + 1
let () = Printf.printf "%d\n" (foo None)

you'll get an earful from the compiler when you try to build it:

bash-3.2$ ocamlc -o ocaml-foo foo.ml
File "foo.ml", line 1, characters 8-24:
Warning P: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
None

We go even farther at Jane Street, where we use compiler flags to turn that warning into an error, so that the code can't build when the match is incomplete. When people want an incomplete match, they need to do it explicitly by adding a catch-all case, and to throw an explicit exception, as follows:

let foo = function Some x -> x + 1 | None -> failwith "Argh!"
let () = Printf.printf "%d\n" (foo None)

It is worth noting that all is not wine and roses in the ML world. Many, maybe most, ML programmers basically ignore the compiler's warnings about inexhaustive matches, which makes the warning the compiler does give you kind of useless. Still, the lack of even an admonition from ghc surprises me.

Presumably Haskell programmers are just as concerned with getting static guarantees as ML programmers are. So I'm wondering why the difference in the default compiler behavior. I'd be interested in hearing from any Haskell programmers who can explain what's going on.

Comments

Warnings

I do like to turn on warnings like -fwarn-incomplete-patterns and -fwarn-name-shadowing in ghci. According to the manual, -fwarn-incomplete-patterns "isn't enabled by default because it can be a bit noisy, and it doesn't always indicate a bug in the program. However, it's generally considered good practice to cover all the cases in your functions."

Using -Wall with GHC

I regularly code in C, C++, Ocaml and Haskell. Before picking up Ocaml and Haskell I was a keen advocate of gcc's -Wall compiler option which turns on all warnings. For my onw code, I often use -Wextra which turns on still more warnings and -Werror which turns warnings into errors.

When I picked up Ocaml about 5 years ago, I was hit by the missing pattern problem and started using the "-warn-error A" compile option to turn missing patterns into errors instead of just warnings.

It turns out the GHC also has -Wall and -Werror options and for my own code, I tend to use them both. With -Wall on your first example, ghc says:

a.hs:1:0:
    Warning: Pattern match(es) are non-exhaustive
             In the definition of `foo': Patterns not matched: Nothing

The -Wall option also screams when there is no function signature on a function which I also find very useful.

Use the -Wall flag

At Galois, and across the community, people are required to use -Wall to enable exahustiveness checking. So much so it should really be the default.

In addition, other tools for checking totality are popular, such as Neil Mitchell's 'catch' tool, for checking functions the user knows to be total, but which appear partial.

It's some quirk of history that ghc -Wall is the expected practice, but you have to specify it (my guess: it used to be too strict). I think GHC HQ will accept patches.

-Wall and -Werror

That makes a lot of sense -- history often leads one to pick the wrong default, and such decisions can take a while to unwind.

I'm curious whether at Galois you've tried turning warnings for inexhaustive matches (and other such tests) into errors. My ideal is to have such issues come up as errors, so long as there is a not-too-painful way of turning the error off by explicitly marking the situation in the code. For example, we turn OCaml's unused-variables warning into an error, but one can make the error go away by prefixing the variable in question with an underscore. This forces the code to be explicit about its intent, which, if nothing else, allows the decision to be reconsidered during the code review process.

-Wall -Werror

Yes, the use of -Wall -Werror is pretty common (all warnings have to be cleaned up before a succesful build). This also means top level type signatures, shadowing, and unused variables (which you can turn off with a leading underscore).

See also...

This thread on glasgow-haskell-users discussing the issues:

http://thread.gmane.org/gmane.comp.lang.haskell.glasgow.user/16926

Fascinating

An interesting and somewhat surprising discussion.

The first surprising bit is the idea that GHC's built-in exhaustiveness checker is not quite ready to be put in front of users by default. Some of the issues sound like fairly shallow issues (which is not to say they're easy to fix), like errors referring to a de-sugared representation rather than the written code. But there was also some indications given that proper exhaustiveness checking in Haskell is undecidable. Is that really right? Are they talking about something considerably more precise than the exhaustiveness checking in OCaml?

I was also surprised by the number of people who seem to think that exhaustiveness checking is basically not that big of a deal. Neil Mitchell argued that he found exhaustiveness checking "not worth it for personal code". Maybe I've been spending to much time writing correctness-critical code, but this strikes me as deeply counter-intuitive. Even for small projects, I find exhaustiveness checking a valuable finder of bugs, and a valuable refactoring tool.

Proper exhaustiveness

> proper exhaustiveness checking in Haskell is undecidable .. talking about something considerably more precise

Yes, they mean in the more precise sense (i.e. things that locally look partial, but are actually total because of invariants in other parts of the program). (Try regular exhaustiveness checking in GHC -Wall, it does as you expect for missing cases in sum types, etc).

catch-all case

Hi,

I'm curious about your phrase "catch-all" case. I've often taken that to mean using an underscore to handle unimplemented cases:

let foo = function Some x -> x + 1 | _ -> failwith "Argh!"

The problem with this is that one of the things you like the type checker to do is inform you where you need to add a branch when additional constructors are added to a datatype. For instance, if we changed the option type to

type 'a option = Some of 'a | None | Extra

than the code you wrote above will (correctly, in my view) give a non-exhaustive warning for foo, but the underscore will not. Which of these do you enforce at Jane Street?

  • Sean

catch-all case

You're right: catch-all cases are problematic, and you normally don't want them. I was just suggesting the catch-all case as preferable to leaving an inexhaustive match without any indication of that in the code, without any real structural change. Clearly, the best solution is to flesh out the case analysis, i.e.:

let foo = function Some x -> x + 1 | None -> failwith "Argh!"

There are some situations where catch-all cases are the right thing, but they are few and far between.

Syndicate content