Church-encoded free monad

Stream: new members

[Adrien Champion]

I have a question regarding the free monad, or more precisely regarding a "Church-encoded version" of the free monad.

I'm interested in an efficient pause monad, i.e. a monad that can suspend computations. It lead me here

• https://stackoverflow.com/questions/10236953/the-pause-monad

where the accepted answer references three great blog posts, though you need to change the background to be able to read them.

[Adrien Champion]

But first, thanks to

• https://stackoverflow.com/questions/78274957/how-to-define-free-monads-and-cofree-comonads-in-lean4/78275159#78275159 (which I found originally in this Lean 4 Zulip thread)

I managed to write a working Pause monad which looks like this.

free version

/-! # Defining `Free` -/

inductive Free (F : Type u → Type u) (α : Type u) : Type (u + 1)
| protected pure : α → Free F α
| free : ∀ (β : Type u), F β → (β → Free F α) → Free F α

namespace Free

protected def bind : Free F α → (α → Free F β) → Free F β
| .pure a, f => f a
| free β fc g, f =>
  free β fc (fun c => g c |>.bind f)

instance instMonad : Monad (Free f) where
  pure := Free.pure
  bind := Free.bind

instance instMonadLift : MonadLift M (Free M) where
  monadLift m := free _ m .pure



/-! ## Now I can write `Pause` -/

inductive Pause.Op (σ : Type u) (α : Type u)
| mutate : (σ → σ) → α → Op σ α
| yield : α → Op σ α

abbrev Pause (σ : Type u) :=
  Free (Pause.Op σ)

namespace Pause

def mutate (f : σ → σ) (next : α) : Pause σ α :=
  liftM (Pause.Op.mutate f next)

def yield (a : α) : Pause σ α :=
  liftM (Pause.Op.yield (σ := σ) a)

def done (a : α) : Pause σ α :=
  .pure a

def step (code : Pause σ Unit) (state : σ) : σ × Option (Pause σ Unit) :=
  match code with
  | .pure () => (state, none)
  | .free _ (.mutate f next) k =>
    let code := k next
    step code $ f state
  | .free _ (.yield next) k => (state, k next)

def test : Pause Nat Unit := do
  mutate Nat.succ ()
  yield ()
  mutate Nat.succ ()
  yield ()
  mutate Nat.succ ()
  yield ()
  done ()

/-- info:
-> 1
-> 2
-> 3
done 3
-/
#guard_msgs in
  #eval do
    if let (s, some nxt) := test.step 0 then
      println! "-> {s}"
      if let (s, some nxt) := nxt.step s then
        println! "-> {s}"
        if let (s, some nxt) := nxt.step s then
          println! "-> {s}"
          if let (s, none) := nxt.step s then
            println! "done {s}"

end Pause

end Free

[Adrien Champion]

I was afraid because Free is u + 1 since it quantifies on β which is a Type u, but it works.

That's great, but if I understand the first link I provided it yields code that's asymptotically slower than necessary.

So I went for the Yoneda/Rec encoding discussed in the second blog post reference (beware the aggressive background), which goes like this unless I messed something up.

Church-encoded

/-! # Defining `Fre` through `Yoneda` and `Rec` -/

abbrev Yoneda (F : Type u → Type u) (α : Type u) :=
  ∀ {β : Type u}, (α → β) → F β

namespace Yoneda

def drop (y : Yoneda F α) : F α :=
  y id

instance instMonad [Monad M] : Monad (Yoneda M) where
  pure a :=
    fun k => return k a
  bind y f :=
    fun k => y.drop >>= (f · k)

end Yoneda



abbrev Rec (M : Type u → Type v) (α : Type u) : Type (max u v) :=
  (M α → α) → α

abbrev Fre (M : Type u → Type u) :=
  -- `∀ {β : Type u}, (α → β) → (M β → β) → β`
  Yoneda (Rec M)

namespace Fre

instance instMonad : Monad (Fre M) where
  pure a := fun k _k' => k a
  bind self f := fun k k' =>
    self (f · k k') k'

instance instMonadLift [Functor M] : MonadLift M (Fre M) where
  monadLift m := fun k k' =>
    k <$> m |> k'

def lift [Functor M] : M α → Fre M α :=
  monadLift



/-! ## Now I can define `Pause` -/

inductive Pause.Op (σ : Type u) (α : Type u)
| mutate : (σ → σ) → α → Op σ α
| yield : α → Op σ α

/-- Needed to use `Fre.lift` directly. -/
instance Pause.Op.instFunctor : Functor (Op σ) where
  map f
    | mutate g a => mutate g (f a)
    | yield a => f a |> yield

def Pause (σ : Type u) :=
  Fre (Pause.Op σ)

namespace Pause

def mutate (f : σ → σ) (next : α) : Pause σ α :=
  Op.mutate f next |> Fre.lift

def yield (a : α) : Pause σ α := fun conv tail =>
  Op.yield (conv a) |> tail

def done (a : α) : Pause M α :=
  Fre.instMonad.pure a

instance instMonad : Monad (Pause σ) := by
  unfold Pause
  exact inferInstance

def step (code : Pause σ α) (state : σ) : σ × Option (Pause σ α) :=
  sorry
  -- code (fun _ => (state, none))
  --   fun
  --   | .mutate f (state, res?) => sorry
  --   | .yield res => sorry

end Pause

end Fre

[Adrien Champion]

But now I don't see how I can write the Fre.Pause.step function. My understanding is that I need to get code to produce the result I want, meaning the (hidden) β : Type u in Fre's definition must be σ × Option (Pause σ α) or something similar.

But that can't work since β : Type u and σ × Option (Pause σ α) : Type (u + 1).

[Adrien Champion]

At this point I assume I discovered something well-known about type constructors like Fre in constructive languages and/or languages with non-cumulative type universes. Probably that if allowed this would bring untyped lambda-calculus or something.

Is it the case, or did I mess something up?

If it's the former, is there a way around it? Like using Free but doing something tricky with SeqLeft/SeqRight?

If it's the latter, I would appreciate if anyone had time to elaborate.