Support type annotations on LHS of a monadic bind `<-`

[joelberkeley]

• [x] I have read CONTRIBUTING.md.
• [x] I have checked that there is no existing PR/issue about my proposal.

Summary

I want to be able to annotate the LHS of a monadic bind with types and quantities, just like with let. I usually want this when debugging type errors.

Motivation

If my function is not type checking, I scatter the code with annotations until I find the problem. This is easy with let, but with monadic bind, I can only pseudo-annotate the RHS with the, like

foo : IO Nat

main : IO ()
main = do
  x <- the (IO Nat) foo
  printLn x

However, this is verbose, in part because I have to name the monad in the "annotation". I'd much rather be able to write

main : IO ()
main = do
  x : Nat <- foo
  printLn x

The proposal

On the LHS of a monadic bind, rather than just a pattern, you can also add quantity and/or type annotations, like

f = do
  0 x <- foo
  ?res

g = do
  x : Nat <- foo
  ?res

h = do
  0 x : Nat <- foo
  ?res

I don't believe there would be any breaking changes, as it's optional, and I can't think of any valid syntax like it. The syntax would identical to the syntax between let and =.

Examples

see above

Technical implementation

This is beyond me atm.

Alternatives considered

No other options come to mind

Conclusion

This feature has received interest from core contributors. I can also imagine it using a similar grammar to the monadic let binding, even if it's interpreted differently, so I don't expect it to diverge from the current grammar, just add to it.

[buzden]

It also needs to be thought how this feature would interplay with pattern matching and shortcut alternatives:

do (a, b) : (X, Y) <- foo
   1 (c, d, e) : (A, B, C) <- bar
   5 : Nat <- baz
     | 6 => unbaz
     | _ => unbaf
   unfoo

[joelberkeley]

Those appear to me to all agree with how let bindings work (which is a very good thing, as having subtly different syntax for each would be a recipe for confusion)

[dunhamsteve]

I don't think the 5 example is consistent with the current behavior of let. Because of parsing for multiplicities, let will give a parse error for:

let 5 := ...

and

let 5 : Nat := ...

but accepts:

let (5) := ...

The parser for multiplicity could be tweaked to only have this behavior for 0 and 1, but it might rule out having other multiplicities in the future.

[joelberkeley]

what about let 5 : Nat =?

[dunhamsteve]

Currently that is a parse error:

1: Couldn't parse declaration.

src.Temp:12:13--12:14
 08 | --      then S (countFst (x :: zs) | zs) 
 09 | --      else countFst (x :: zs) | zs
 10 | 
 11 | foo : Nat -> Nat
 12 | foo x = let 5 : Nat = x | _ => 42 in 6
                  ^
... (6 others)

If you put parens around the 5, it parses, because the parser for multiplicity doesn't see the number.

[dunhamsteve]

Because of this - it maybe parses a number and then decides its an error if there is a number there that is not 0 or 1. Arguably correct if we plan to support other numbers someday?

  multiplicity : OriginDesc -> EmptyRule RigCount
  multiplicity fname
      = case !(optional $ decorate fname Keyword intLit) of
          (Just 0) => pure erased
          (Just 1) => pure linear
          Nothing => pure top
          _ => fail "Invalid multiplicity (must be 0 or 1)"

If we do want a bare 5 to work, this would have to change to succeed without consuming anything for integers other than 0 or 1.

[buzden]

Arguably correct if we plan to support other numbers someday?

Maybe, but someday we will have support of whole expressions for quantities, and this will anyway cause similar problems on the next level

[joelberkeley]

OK thanks. I'd only suggest parsing what can be parsed currently in let, even using the same parser code if possible

[dunhamsteve]

I've coded this up and the type annotations are working fine, but I need to drop the multiplicities on the pattern matching version. We can still have quantities on bare variables.

There are two problems with quantities on patterns. One is that the syntax is breaking existing code (CI fails). E.g. Network.Socket.Data does:

nullPtr p = do 0 <- primIO  $ prim__idrnet_isNull p

which no longer parses because 0 is getting eaten as a quantity.

The second issue is that it won't work at all in the current Idris (this is issue #2513). You can see that while the syntax is accepted for let, it's not functioning correctly. E.g. y is unerased in the hole in this code:

blah : Maybe Nat -> Nat
blah x = let 0 (Just y) = x | Nothing => 0 in ?hole

Issue #2513 is fixed in PR #2535 which we closed pending new core. I'm happy to revive that work separately, if and when we're ready to merge it.

But the type annotations and quantities on variables do work. I can PR this after backing off the pattern quantities. I'll leave the previous commit in the branch history.