Cases where exhaustive pattern matching got in the way?

Request Feedback
1

Hi all,

I’m currently doing a research project on pattern matching and exhaustiveness checking. Elm has mandatory exhaustive pattern matching i.e. your code won’t compile if a “case” expression is missing a branch.

I’m wondering if people could share experiences with cases where this got in the way: code you’ve written where you needed to use Debug.crash to cover a branch that you knew was unreachable, but the compiler didn’t.

Thanks!

2 Likes
2

Well if you need to do that your problem is likely the type your matching on.

The only way of getting in the way I can think of, would be if your matching for _ and extend your type. In that case the compiler can’t help you and it will just work. So you need to find each usage manually.

1 Like
3

I started doing a chessboard at one point, which I modelled internally as an array, but had public API so you could interact with it via normal chess positions ala “A,2”. Converting from my custom types to an array index was fine, but converting the other way required an exhaustive check, even though getting into that state should not logically be able to happen. Now I’m just assigning a default value, but I could only ever hit that case if my business logic was screwed beyond making a reasonable recovery, so a default value really scares me more than just outright crashing the program.

Until the language can reason about integer sizes though, it’ll have to do at least. :slight_smile:

4

Just a quick side node:
I’m currently working on a master thesis with the goal of creating a type checker for Elm that introduces bounded integer types. I estimate to be done next year, lets see, though it would probably not help you with that exact code. It will not change the way exhaustive pattern matching works, but it will help making impossible states impossible.

It would look like this:

convert : Int -> Int7
convert = clamp 0 7
2 Likes
5

Not so much an unreachable branch but I frequently catch and ignore illegal states with pattern matching. What I often do is to model a UI as a state machine, and pattern match on a combination of the current state and the current event. Here is a contrived example:

type State
 = Initial
  | DataLoaded

type Msg
 = HttpRequestComplete
 | PressedCancel

type alias Model
 = State

update msg model = 
    case (model, msg) of
        (Initial, HttpRequestComplete) -> (DataLoaded, Cmd.none)
        (Initial, PressedCancel) -> (Initial, Cmd.none)
        _ -> (model, Cmd.none)

In this example, an HTTP request is made but the user is also shown a dialog with the option to cancel the data load operation. The completion of the network call or the user pressing the cancel button are in a race that may change the state of the application. In this case if the data loads the application goes to the DataLoaded state, but if the user also pressed the cancel button very close to when this happened, its event may have been placed on the event queue. So I want to guard against processing the PressedCancel event when in the DataLoaded state.

Exhaustive pattern matching needs to cover all states, and I solve that by simply ignoring illegal state + event combinations.

1 Like
6

One thing where this happens is when working with indices into an array derived from some input list. When we Array.get things out of the array the code “knows” that the array index must be in bounds, and in my case whenever I was doing it, the code was generic over the contents of the input. So no luck returning a bogus “default” value.

So the options were:

  1. Return a maybe type even though we know the code will never return a Nothing.
  2. Induce a crash in the branch via infinite recursion.

Neither option is really that great.

7

Hi Joey,

At the time that Elm 0.19 came out, I did a review of all Elm 0.18 packages to check for this (uses of Debug.crash in a place where it seems like incomplete matching was potentially valuable and/or unavoidable).

Here’s the summary of what I found along with links to each relevant package’s relevant code: https://gist.github.com/avh4/ec82d9b41fc385a4cbfb8bb73e6d5abb

3 Likes
8

I am wondering if you will run into the classical problem of sub-typing breaking type inference with this direction of research?

For example, a bounded integer between 1…10 should be able to be used wherever a bounded integer between 1…100 could be used. So there is a sub-typing relationship between bounded integers. When inferring types this will likely be problematic.

9

That will not be the problem. I’m actually implementing refinement types (quite similar to how Liquid Haskell does it) so I would have a type {a | 1 < a && a < 10} and a type {a | 1 < a && a < 100} and then I’ll prove that _1 < a && a < 10 => 1 < a && a < 100 (that’s something that the computer can prove for me).

What will break my system is something like {(a,b) | a * b == a + b}. Right now there does not exist a general way of proving statements containing multiplication. But Bounded integer types should work great.

But let’s not get off-topic. I’ll create my own thread as soon as I’ve got something to show.

10

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.