Jon Purdy
Jon Purdy

Reputation: 54971

Exhaustive case with monadic guard

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?

Upvotes: 3

Views: 591

Answers (4)

mb14
mb14

Reputation: 22596

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.

Upvotes: 0

Jon Purdy
Jon Purdy

Reputation: 54971

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.

Upvotes: 0

Benjamin Hodgson
Benjamin Hodgson

Reputation: 44634

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.

Upvotes: 3

chi
chi

Reputation: 116139

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.

Upvotes: 3

Related Questions