WIP: Case bind

[Ericson2314]

Provide a more concise why to handle failure patterns in do notation.

To be honest, I am writing this mainly to put #319 in context. I would certainly use this sugar all the time, but I am just more excited about shrinking the language via deprecation than growing it with via sugar.

Rendered

[nomeata]

Wasn’t there a way to be able to do

do
  res0 <- action
  case res0 of
    Bad0_0... -> ...
    Bad0_1... -> ...
    Good0... -> do
  res1 <- action
  case res1 of
      Bad1_0... -> ...
      Bad1_1... -> ...
      Good1... -> do
   ...

so that indentation doesn't grow? (Not equivalent when the order of pattern matters)

But maybe I am mistaken… or maybe that’s only the case in GHC-style code with explicit {…}.

[glaebhoerl]

This is currently motivated in terms of handling "failure cases", but do I understand correctly that it's a solution to the very common annoyance of having to bind the result of a monadic action to a name before you can case on it?

That is, where our current alternatives are:

result <- checkThing
case result of
    True  -> yesItIs
    False -> noItIsn't

or

checkThing >>= \case
    True  -> yesItIs
    False -> noItIsn't

this would add the possibility of:

case <- checkThing of
    True  -> yesItIs
    False -> noItIsn't

If so, I like it.

It suggests the analogous thing for if then else:

if <- checkThing
    then yesItIs
    else noItIsn't

[ocharles]

Is this the same as Agda's do notation pattern matching? They use:

  true ← p x ∷ []
    where false → []

I think it might be worth referencing that. https://agda.readthedocs.io/en/v2.5.4.1/language/syntactic-sugar.html

If it's not this, then please ignore this comment!

[Ericson2314]

@nomeata There is -XNondecreasingIndentation which is rather weirdly documented in https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/bugs.html#extension-NondecreasingIndentation .

There is also the similar extension which makes monsters like do { pure False; let; x = False; in pure 1; } work, whose name I forget. It is very confusing that the -XNondecreasingIndentation was enabled by default Haskell 98 but not Haskell 2010, while the latter is enabled by default in starting in Haskell 2010).

I dislike both of those for complicating layout, but -XNondecreasingIndentation absolutely deserves mention as an alternative.

@glaebhoerl Ah thanks, you made me realize my example was wrong. Fixed now. I will include the if version in the alternatives. I am less excited about doing it "for symmetry" because with #302 -XMultiWayIf, the other extension"for symmetry", can be deprecated as -XMultiWayLambda subsumes it.

[If anything I would advocated for a -XIfThenElse and -XNoIfThenElse so we can all stop worrying about it :). bool is more concise, case is more flexible, I have little use for if...then...else....'s awkward middle ground between.]

@ocharles Yes it is! I vaguely Idris did something like this, but couldn't find the docs so and moved on. I guess it was Agda I was mis-remembering.

[Ericson2314]

@glaebhoerl Oh but you do need the pattern before the <-. the point of this is for "early return" I personal find the >>= \case idiom fine for ending a do block with a case on action result.

[sgraf812]

John made me aware of this proposal after I came up with something similar in #319 (comment). I like it! Maybe it would serve as further motivation to add the particular loadInterface example from the linked comment, which uses the convoluted do { ...; ... }-style that Joachim refers to above.

this would add the possibility of:

case <- checkThing of
    True  -> yesItIs
    False -> noItIsn't

If so, I like it.

I'm afraid that won't work as expected, as you would still need to add an (albeit unreachable) continuation after the case _ <- checkThing of .... Your program would yield a syntax error and you'd need to write

blah = do
  case _ <- checkThing of
      True  -> yesItIs
      False -> noItIsn't
  error "unreachable"

The proposed extension is strictly about do blocks and morally like a <- in that another expression must follow.

Since the semantics we want is pretty clear, what follows is bikeshedding the syntax.

Is this the same as Agda's do notation pattern matching?

Interesting, I didn't know about that! The syntax seems a bit cleaner than the proposed one, although I'm not sure if we can implement it unambiguously.

I vaguely Idris did something like this

Me too. And now I found it: http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#pattern-matching-bind. Maybe we can implement something similar? Out of all the alternatives so far, I like that syntax the most. E.g.

do
  Good0... <- action0 
    | Bad0_0... -> ...
    | Bad0_1... -> ...
  Good1... <- action1
    | Bad1_0... -> ...
    | Bad1_1... -> ...
  ...

But | suggests that what follows is a guard. Maybe that syntax is also taken... And it only gets weirder if you actually write a guard:

do
  Good0... <- action0 
    | Bad0_0... | even blah -> ...
  Good1... <- action1
    | Bad1_0... -> ...
    | Bad1_1... -> ...
  ...

No, it seems that we should keep case of in there somewhere. In that case, I would also put p <-case e of alts on the table, but maybe that will need adjustments to the lexer and is only one space apart from p <- case e of ..., which has completely different semantics.

Summary:

• Agda uses p <- e where p_1 -> e_1; ...; p_n -> e_n. I tested it, our LR parser accepts it and we get full case alt including guards. Biggest pro: It doesn't look like case and thus doesn't convey the intuition that the where pattern match happens first.
• Idris uses p <- e | p_1 -> e_1; ...; p_n -> e_n. Similarly doesn't fit into our grammar and makes full case alts with guards look weird. Has the best looks IMO.
• p <-case e of alts puts the pattern on the LHS, but is too easily confused with p <- case e of alts, which has completely different semantics
• p case <- e of alts is some middle-ground. I'm a bit doubtful we can fit it into our grammar. Also the p is separated from <-, which makes it a bit ugly.
• So case p <- e of alts still wins over the others IMO
• But here's another idea: Maybe we can simply say p <- e of alts, without case! E.g., simply make the of alts optional. I just checked a quick prototype with happy and it seems unambiguous. So that's my preferred solution so far!

[chreekat]

case ... of {alts} makes me think all the alts are in {alts}. :)

It's probably not possible, but if could pick names out of a hat, I'd pick

do
  guard Good0 <- action0
    where
      Bad0_0 ... -> 

[sgraf812]

I really like this proposal and am thinking about adopting it. The only real open question to me is the syntax. I think I accurately summarised the different ideas in #327 (comment).

I'm quite attached to the terse p <- e of alts, but I think there are people like @chreekat who disagree, perhaps strongly, because it's too close to case of. I'm willing to let Agda-style p <- e where alts win here. Any other opinions?

Unfortunately, I don't think @chreekat's guard p <- e where alts is an option, because that steals syntax (I think guard p might parse as a pattern? Haven't tried) or at least introduces a new contextual keyword. It also means that because of the length of the prefix guard , the main code path p is further to the right than the regularly indented alts, which is a bit weird, too.

[tomjaguarpaw]

Is it clear what one should write if there are two "good" constructors? I can't see how I would proceed.

[sgraf812]

In that case I'd simply use the constructs available today, e.g. a case e of p -> rest; alts instead of p <- e where alts; rest. This proposal is written with error handling in mind, where there's exactly one path that has the most interesting/intricate logic. I'd never use Case Bind if the error handling takes more than 10 lines, for example; then I'd simply stick to regular case.

[tomjaguarpaw]

I believe that this proposal is suggested as a more general alternative to failable patterns in do notation. That's great! I'm strongly in favour of replacing syntax with more general syntax as long as the old syntax is thoroughly deprecated. If we keep accreting syntax then Haskell gets more and more complicated. It's a big headache for anyone who doesn't live in the language every day.

Alternatively, have we thoroughly fleshed out the library level solutions to this particular problem? For example, suppose we had

import Optics

match prism handler v = case matching prism v of
    Right r -> pure r
    Left l -> handler l

Then we could write

do
  ...
  v <- fetchData >>= match _Just \case
          Just j -> absurd j
          -- ^ Annoying that the type checker
          -- can't prove this impossible
          _ -> error "Not in map"
  pure (v + 1)

(requires BlockArguments but other recipes are possible)

No new syntax needed! Still, there are a few downsides of this "library" version when compared to the "syntax" version:

1. The big downside is that the handler has to handle the prism constructor (Just, in the example above) even though it is impossible. If the prism is not polymorphic you can't even use absurd!
2. It's annoying that you have to define prisms for every constructor you want to match on (or a specialised fused version of match prism).

But I think it's worth asking the question: are we thoroughly convinced that there is no solution to this problem unless we introduce new syntax?

[phadej]

@tomjaguarpaw Prisms don't work with patterns which expose the existential type variables, which is a motivation for failable patterns. So your approach doesn't solve the problem with newtype Some f = ... and pattern Some x = .... (@Ericson2314 could add that as an example to the motivation section. It could be solved by do desugaring knowing about COMPLETE or newtype existentials, but these are not coming any time soon AFAIU).

[Ericson2314]

@tomjaguarpaw Yes @sgraf812 and I both dislike today's fallible patterns in do notation, and #319 is a proposal to make an (anti-)extension to get rid of it, that is certainly deemed block on there being no replacement like that.

I firmly agree we must not not keep on adding more complexity without cleaning things up, too.

[sgraf812]

By the way, @tomjaguarpaw, the current "best practice" on error handling (with debatable looks) in do blocks within GHC is to use explicit layout + -XNonDecreasingIndentation. In #319 (comment) I show case a live example, namely:

     do { ...
        ; read_result <- case (wantHiBootFile home_unit eps mod from) of
                           Failed err             -> return (Failed err)
                           Succeeded hi_boot_file -> do
                             hsc_env <- getTopEnv
                             liftIO $ computeInterface hsc_env doc_str hi_boot_file mod
        ; case read_result of {
            Failed err -> do
                { let fake_iface = emptyFullModIface mod
                ; updateEps_ $ \eps ->
                        eps { eps_PIT = extendModuleEnv (eps_PIT eps) (mi_module fake_iface) fake_iface }
                        -- Not found, so add an empty iface to
                        -- the EPS map so that we don't look again
                ; return (Failed err) } ;

            Succeeded (iface, loc) ->
        let
            loc_doc = text loc
        in
        initIfaceLcl (mi_semantic_module iface) loc_doc (mi_boot iface) $

It becomes really hard to see where the early return is happening. For example the first case of isn't actually an early return, but the second one is. It is very non-obvious code. With the extension proposed here, we'd rewrite the second case of to a Case Bind, thereby explicating the early return semantics and contrasting it with the first case of, where we can't (fruitfully) use Case Bind. Then we could get rid of -XNonDecreasingIndentation and still keep the indentation for the main code path flat.

Edit: I agree we need to put more of these examples in the proposal. So maybe we should polish it first before asking for any buy-in from users/steering committee.

[Ericson2314]

Well, I guess the next step after #319 is rejected is to finish up this one.

[konsumlamm]

I honestly find this syntax very confusing. I had to read the example multiple times to see what's going on.

Normal case ... of ... has the form case <expression> of <alternatives>, but here we have case <first alternative> <- <expression> of <other alternatives>, so there is an alternative in the part where the expression usually is and it is special cased and the other alternatives are early returns. That doesn't reflect what case ... of ... does, so why reuse it's syntax for something different?

On first sight, it seems like one should just use something like ExceptT (or a custom version thereof) to solve this (I'm a bit surprised that noone has brought this up, is there a reason why it is no alternative?). Ironically, this proposal essentially special cases a use case (error handling) of monads by adding more do-notation sugar.

[tomjaguarpaw]

@konsumlamm, I believe that your objection is addressed in the second example of the Motivation isn't it? Still, like you I am skeptical that this new syntax pulls its weight.

[Ericson2314]

I honestly find this syntax very confusing.

I am happy to change it, very not attached to how it's written today.

On first sight, it seems like one should just use something like

If people used monad transformers in a very fine grained way, I would agree. But people tend to lug around big stacks in a very coarse-grained way, so I am not sure it is good. In particular stuff like MTL's catchError is quite bad, because the type system doesn't track which exceptions are in fact caught!

[Ericson2314]

@tomjaguarpaw I am not super excited about adding more syntax either, but it appears to be this is the way way anything like NoFallibleDo has a chance. My big motivation for that is a) confidence in the code I read and the ability for a team to collaborate without mistakes going unnoticed b) simplifying the language to remove cruft. But it seems the only way it will possible get through is a little default tweak on top of something for expressive power. I am saddened by the focus on "writing" over "reading", but as I would certainly use this syntax (e.g. cleaning up GHC, where monad transformers are not fashionable) I am willing to play ball.

[tomjaguarpaw]

If I am understanding this proposal correctly it entangles two separate concerns:

1. "case with default branch" to avoid deep nesting
2. Running the scrutinee in a monad before pattern matching it.

I don't see why these two concerns should be mixed. @glaebhoerl seems to be talking in favour of 2 without mentioning 1 as important. Yet 1 could very well be useful in pure code and this proposal doesn't support it, as far as I can tell.

For a concrete example of 1, consider the hypothetical syntax

stmt → case pat = exp of { alts } in rhs

desugared as

case p = e of { alts } in rhs ~> case e of { p -> rhs; alts }

Now this is a generic way of avoiding awkward nesting problems in all code. It does not have the unfortunate weakness of being restricted to do blocks only. A completely separate proposal could address 1, providing some syntax for allowing a monadic scrutinee in if and case statements (although personally that doesn't excite me).

[nomeata]

I'm also not very enthusiastic about this feature yet, but that won't stop me from throwing out shower thoughts about possible syntax. How about “trailing else”

  do <pat> <- <exp> else <alts>

(vaguely inspired by python ... if ... else ...). I find this reads out a bit more naturally. Not sure of this grammar would actually work.

[Ericson2314]

@tomjaguarpaw I see what you mean, but I guess subjectively I think nesting is not a problem for "normal expressions", and only do notation, by virtual of it's stylistic harkening to imperative programming, makes caring about "flatness" or the "appearance of sequentiality" tolerable foibles.

[tomjaguarpaw]

subjectively I think nesting is not a problem for "regular expressions", and only do notation, by virtual of it's stylistic harkening to imperative programming

I can see why that would be a popular point of view, but personally I'm moving more towards using Haskell in the "best imperative language" style, using "sequences of let expressions", rather than where clauses that jump control flow all around the page. See, for example, my Python-to-Haskell translation at https://discourse.haskell.org/t/help-with-purses-problem/3883/7.

If this proposal worked for "regular case", rather than only "case inside do" then I would be strongly supportive of it, as opposed to rather resistant to it.

[Ericson2314]

@nomeata hmm @sgraf812 proposed of which is nicely a layout herald. but else captures the meaning. Por qué no los dos?

do <pat> <- <exp> else of <alts>

to be read "bind exp through pat or else match one of alts". Hamfisted win!

[Ericson2314]

@tomjaguarpaw perhaps you and @sgraf812 should take this proposal from me? @sgraf812 was already more enthusiastic about the idea. And if there is a variant that makes you enthusiastic that would be good, too. I don't see myself being super enthuasiastic about any variation so I am probably better of supporting someone who is. And if these was something you both were enthusiastic about that would be very good indeed.

[tomjaguarpaw]

Sorry if my comments are motivation-reducing, that wasn't my intention. Personally I'm more supportive of no proposal than any particular proposal. I just can't envisage Haskell's syntax getting better piecemeal. I think we need a ground-up rethink of all the syntax we value, the syntax we don't, and the best way to fit everything we value together. But that's a multi-year effort, probably.

[Ericson2314]

@tomjaguarpaw I am quite sympathetic to that. I wrote #442 in hopes that we can accumulate a longer and more comprehensive plan than we can with isolated proposals, combined as a difficult mentally exercise. I suppose I would be curious to hear your thoughts on that over that.