Zulip Chat Archive

Stream: lean4

Topic: algebraic effects and handlers?


view this post on Zulip Jason Gross (Mar 23 2021 at 17:43):

I've heard that algebraic effects and handlers form a nicer basis for stateful computation than monads (for example, there's no need to lift operations as there is when you nest monads). Has anyone thought about basing things in Lean on algebraic effects and handlers rather than monads? (c.f. https://xnning.github.io/papers/haskell-evidently.pdf , for example)

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 17:50):

Yes, it's a topic we've considered before. The very short answer is that AFAIK there are only two ways to avoid lifting, neither of which is acceptable for building nontrivial programs like Lean itself: by blowing up the runtime overhead (open union encoding etc.) or the compile time overhead (monomorphization).

view this post on Zulip Daniel Selsam (Mar 23 2021 at 18:06):

Jason Gross said:

I've heard that algebraic effects and handlers form a nicer basis for stateful computation than monads (for example, there's no need to lift operations as there is when you nest monads). Has anyone thought about basing things in Lean on algebraic effects and handlers rather than monads? (c.f. https://xnning.github.io/papers/haskell-evidently.pdf , for example)

FWIW I have found the auto-lifting in Lean4 to be so good that I almost never need to think about this.

view this post on Zulip Jason Gross (Mar 23 2021 at 19:28):

Open union encoding is where everything is polymorphic over all the other effects (or underlying monads) that might be present?


Last updated: May 18 2021 at 22:15 UTC