Applicative and do-notation

Stream: lean4

[Shreyas Srinivas]

People have thought about this btw

https://simonmar.github.io/bib/papers/applicativedo.pdf

[Shreyas Srinivas]

They make the case they in many cases one can infer when to use applicative combinators instead of monadic bind within do notation

[Kyle Miller]

@Shreyas Srinivas That's for Applicative, not Alternative — I don't see anything in the paper that would be relevant. The paper's certainly interesting.

[Shreyas Srinivas]

Yeah but alternatives are applicatives

[Shreyas Srinivas]

I checked and this is also mentioned in the lean reference manual

The Alternative type class describes applicative functors that additionally have some notion of failure and recovery.

Source: https://lean-lang.org/doc/reference/latest/Functors___-Monads-and--do--Notation/

[Eric Wieser]

Shreyas Srinivas said:

They make the case they in many cases one can infer when to use applicative combinators instead of monadic bind within do notation

at risk of derailing the thread further, lean4#10231 and lean4#10202 go a little in this direction

[Eric Wieser]

From the paper that you link

But, tantalisingly, fx manifestly isn’t used by the second call, so we actually could run the two in parallel.

Does Lean today have any monads that allow f <$> gx <*> gy to run gx and gy in parallel?

[Shreyas Srinivas]

I don't think it is quite off-topic. The same idea that 's applied to applicatives can be applied to alternatives.

[Shreyas Srinivas]

Eric Wieser said:

From the paper that you link

But, tantalisingly, fx manifestly isn’t used by the second call, so we actually could run the two in parallel.

Does Lean today have any monads that allow f <$> gx <*> gy to run gx and gy in parallel?

Monads have a sequential dependency. You always evaluate the first argument to the bind to be able to apply it to the second. So it might not make sense to do this for Monads themselves. However, for applicatives this is not the case, all arguments can be evaluated in parallel (or any sequential order). This is also true for Alternatives, for example multiple match attempts by Parser can be executed in parallel.

[Eric Wieser]

Right, hence my question "Does Lean today have any monads that [execute applicative operations] in parallel". I was not asking about bind operations.

[Shreyas Srinivas]

Eric Wieser said:

Right, hence my question "Does Lean today have any monads that [execute applicative operations] in parallel". I was not asking about bind operations.

It wouldn’t be a monad without the bind operation would it? Just an applicative? Anyway, I think we are in broad agreement that a do notation for applicatives (and by extension alternatives) with parallel execution is worth exploring.

[Eric Wieser]

Irrespective of whether the bind operation exists, my question is about f <$> gx <*> gy which does not mention it. Of course, a monad can implement seq and map in terms of bind, but it is not required to do so.

[Shreyas Srinivas]

To further clarify, there are two separate, somewhat orthogonal issues :

1. Extending do notation to desugar into the applicative <*> (and maybe also <|>) operator instead of the monadic >>= operator where possible.
2. Parallel execution of applicative actions.

[Notification Bot]

13 messages were moved here from #lean4 > Alternative and do-notation by Eric Wieser.

[Eric Wieser]

(I think this discussion is worth keeping, but let's remove the distraction from the first | proposal; feel free to edit the first message to quote something from the original thread to make it make more sense)