Monadic Bang: A plugin for more concise do-block notation, inspired by Idris

[JakobBruenker]

I’ve written a GHC plugin that lets you take things like the following code:

main :: IO ()
main = do
  putStrLn "Which argument would you like to print?"
  line <- getLine
  args <- getArgs
  putStrLn $ args !! read line

and instead write this code:

main :: IO ()
main = do
	putStrLn "Which argument would you like to print?"
	putStrLn $ !getArgs !! read !getLine

This is heavily inspired by Idris’s !-notation, the main difference being that this plugin only allows you to use ! inside of existing do-blocks, whereas Idris will insert a do if it doesn’t exist.

It currently works with ghc 9.4. You can find it here:

monadic-bang

Please feel free to try it out and let me know what you think!

[dixonary]

That’s awesome! Seems like a really useful feature, especially in IO or shelly-style code.

[rubenmoor]

putStrLn $ !getArgs !! read !getLine

could be written as

((!!) <$> getArgs =<< read <$> getLine) >>= putStrLn

or

putStrLn =<< ((!!) <$> getArgs =<< read <$> getLine)

if I got it right. I guess in absence of the monadic bang, the do syntax is a whole lot clearer. The monadic bang seems so elegant, it feels like cheating.

[david-christiansen]

The bang notation is great! There are a couple of pitfalls in the Idris syntax, however. For example,

main = do
  b <- findSomeBooleanInAFile
  if b
    then putStrLn $ "The temp file contains " ++ !(readFile "/tmp/thingy")
    else putStrLn "Not reading a file"

desugars to something like

main = do
  b <- findSomeBooleanInAFile
  x <- readFile "/tmp/thingy"
  if b
    then putStrLn $ "The temp file contains " ++ x
    else putStrLn "Not reading a file"

which has more effects than some readers might expect. The rule can be made more “natural” (but also more complicated) by e.g. special-casing things like if under do and only lifting the bind that high, but then things like when would behave differently from if.

The Lean rule is that if and case expressions that are a statement of a do block have implicit do blocks in each branch, which works well there, but would be a much bigger disturbance to Haskell and still doesn’t solve the when issue. And laziness means that control structures as functions are much more common in Haskell than in strict languages.

[david-christiansen]

And super cool plugin, BTW

[JakobBruenker]

Absolutely - if I’m understanding the options you’re suggesting correctly, there’s actually a third option, also involving speical-casing if and case:

You can desugar

do rest $ if !condition
          then f !foo
          else g !bar !baz

as

do _condition <- condition
   _if_body <- if _condition
               then do _foo <- foo
                       pure (Left (# _foo #))
               else do _bar <- bar
                       _baz <- baz
                       pure (Right (# _bar , _baz #))
   rest $ case _if_body of
     Left (# _foo #) -> f _foo
     Right (# _bar , _baz #) -> g bar baz

This is quite unwieldy, but what it means is essentially that actions in a branch will only be executed if that branch is selected. The advantage over having implicit dos in each branch is that here, the branches of the if do not need to have a monadic type.

I wanted to go for this at first, but in the end, it didn’t seem worth the significantly higher complexity in both specification and implementation, and as you say, it wouldn’t solve something like when anyway.

[santiweight]

Why can’t the rule be that then/else are always treated as implicit-do constructs? Simpler rule that covers the above cases no?

Edit: I see however, that the problem of custom-control-flow operators stands. that’s quite annoying I guess that would a lot more trouble than it’s worth, but at the least you could cover the builtin cases.

[JakobBruenker]

There’s a couple of reasons:

• I think it’s good to have consistency between built-in and custom control flow operators
• While inserting dos in specific situations isn’t a terribly complicated rule, it still makes the specification more complex
• As things are now, you can always insert an explicit do in each branch to get that behavior. However, if the plugin inserted dos there itself, it wouldn’t be possible to get the current behavior as easily.
• When you say “above cases”, I don’t know if you’re including the example from my comment, but, to be clear, that would not work with just inserting dos, since the branches don’t have monadic types, so you’d get a type error.

[nomeata]

@santiweight

I guess that would a lot more trouble than it’s worth, but at the least you could cover the builtin cases.

It seems tempting, but I think this would be a serious mistake. At least to me, the ability to define custom control operators (when, forM etc.) is close to the top advantage of a pure and lazy language like Haskell, and we should not give it up lightly. Let’s keep if as sugar, not as something special!

[JakobBruenker]

This conversation did get me thinking if perhaps there’s some way to support even custom control operators. Doesn’t seem likely, but it’s interesting to think about

[nomeata]

At least for IO, you could desguar

do foo (! act)

to

do x <- unsafeInterleaveIO act
   foo x

…

[JakobBruenker]

Tempting but I don’t think even that would be enough:

whileM (!getCount < 100) do something should execute getCount on every loop, but I think with unsafeInterleaveIO it would only be executed once

edit: Might have gotten the type of whileM a bit wrong, but you get the idea I think

[jaror]

One way to do it would be to have users write source annotations:

{-# ANN when [Data,Control] #-}

Meaning the first argument is data and the second is control.

I just tested it and it seems it is impossible to attach source annotations to functions in other modules, so that is unfortunate…

[santiweight]

As a small guess for a control flow operation, I think that monad-bang cannot appear in lazy arguments to a function. So something like when with the following strictness annotations (not real Haskell but you get the gist):

when :: !Bool -> ~(m a) -> m a

Then only allow monad-bang when present in strict argument positions…

Not great but also not terrible?

Note: while writing this, I realize that using ! for monad-bang notation is a bit of a non-starter. It’s super confusing that let !a = f !b uses two different meanings for bang

[atravers]

Before we’re all buried in syntactic sugar:

callbyeffect.pdf

^{(page 15 of 17)}
Furthermore we cannot express control operators such as if as functions. In Haskell, one may write:

tester True yes no = yes
tester False yes no = no

In a call by effect setting, any side effects of either yes or no will occur, which is almost surely not the intention of the programmer.

Problems like these could be why Idris is a strict language…

[jaror]

Instead of source annotations you can add custom comments like how Liquid Haskell does it:

{-@ when {Data} {Control} @-}

That solves the problem of adding annotations to imported functions.