Exhaustive case with monadic guard

Question

I have a case expression with a relatively large number of patterns:

case x of
  ... -> ...
  ... -> ...
  ... -> ...
  ... -> ...
  ...
  _ -> ...

One of these cases has a guard:

case x of
  ... -> ...
  ... -> ...
  ... | condition -> ...
    -- If condition is false, fall through to “Rest”.

  -- Rest:
  ... -> ...
  ... -> ...
  ...
  _ -> ...

If the guard doesn’t match, we just fall through to the remaining cases, no problem. But now I need to test the condition monadically, so I do:

case x of
  ... -> ...
  ... -> ...
  ... -> do
    condition <- action
    if condition
      then ...
      else ...  -- How to fall through?

  -- Rest:
  ... -> ...
  ... -> ...
  ...
  _ -> ...

However, I think I’ve made a misstep. There doesn’t seem to be a way of having the else branch proceed to the remaining cases without duplicating those branches or factoring them into a function. And either way messes with exhaustivity checking: if I want to add a case after the guard, the compiler doesn’t know whether the matches are exhaustive.

How can I change this function, or parameterise/wrap the datatype, to get exhaustiveness checking using a monadic guard?

I think you've confused yourself. You'll only enter the guard (or the `if-then-else`) if `Bar` matches. If `Bar` matched (and you reached the conditional), then you already know that `Baz`, `Quux` et al don't match, so there's no reason to continue with the `case` block. — Benjamin Hodgson, Jul 18 '16 at 18:01
@BenjaminHodgson: Good catch. Updated the example. I’m operating on a pair of values, and it’s still possible for later cases to match. — Jon Purdy, Jul 18 '16 at 18:06
No it's not. Can you just provide the **actual case** you are using instead of one with made up names that doesn't actually show what you are doing? — Bakuriu, Jul 18 '16 at 18:13
@Bakuriu: The real code is more complex, and I don’t know that it’s really relevant, but I can update the example in a moment. In reality I have a constructor `:@`, and my `Bar` case is really a match on `Ctor "Join" :@ a :@ b`, which comes before matching on the more generic case of `a :@ b`. — Jon Purdy, Jul 18 '16 at 18:24
@JonPurdy You don't have to post your real code, but you do need to post an *actual*, executable example that demonstrates the problem. — chepner, Jul 18 '16 at 18:26

Benjamin Hodgson · Answer 1 · 2016-07-18T21:24:24.990

3

One simple option would be to grab the second half of your case block and put it in a separate function.

case (x, y) of
  (Foo ..., Foo ...) -> ...
  x@(Bar ..., Bar ...) -> do
    condition <- action
    if condition
    then ...
    else rest x
  x -> rest x

rest (Baz ..., ...) = ...
rest (Var ..., ...) = ...
...
rest _ = undefined

It's a bit unsatisfying to use undefined in the fall-through case of rest to catch patterns which you believe should've been matched in the first half of the original case block. If you manage to violate the precondition (that (Foo, Foo) etc didn't match) then you'd get a runtime error.

edited Jul 18 '16 at 21:24

answered Jul 18 '16 at 18:14

Benjamin Hodgson

42,952
15
108
157

2

If the match in the fall-through is something relatively specific like `x :@ y` (as @JonPurdy seems to have implied in a comment), you could make `rest` a two argument function to avoid having a partial function. – David Young Jul 19 '16 at 00:19

chi · Answer 2 · 2016-07-18T18:38:33.470

I'm not a fan of the approach below, but I will share it anyway:

fix (\proceed b -> case (x, y, b) of
  (Foo ..., Foo ..., False) -> ...
  (Bar ..., Bar ..., False) -> do
    condition <- action
    if condition
      then ...
      else proceed True
  (Baz ..., ..., _) -> ...
  (Var ..., ..., _) -> ...
  ...
) False

The additional flag b is initially false, so all the branches are considered. Once we proceed, we set it to true so that the first branches are skipped.

May or may not be statically found exhaustive, depending on the actual patterns.

score 0 · Answer 3 · answered Apr 15 '18 at 06:05

What I ended up doing was using a monad stack equipped with Maybe and replacing the case with asum over a list of actions, following this structure:

asum

  [ do
    pattern1 <- pure input  -- failed pattern matches fall through
    body1

  , do
    pattern2 <- pure input
    body2

  , do
    pattern1 <- pure input
    guard condition         -- guards also fall through
    body3

  , ...

  ]

As I recently described in this answer to someone else’s question. Unfortunately, this doesn’t allow exhaustiveness checking.

score 0 · Answer 4 · answered Apr 15 '18 at 10:41

The obvious question is : can you not untangle the pure and impure bit ? Without the actual code is hard to tell but if only one condition is actually the problem you can do a two level cases using Either or Maybe, which capture all the specific conditions.

step <-case x of 
   pattern2 -> condition <- action
                if condition 
                then Just whatToDo
                else Nothing

   pattern5 -> condition <- action2
                if condition
                then Just whatToDo2

   _ -> Nothing

case step of
  Just action -> action
  Nothing -> case x of
       pattern 1 -> body1
       ....

Depending on your real case, you might want to use a different intermediate type, maybe even create your own custom one, or realize you actually don't even need any.

Exhaustive case with monadic guard

4 Answers4