Explicit bind for do notation

[ziman]

When I make a mistake in the middle of a do block, the errors I get tend to be quite unhelpful. Consider this program, where I try to add 1 to (). (The example is a bit contrived to get a short program with multiple plausible disambiguations of >>=.)

(>>=) : IO a -> IO b -> IO b
(>>=) f x = f *> x

main : IO ()
main = do
  printLn $ "foo"
  printLn $ "moo"
  map (+1) $ do
    printLn $ "boo"
  printLn $ "moo"
  printLn $ "moo"
  printLn $ "moo"

The above program produces these errors:

1/1: Building x (x.idr)
x.idr:10:3--11:3:While processing right hand side of main at x.idr:5:1--13:1:
Sorry, I can't find any elaboration which works. All errors:
If Main.>>=: Sorry, I can't find any elaboration which works. All errors:
If Main.>>=: Sorry, I can't find any elaboration which works. All errors:
If Main.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
    ?_ -> IO ()
and
    IO ?b

If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
    ?_ -> IO ()
and
    IO ?b

If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
    ?_ -> IO ()
and
    IO ?b

If Prelude.>>=: Sorry, I can't find any elaboration which works. All errors:
If Main.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
    ?_ -> IO ()
and
    IO ?b

If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
    ?_ -> IO ()
and
    IO ?b

Error(s) building file x.idr

There's no mention of Num or () or any hint of what's really wrong because the disambiguation errors get in the way.

For debugging, or maybe for real-life use, too, I always wanted to say explicitly which bind I mean.

(>>=) : IO a -> IO b -> IO b
(>>=) f x = f *> x

main : IO ()
main = do @{Prelude.(>>=)}  -- aha!
  printLn $ "foo"
  printLn $ "moo"
  map (+1) $ do
    printLn $ "boo"
  printLn $ "moo"
  printLn $ "moo"
  printLn $ "moo"

The resulting error message points exactly where it should:

1/1: Building x (x.idr)
x.idr:8:7--8:12:While processing right hand side of main at x.idr:5:1--13:1:
Can't find an implementation for Num ()
Error(s) building file x.idr

This patch adds this functionality. I don't really care about the syntax; I chose @{...} to avoid clashing with do { f ; x } but I could also imagine do with (Prelude.(>>=)) or something else.

[ziman]

TODO: add tests and documentation for this

[gallais]

Here is a thought: how about a more general contextualisation mechanism allowing users to focus on a specific namespace in a sub-expression?

The expression using NS e would mean that in case there is an ambiguity in e, we prioritise the namespace NS.

using Prelude $ do
  ...

would allow you to recover your proposition but we could also contextualise many more expressions where these kind of ambiguities would also bite us!

These things nest well: using NS2 $ using NS1 e means that:

• if there is an ambiguity in e that involves NS1 as a potential solution, we pick it
• otherwise if there is an ambiguity in e that involves NS2 as a potential solution, we pick it
• otherwise we use the usual ambiguity resolution algorithm

[ziman]

I'm afraid this would not work for the cases discussed above (in particular, the program shown above). I want to stop all disambiguation because no namespace is a solution. Otherwise it would try NS1, then it would try NS2, and then it would run the usual disambiguation, and you'd get the same barrage of disambiguation errors.

On the other hand, I can see that if Prelude.(>>=) is tried first, maybe the corresponding error would appear in the first place, which would be more helpful than what we get now. I'm not sure if it really would appear first, though; we'd have to try it.

It's just that dealing with the fallout of disambiguation feels so... unnecessary. I know I want Prelude.(>>=). I don't need disambiguation. I want to tell that to Idris so it can help me better.

Besides, this option is more general in another way. The content of @{...} can be an arbitrary expression so you can say @{\x, f => x >>= f} or something more useful. But I can't come up with a compelling use case for this at the minute...

BTW, Idris1 has exactly what you propose, written with NS e. :)

[gallais]

My proposal was that if we have an ambiguity and one of the potential solutions is NS then using NS forces us to commit to that disambiguation. So if that leads to a type error, we are then displaying that type error, we do not try to recover from it by attempting another disambiguation.

Sorry if my first message was (ah!) ambiguous.

[ohad]

I would very much like a general disambiguation mechanism. This has come up a lot with Frex, where I want to use type-with-structure, where a single type may have multiple structures, depending on the context. Type-classes/interfaces aren't really addressing it, as far as I can tell.

[ziman]

Right, so a solution is potential if there's an identifier in that namespace with the right name root; not if it typechecks.

What other things could we disambiguate using this and what would it look like?

[gallais]

Instead of writing List.foldr c n (List.map f (List.repeat k a)) you could write using List $ foldr c n $ map f $ repeat k a. It's essentially an expression-wide NS..

[edwinb]

Idris 1 had with Namespace <expr> where, if there was ambiguity inside <expr> it would default to the given namespace (I see @ziman mentioned that). I don't think this is quite what we want in general, though, because sometimes you want to be a bit more precise (that is, inside the expression there might be some names that you don't want to disambiguate the same way, but happen to be in the declared namespace). For the initial problem, sometimes I do something like let x = Prelude.(>>=) in ....

Anyway - we definitely need more control, somehow. Maybe if you say with x e, the x could be either a namespace or a specific name (or a list of both)?

I can see the value in being explicit on do as well, I'm just not sure about the proposed syntax because in @{x} the x would typically be a dictionary, not a method, so it's not consistent with existing uses of @{x}. Idris 0, in the dim and distant past, had do using (bind, return) because it didn't have interfaces yet, so maybe that is something to consider...

[ziman]

@ohad what's your use case for disambiguation? Can you give examples?

[ziman]

Using with or using or whatever on the whole block feels like a bit too much. Like Edwin says, there might be names in the block that you may want to disambiguate in a different way. My particular use case is big do blocks in the Idris compiler, where there's a lot going on. Maybe the explicit namespace given by with could apply only to the do construct itself but not its contents?

In my use case, all I need is to localise the error in big do blocks. I don't remember to struggle with disambiguation in other scenarios, such as what Guillaume describes; not sure if Guillaume runs into that often or if it's just a nice-to-have idea. I think I don't run into that myself because it's easy to add (temporary) namespaces to individual identifiers in an expression to localise errors. You can't do that in a do block, however.

On the other hand, having a nice general disambiguation method would be great, of course.

Also, I've just tried using with Monad do in Idris 1 and it does point out the error correctly in my test program above. I don't know whether it commits to Monad.(>>=) as desired, or whether it just orders error messages so that the one printed happens to be the useful one.

Other people may have other use cases, so Ohad's input would be helpful, too.

[gallais]

Maybe if you say with x e, the x could be either a namespace or a specific name (or a list of both)?

That sounds great.

[ziman]

I have to say I do like with Prelude.(>>=) do, too.

[ziman]

Closed in favour of https://github.com/edwinb/Idris2/pull/359.