algebraic effects and handlers?

Stream: lean4

[Jason Gross]

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)

[Sebastian Ullrich]

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).

[Daniel Selsam]

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.

[Jason Gross]

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

[Locria Cyber]

Maybe have compile-time support for union?

[Locria Cyber]

I made a library for this. https://github.com/locriacyber/lean-eff

[Locria Cyber]

See Example.Handler and Example.HandlerControl for example.

I don't know how to bench mark, but the runtime of those seem minimal.

using this:

#!/usr/bin/fish
time for i in (seq 10000)
    ./test_control
end >/dev/null


time for i in (seq 10000)
    ./test_handle
end >/dev/null

[Locria Cyber]

There is no difference in time used. (probably because it's IO bound)

[Locria Cyber]

I would love to remove the sorry in my code, if anyone want to help.

[Mario Carneiro]

Can you make a #mwe? Those should be proved automatically

[Locria Cyber]

inductive Free : (_monadish: Type u -> Type v) -> (_ret: Type u) -> Type _ where
| pure : α -> Free ε α
| bind : ε α -> (α -> Free ε β) -> Free ε β

/-- Proof that a list has an element -/
class inductive Elem : α -> List α -> Type _ where
| zero : Elem x (x::xs)
| succ : Elem x xs -> Elem x (y::xs)

namespace Elem
  instance : Elem a (a :: xs) := Elem.zero
  instance [prev: Elem a xs] : Elem a (x::xs) := Elem.succ prev
end Elem

inductive Union : {α : Type u} -> List (α -> Sort v) -> α -> Sort _ where
| mk [prf: Elem ε εs] : (x : ε α) -> Union εs α

namespace Union
  example : Type _ := Union [IO] Unit

  def simplify : Union [ε] α -> ε α
  | Union.mk (prf := Elem.zero) x => x
end Union

@[reducible]
def Eff es := Free (Union es)

namespace Eff
  def run1 [Pure ε] [Bind ε] : (stacked: Eff [ε] α) -> ε α
  | Free.pure x => pure x
  | Free.bind val cont => Bind.bind (m:=ε) (Union.simplify val) (λ a => run1 (cont a))
  decreasing_by sorry
end Eff

[Locria Cyber]

I can't prove Eff.run1 terminate.

[Locria Cyber]

Lean doesn't let me do this

mutual
  def bbb (_ : Nat) : Free Option Nat := Free.bind (Option.some 1) aaa
  def aaa (_ : Nat) : Free Option Nat := Free.bind (Option.some 1) bbb
end

So it's safe, right?

[François G. Dorais]

If you replace sorry by { simp_wf; done } you will see the issue: there is no reasonable way to assign a meaningful sizeOf value to cont. With bind : ε α -> (α -> Free ε β) -> Free ε β you want the size of bind val cont to be larger than that of cont x for every x : α. This doesn't make sense, for example, when α is Nat and sizeOf (cont n) > n for every n : Nat.

Bottom line, the Free monad is too big for a measure into Nat. You will need to use a more general form well-founded recursion to make this work.

[Andrés Goens]

Locria Cyber said:

I made a library for this. https://github.com/locriacyber/lean-eff

@Locria Cyber did you migrate this repository somewhere else (i.e. is it still public somewhere)?

[Locria Cyber]

Andrés Goens said:

Locria Cyber said:

I made a library for this. https://github.com/locriacyber/lean-eff

Locria Cyber did you migrate this repository somewhere else (i.e. is it still public somewhere)?

https://git.envs.net/iacore/lean-eff