Monadic operations inside `match` nested inside `with` have unexpected behaviour

[developedby]

Reproducing the behavior

When writing a monadic operation inside of a pattern matching statement nested inside a with block, the value returned by the match, assigned to the variable is the bind operation.

Users will expect instead for the operations to be executed, then the variable assigned and only then the following monadic operations executed.

Example:

def main():
  with IO:
    match []:
      case List/Cons:
        * <- IO/print("X")
        ok = 0
      case List/Nil:
        * <- IO/print("O")
        ok = 1
    return wrap(ok)

Here, the value of ok is λa (a IO/Call/tag IO/MAGIC "WRITE" (IO/FS/STDOUT, [79]) λ* 1) when we expected it to be 1.

This means that the print is never actually executed since it's stored inside of a wrap, which ends the IO action.

In the functional syntax, it's a bit more obvious that this happens:

main = with IO {
  let ok = match [] {
    case List/Cons:
      ask * = (IO/print "X")
      0
    case List/Nil:
      ask * = (IO/print "O")
      1
  }
  (wrap ok)
}

Syntactically, i don't know that is the best way of solving this.

In a previous version of Kind, we made the block inside with in a functional syntax be a separate AST that parses similar to the imperative one. That's not a very elegant solution, but it worked.

With the imperative syntax the correct compilation is pretty obvious. We just need to make the final assignment of the variable of a match inside a with be a monadic bind instead of a normal variable bind.

We need to solve how to do this in a nice way for the functional syntax and how to handle the interaction of nested blocks (how to deal with nested withs, nested other things, how to handle nested lets with separate with blocks, how to handle recursion in these nested blocks, etc).

System Settings

Bend: 0.2.36 HVM: 2.0.21

Additional context

No response

[developedby]

We can also not solve this issue directly and instruct users on the way of writing that will lead to the correct result. Basically, when your block has a monadic operation then it must return/assign a value with that monad as the type.

In the example above they are for the both syntaxes:

def main():
  with IO:
    match []:
      case List/Cons:
        * <- IO/print("X")
        ok = wrap(0)
      case List/Nil:
        * <- IO/print("O")
        ok = wrap(1)
    ok <- ok
    return wrap(ok)

and

main = with IO {
  ask ok = match [] {
    List/Cons:
      ask * = (IO/print "X")
      (wrap 0)
    List/Nil:
      ask * = (IO/print "O")
      (wrap 1)
  }
  (wrap ok)
}

It works as expected, but it's not very user friendly

[developedby]

We can implement the transformation I said in the OP and leave the functional as it is, like my comment above.

Maybe that's a good compromise, but I'd like for the two syntaxes to not have this kind of divergent behaviour.

[developedby]

I think the best way from a functionality point of view is adding <- assignments in final block position and instructing users that blocks that use <- take the type of the monad that's being used.

However, that's not very user friendly and would definitely be a large source of confusion for new users. I thought of making all blocks nested in a with return the monad type, but that's also not good because it leads to a big overhead in blocks that don't need monadic binds.

def main():
  with IO:
    * <- IO/print("hi")
    match []:
      case List/Nil:
        a <- wrap(0)
      case List/Cons:
        a <- wrap(1)
    return a

Here the a <- wrap part could be written much more simply as a = 0/1.

I still don't know how to do this in a nice way

[developedby]

I'll reopen this since we need to write documentation that explains how to do IO with matches, etc, properly