Nested action notation to avoid annoyance(Meta programming related)

[Wxkj99]

(Meta programming related)
Codes like:

    do
        x <- get
        putStrLn $ "Number " ++ show x

are annoying. Can we manage to enrich the do notation to make it into one line just like in Lean4?

(And this need seems common. Have somebody already written one?)

[jaror]

There is some previous discussion:

• Monadic Bang: A plugin for more concise do-block notation, inspired by Idris
• Borrow some Applicative/Monad syntax from Idris · Issue #527 · ghc-proposals/ghc-proposals · GitHub

[Wxkj99]

The plugin is very helpful! Thanks a lot!

[atravers]

But also be careful where you use it. Haskell is non-strict whereas Lean4 and Idris are strict, so not all of their “syntactic sweeteners” can be trivially reimplemented in Haskell.

[ocramz]

TIL Lean has monads? now that’s something I can wrap my head around

[evincar]

I also proposed this as InlineBindings in 2017: Add InlineBindings proposal. by evincarofautumn · Pull Request #64 · ghc-proposals/ghc-proposals · GitHub. Lean’s syntax is this plus parentheses.

Nowadays if I want this I use monadic-bang. It’s nice that it doesn’t have to be an extension, but I still think maybe it should be, because it reveals a lot of minor issues with plugins (summarised under “Caveats”).

[atravers]

@evincar

It’s nice that it doesn’t have to be an extension, but I still think maybe it should be […]

From where this was previously discussed, as provided by jaror:

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

  ---

  Call by Effect (2009)

  (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.

  ---

…hence the final Caveat for monadic-bang:

[…] the plugin is usually best used in situations where the order in which effects happen makes no difference.

(and the associated detail) along with my cautionary post earlier. As for that second Lean example:

def f (x y : Nat) : IO Unit := do
  if (<- isGreaterThan0 x) && (<- isGreaterThan0 y) then
    IO.println s!"{x} and {y} are greater than 0"
  else
    pure ()

(page 15 of 17, again)

Similarly, short-circuiting ∨ and ∧ operators cannot be defined as functions for arguments with side effects. The side effects will invariably occur […]

Now just imagine the ordering of those side effects changing with each run of the program:

• Compile with threaded RTS by default by ulysses4ever · Pull Request #240 · ghc-proposals/ghc-proposals · GitHub

• #16126: Make -threaded the default · Issues · Glasgow Haskell Compiler / GHC · GitLab

• Make GHC -threaded the default RTS

…it might just be easier to use Lean instead of trying to extend Haskell in this way.

[evincar]

The caveats I was referring to are all to do with poor source locations and error messages from GHC and lack of support in GHCi. I’m saying it would be better to fix this so that plugins don’t suffer from these issues, but possibly easier to get better UX from an extension.

I’m fine with the scoping semantics. To me this doesn’t feel much different from any other “hoisted” inline structure—lambdas, string literals, string interpolation, comprehensions, and so on.

It’s true that (<- m1) && <- m2 has the same issue as m1 <&&> m2 where (<&&>) = liftA2 (&&). If you want sequencing of effects, you need something like m1 <&&> m2 = m1 >>= \case { True -> m2; False -> pure False }. My feeling is that this doesn’t worsen the learning pitfalls that Haskell already has about execution vs. evaluation, and I personally don’t mind just adding another level of do if it’s really necessary, like when !m1 do when !m2 ….

[atravers]

@evincar

The caveats I was referring to are all to do with poor source locations and error messages from GHC and lack of support in GHCi.

…if these problems afflict most other plugins: certainly! But if it’s mostly a problem for “semantics-bending” plugins such as monadic-bang, it may not be so easily solved by expanding GHC(i)'s plugin infrastructure.

---

@evincar

My feeling is that this doesn’t worsen the learning pitfalls that Haskell already has about execution vs. evaluation, and I personally don’t mind just adding another level of do if it’s really necessary, like when !m1 do when !m2 ….

Hmm - that begs the question: how well does monad-bang work with do-do notation? As for those “learning pitfalls”…they’re usually associated with monadic types having visible (outside the program) effects - other monadic types like ST s a, Either c a, Maybe a and [a] seem to be less confusing with regards to their execution versus their evaluation.

But as the examples in the OP clearly show, Lean’s monadic !-notation also works with IO a, the original monadic type having visible effects. On that point, and also from the second example:

Here is an example with two nested actions. Note that both actions are executed even if x = 0.

def f (x y : Nat) : IO Unit := do
  if (<- isGreaterThan0 x) && (<- isGreaterThan0 y) then
    IO.println s!"{x} and {y} are greater than 0"
  else
    pure ()

…because Lean is strict, therefore both arguments to (&&) would be evaluated first.

But what stops Lean from transforming that example into:

def f (x y : Nat) : IO Unit := do
  if (<- isGreaterThan0 y) && (<- isGreaterThan0 x) then
    IO.println s!"{x} and {y} are greater than 0"
  else
    pure ()

…is Lean more than just strict - does it also preserve the ordering of (what appear to be) expressions? By default Haskell doesn’t, and for good reason:

(page of 210)

[…] the seemingly simple ‘in the order of occurrence’-rule is hardly adequate in the presence of β-reduction, as in the following small program:

let
   f x y = g y x
   g x y = h y y
   h x y = "what?"
in f (puts "hello ") (puts "world\n")

What is this program supposed to write on the screen? Depending on the interleaving of reductions and input/output-operations, it might print any of "hello world\n", or "world\nhello ", only "hello ", only "world\n", twice "hello ", or nothing at all, since none of the parameters needs to be evaluated to compute the final result of "what?".

Functions, Frames and Interactions (1998).

Again, it might just be simpler to use Lean rather than try to duplicate its monadic !-notation in Haskell…