Nested action notation to avoid annoyance(Meta programming related)

atravers · August 18, 2024, 12:59am

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

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

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