Stuck on ManyT in "Functional Programming in Lean"

Stream: new members

[Sebastian Miele]

Hello!

I am currently working through Functional Programming in Lean and got stuck on the exercise that asks to create the monad transformer ManyT in section 6.3.2.

Up to this one, I found the exercises in the book not difficult, and I enjoy the book and Lean in general very much. But I just did not find a suitable definition for ManyT, yet, and for some while. Can anyone give a definition for a suitable ManyT, or a hint?

What I tried so far:

The Many type in the book is a pure list type with a laziness optimization that holds the rest of a list without already having evaluated it. When I defineManyT m α := m (Many α) I cannot find a way to meaningfully transfer the laziness of Many into the underling monad. And without that, it effectively degenerates to a ListT m α := m (List α) where the bind operator is List.flatMapM. But that is non-associative.

As far as I see it, in order for ManyT to retain associativeness, running a value of type ManyT m α would have to be able to compute one element at a time in m. It would have to be some kind of iterator in the underlying monad. So that the bind operator of the monad can work strictly depth first.

But I did not manage to define something along that lines that satisfies the type system. One guess was ManyT m α := m (Option (α × ManyT m α)). But the type system rejects that, either because of universe levels (when m : Type u → Type v), or because of non-terminating recursive definition of the type (when m : Type u → Type u).

Best wishes
Sebastian

[Jakub Nowak]

Hi!

Well, actually union and bind implementation of Many in the book, aren't in fact lazy. Only more is.

E.g., you can create infinite list with Many.more:

partial def count (i : Nat := 0) : Many Nat := Many.more i fun () ↦ count (i + 1)
#eval Many.take 20 count

However, the addsTo implementation is not lazy, it computes all the elements of the result when called. If I try

#eval printList $ addsTo 15 (List.replicate 100 1) |>.take 1

it just crashes online Lean 4. On local machine it might not crash, and just run for a very long time.

You can try implementing it differently, to make it lazy. This will require some changes in the implementation of Many or its operations.
Implemented correctly it should run this without any problems:

#eval printList $ lazyAddsTo 15 (List.replicate 1000 1) |>.take 1

Feel free to ask more questions and good luck!

[Sebastian Miele]

Thanks a lot for the answer, @Jakub Nowak. I was able to introduce more laziness into union, bind and addsTo, so that addsTo 15 (List.replicate 1000 1) does not crash anymore. Now union's second argument is lazy. That way the recursive case of binddoes not take all of the first argument at once.

universe u
variable {α β γ: Type u}

inductive Many (α : Type u) where
| none : Many α
| more : α → (Unit → Many α) → Many α

def Many.one (x : α) : Many α := .more x (fun () => .none)

def Many.union : Many α → (Unit → Many α) → Many α
| .none, ys => ys ()
| .more x xs, ys => .more x $ fun () => union (xs ()) ys

def Many.bind : Many α → (α → Many β) → Many β
| .none, _ => .none
| .more x xs, f => union (f x) (fun () => (bind (xs ()) f))

instance : Monad Many where
  pure := Many.one
  bind := Many.bind

def Many.take : Nat → Many α → List α
| 0, _ => []
| _+1, .none => []
| n+1, .more x xs => x :: take n (xs ())

def addsTo (goal : Nat) : List Nat → Many (List Nat)
| [] => if goal = 0 then Many.one [] else Many.none
| x::xs =>
  if x > goal then addsTo goal xs else
  Many.union
    (addsTo goal xs)
    (fun () => (x::·) <$> (addsTo (goal - x) xs))

#eval addsTo 15 (List.replicate 1000 1) |>.take 1

But I do not see how that helps with defining ManyT. Can you give further hints?

[Jakub Nowak]

I think ManyT m α := m (Many α) you proposed should work now with fixed Many. Does it not?

[Sebastian Miele]

Here is a complete definition of ManyT along that lines, including #evals at the end that demonstrate the resulting bind's non-assiciativeness.

universe u
variable {α β γ: Type u}

inductive Many (α : Type u) where
| none : Many α
| more : α → (Unit → Many α) → Many α

def Many.one (x : α) : Many α := .more x (fun () => .none)

def Many.union : Many α → (Unit → Many α) → Many α
| .none, ys => ys ()
| .more x xs, ys => .more x $ fun () => union (xs ()) ys

def Many.bind : Many α → (α → Many β) → Many β
| .none, _ => .none
| .more x xs, f => union (f x) (fun () => (bind (xs ()) f))

instance : Monad Many where
  pure := Many.one
  bind := Many.bind

def Many.fromList : List α → Many α
| [] => .none
| x::xs => .more x (fun () => (fromList xs))

def ManyT (m : Type u → Type v) (α : Type u) := m (Many α)

variable {m : Type u → Type v} [Monad m]
variable {α β γ : Type u}

def ManyT.run: ManyT m α → m (Many α) := id
def ManyT.mk : m (Many α) → ManyT m α := id

protected def ManyT.pure : α → ManyT m α
:= mk ∘ pure ∘ Many.one

def ManyT.bind : ManyT m α → (α → ManyT m β) → ManyT m β
| x, f => mk (run x >>= cont f)
where
cont (f : α → ManyT m β) : Many α → ManyT m β
| .none => mk do pure .none
| .more x xs => mk do
  let y₁ ← run (f x)
  let y₂ ← run (cont f (xs ()))
  pure (Many.union y₁ (fun () => y₂))

def ManyT.lift : m α → ManyT m α
| x => mk (x >>= pure ∘ Many.one)

def ManyT.fromList : List α → ManyT m α := mk ∘ pure ∘ Many.fromList

instance: Monad (ManyT m) where
  pure := ManyT.pure
  bind := ManyT.bind

instance: MonadLift m (ManyT m) where
  monadLift := ManyT.lift

variable {α : Type}

abbrev M := ManyT <| StateT (List Nat) <| Id

-- Runs the monad, starting with a state of `[]`, and returns only the
-- resulting state.
def M.run : M α → List Nat
| x => (Id.run <| StateT.run (ManyT.run x) []).snd

def log (n : Nat) : M Unit := modify (· ++ [n])

def x : M Nat         := .fromList [1, 2]
def f : Nat → M Unit  := log
def g : Unit → M Unit := (fun () => .fromList [10, 20] >>= log)

#eval M.run <| (x >>= f) >>= g
-- [1, 2, 10, 20, 10, 20]

#eval M.run <| x >>= (f · >>= g)
-- [1, 10, 20, 2, 10, 20]

As far as I can see, when defining ManyT m α := m (Many α), it does not matter how lazy Many is. The problem is the way it is encapsulated in the underlying monad m. That way, in (x >>= f) >>= g, the x >>= f must be finished completely before anything (and then all at once) can be passed to g.

I guess the x >>= (f · >>= g) example shows the only way it could be correct. But for (x >>= f) >>= g to produce the same result, ManyT must be some kind of iterator in m, so that binding x >>= f to g can run x >>= f "one element at a time" in m. Putting the whole Many in m fundamentally defeats this, as far as I can see.

[Derrik Petrin]

I too just got stuck on this one today, and am quite puzzled. Another approach I've tried is to define ManyT m α as Many (m α), but it does not appear possible to apply the f : ManyT m α in bind to the m α value at the head of the Many stream. In order to bind the m α value you need to be in the m monad, but then you cannot use f, as its return type is in the Many monad.

[Derrik Petrin]

A note about the discussion of union above, however. The original definition of union actually works lazily just fine. You can test this by running

#eval (count.union count).take 5

which should result in [0, 1, 2, 3, 4], and take no time at all. It does not try to fully compute the infinite stream.

The definition of bind in the book, however, does fail to operate lazily. The issue here is that the recursive call to bind is not happening lazily. If instead of union you use orElse, then bind works just fine. Of course, the lazy redefinition of union proposed above is in fact the same as the definition of orElse. :)

[Sebastian Miele]

Hi @Derrik Petrin, thanks for chiming in! Now I feel much less stupid and much more confident.

[Sebastian Miele]

Derrik Petrin said:

A note about the discussion of union above, however. The original definition of union actually works lazily just fine. You can test this by running

#eval (count.union count).take 5

which should result in [0, 1, 2, 3, 4], and take no time at all. It does not try to fully compute the infinite stream.

The definition of bind in the book, however, does fail to operate lazily. The issue here is that the recursive call to bind is not happening lazily. If instead of union you use orElse, then bind works just fine. Of course, the lazy redefinition of union proposed above is in fact the same as the definition of orElse. :)

I felt free to create https://github.com/leanprover/fp-lean/issues/247.

[Sebastian Miele]

Derrik Petrin said:

Another approach I've tried is to define ManyT m α as Many (m α), but it does not appear possible to apply the f : ManyT m α in bind to the m α value at the head of the Many stream. In order to bind the m α value you need to be in the m monad, but then you cannot use f, as its return type is in the Many monad.

Yes, I got stuck along that line, too.

[Sebastian Miele]

The rest of the book seems to not refer to ManyT. After having tried for quite some time, I'll just ignore this exercise for now, and move forward in the text. When in about a week no solution has popped up here I'll create another issue against https://github.com/leanprover/fp-lean.

[Jakub Nowak]

Derrik Petrin said:

A note about the discussion of union above, however. The original definition of union actually works lazily just fine. You can test this by running

The version of union from the book unnecessarily computes the first element if it's second Many argument, this only stacks with multiple recursive calls, like in addsTo implementation. But yeah, it doesn't try to compute whole lazy infinite lists.

[Derrik Petrin]

I found an article in the Haskell wiki that discusses essentially the same issue, concerning the original implementation of the non-lazy ListT. It corresponds to your above implementation of ManyT m α as m (Many α).

That version of ListT is essentially admitted to not be a proper monad transformer; in some cases the transformed monad is still a monad, and in other cases it is not. Part of the discussion in the article is the very non-associativity of bind that you demonstrate above:

ListT m is not associative (which is one of the monad laws), because grouping affects when side effects are run (which may in turn affect the answers).

I had to use an LLM to translate the Haskell to comparable Lean 4 code so that I could make better sense of it. The proposed monad transformer in that article is something like this:

inductive ManyT' (m : Type → Type) (α : Type) where
  | none
  | more (x : α) (xs : Unit → m (ManyT' m α))
abbrev ManyT (m : Type → Type) (α : Type) := m (ManyT' m α)

def ManyT.mk {m : Type → Type} {α : Type} (x : m (ManyT' m α)) : ManyT m α := x
def ManyT.run {m : Type → Type} [Functor m] {α : Type} (x : ManyT m α)
    : m (Option (α × ManyT m α)) :=
  (fun
    | .none => none
    | .more x xs => some (x, (xs ())))
  <$> x

def ManyT.none [Monad m] : ManyT m α :=
  ManyT.mk (pure ManyT'.none)
def ManyT.more [Monad m] (x : α) (xs : Unit → ManyT m α) : ManyT m α :=
  ManyT.mk (pure (ManyT'.more x xs))

However, as you noticed when trying something similar, Lean's type system doesn't allow this sort of definition. So it may be that a properly-behaved ManyT monad transformer is simply not admissible in Lean?

[Derrik Petrin]

Interestingly, the article mentions that:

There is a canonical distributive law when m is commutative — then ListT m is a monad.

Examples given of commutative monads are Reader and Option. If the book had introduced the concept of commutative monads, and a corresponding type class, the exercise could have asked the reader to construct a ManyT monad transformer whose Monad instance requires m to be commutative:

instance [CommutativeMonad m] : Monad (ManyT m) where
  ...

where CommutativeMonad is not an actual type class, but would contain a proof of commutativity, similar to how the LawfulMonad type class contains proofs of the monad contract.

Of course this would also make the following exercise no longer meaningful, since I believe State is not commutative.

[Derrik Petrin]

(By the way, I liked your straightforward approach to disproving the associativity by directly executing contradictory examples; my typical approach in proof assistant languages is to go straight for writing the proof, and only turning to executing examples once I've been banging my head for far too long. A welcome reminder that it's a good idea to do some computation with your objects to check their behavior before diving into proofs about them!)

[Derrik Petrin]

Jakub Nowak said:

The version of union from the book unnecessarily computes the first element if it's second Many argument, this only stacks with multiple recursive calls, like in addsTo implementation. But yeah, it doesn't try to compute whole lazy infinite lists.

Ah, I see what you're saying now! In the example I gave with counts, the evaluation goes as:

counts.union counts
 ==>
(more 0 fun () => counts 1).union (more 0 fun () => counts 1)

where the 0 in the second counts is produced prematurely.

This makes sense to me. orElse is supposed to be the monoidal append-like operator for the monad, and union should also correspond to the same monoidal operator, so it makes sense that their definitions should be the same.

[Sebastian Miele]

Derrik Petrin said:

(By the way, I liked your straightforward approach to disproving the associativity by directly executing contradictory examples; my typical approach in proof assistant languages is to go straight for writing the proof, and only turning to executing examples once I've been banging my head for far too long. A welcome reminder that it's a good idea to do some computation with your objects to check their behavior before diving into proofs about them!)

I wish I could claim that smartness. But I was able to think about and find counterexamples only after trying to prove the correctnes of a strict ListT m α := m (List α). The way the proof failed provided very clear insight into how and why it fails.

[František Silváši 🦉]

You can always throw a plausible at it as well.

[Sebastian Miele]

Sebastian Miele said:

When in about a week no solution has popped up here I'll create another issue against https://github.com/leanprover/fp-lean.

https://github.com/leanprover/fp-lean/issues/250.

[Derrik Petrin]

I'm going to make an attempt at defining the type using manual mutual inductive types rather than a nested inductive type, but I suspect it won't be possible. And even if it is, the characterization of the exercise as "less trivial than intended" is almost certainly accurate. :)

[Jakub Nowak]

It's possible to bypass Lean's termination checker to get the implementation from Haskell to work in Lean. For simplicity, I didn't make it lazy.

Code

inductive ManyT'G (m : Type → Type) (α : Type) (r : Type) : Type where
| none : ManyT'G m α r
| more (x : α) (xs : m r) : ManyT'G m α r

partial def ManyT' (m : Type → Type) (α : Type) : Type :=
  ManyT'G m α (ManyT' m α)

axiom ManyT'.eq : ManyT' m α = ManyT'G m α (ManyT' m α)

def ManyT (m : Type → Type) (α : Type) : Type :=
  m (ManyT' m α)

theorem ManyT.eq : ManyT m α = m (ManyT' m α) := by
  rfl

def ManyT'.none : ManyT' m α :=
  eq ▸ ManyT'G.none

def ManyT'.more (x : α) (xs : m (ManyT' m α)) : ManyT' m α :=
  eq ▸ ManyT'G.more x xs

instance : Nonempty (ManyT' m α) := .intro ManyT'.none

def ManyT.none [Monad m] : ManyT m α :=
  eq ▸ pure ManyT'.none

def ManyT.more' [Monad m] (x : α) (xs : ManyT m α) : ManyT m α :=
  eq ▸ return ManyT'.more x xs

def ManyT.more [Monad m] (x : m α) (xs : ManyT m α) : ManyT m α :=
  eq ▸ do more' (← x) xs

def ManyT.one' [Monad m] (x : α) : ManyT m α :=
  ManyT.more' x ManyT.none

def ManyT.one [Monad m] (x : m α) : ManyT m α :=
  ManyT.more x ManyT.none

partial def ManyT'.union [Monad m] (xs : ManyT' m α) (ys : m (ManyT' m α)) : m (ManyT' m α) :=
  match (eq ▸ xs) with
  | .none => ys
  | .more x xs => return .more x (do union (← xs) ys)

def ManyT.union [Monad m] (xs : ManyT m α) (ys : ManyT m α) : ManyT m α :=
  eq ▸ do ManyT'.union (← xs) ys

partial def ManyT'.bind [Monad m] (xs : ManyT' m α) (f : α → m (ManyT' m β)) : m (ManyT' m β) :=
  match (eq ▸ xs) with
  | .none => return .none
  | .more x xs => do union (← f x) (do bind (← xs) f)

def ManyT.bind [Monad m] (xs : ManyT m α) (f : α → ManyT m β) : ManyT m β :=
  eq ▸ do ManyT'.bind (← xs) f

instance [Monad m] : Monad (ManyT m) where
  pure := ManyT.one'
  bind := ManyT.bind

def ManyT.fromList [Monad m] : List α → ManyT m α
| [] => .none
| x :: xs => .more' x (fromList xs)

partial def ManyT'.run [Monad m] (xs : ManyT' m α) : m (List α) :=
  match (eq ▸ xs) with
  | .none => return []
  | .more x xs => return x :: (← run (← xs))

def ManyT.run [Monad m] (xs : ManyT m α) : m (List α) :=
  do ManyT'.run (← xs)

def ManyT.lift [Monad m] (x : m α) := ManyT.one x

instance [Monad m] : MonadLift m (ManyT m) where
  monadLift := ManyT.lift


abbrev M := ManyT <| StateT (List Nat) <| Id

-- Runs the monad, starting with a state of `[]`, and returns only the
-- resulting state.
def M.run : M α → List Nat
| x => (Id.run <| StateT.run (ManyT.run x) []).snd

def log (n : Nat) : M Unit := modify (· ++ [n])

def x : M Nat         := .fromList [1, 2]
def f : Nat → M Unit  := log
def g : Unit → M Unit := (fun () => .fromList [10, 20] >>= log)

#eval M.run <| (x >>= f) >>= g
-- [1, 10, 20, 2, 10, 20]

#eval M.run <| x >>= (f · >>= g)
-- [1, 10, 20, 2, 10, 20]

I should also mention that axiom ManyT'.eq : ManyT' m α = ManyT'G m α (ManyT' m α) is probably unsound (i.e. you can prove False from it).

Maybe it's possible to prove termination of ManyT' by tracking the length of the list?

[Jakub Nowak]

I managed to write the non-lazy implementation, though, I'm not certainly happy with how complicated it is. I'll appreciate it if someone manages to implement ManyT in simpler manner.

Code

import Mathlib

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd
| sup : (ι : Type) → (ι → VecOrd) → VecOrd

def VecT (m : Type → Type) (α : Type) : VecOrd → Type
| .zero => Unit
| .succ o => α × m (VecT m α o)
| .sup ι f => (i : ι) ×' m (VecT m α (f i))

structure ManyT (m : Type → Type) (α : Type) : Type 1 where
  { ord : VecOrd }
  val : m (VecT m α ord)

def VecT.none : VecT m α .zero :=
  ()

def ManyT.none [Monad m] : ManyT m α where
  val := pure .none

def VecT.more (x : α) (xs : m (VecT m α o)) : VecT m α o.succ :=
  ⟨x, xs⟩

def ManyT.more' [Monad m] (x : α) (xs : ManyT m α) : ManyT m α where
  val := pure <| .more x xs.val

def ManyT.more [Monad m] (x : m α) (xs : ManyT m α) : ManyT m α where
  val := return .more (← x) xs.val

def VecOrd.add : VecOrd → VecOrd → VecOrd
| zero, o₂ => o₂
| succ o₁, o₂ => succ <| add o₁ o₂
| sup ι f, o₂ => sup ι (fun i ↦ add (f i) o₂)

def VecT.union [Monad m] (xs : VecT m α o₁) (ys : m (VecT m α o₂)) : m (VecT m α (.add o₁ o₂)) :=
match o₁, xs with
| .zero, () => ys
| .succ .., ⟨x, xs⟩ => pure <| more x (do union (← xs) ys)
| .sup .., ⟨i, xs⟩ => pure ⟨i, do union (← xs) ys⟩

def VecOrd.sum : VecOrd → (α → VecOrd) → VecOrd
| zero, _ => zero
| succ o₁, f => sup α (fun x ↦ add (f x) (sum o₁ f))
| sup ι f', f => sup ι (fun i ↦ sum (f' i) f)

def VecT.bind [Monad m] (xs : VecT m α o₁) (f : α → VecOrd) (map : (x : α) → m (VecT m β (f x)))
    : m (VecT m β (.sum o₁ f)) :=
match o₁, xs with
| .zero, () => pure none
| .succ .., ⟨x, xs⟩ => pure ⟨x, do union (← map x) (do bind (← xs) f map)⟩
| .sup .., ⟨i, xs⟩ => pure ⟨i, do bind (← xs) f map⟩

def ManyT.bind [Monad m] (xs : ManyT m α) (map : α → ManyT m β) : ManyT m β where
  val := do VecT.bind (← xs.val) (fun a ↦ (map a).ord) (fun a ↦ (map a).val)

def VecT.run [Monad m] (xs : VecT m α o) : m (List α) :=
match o, xs with
| .zero, () => pure []
| .succ .., ⟨x, xs⟩ => return x :: (← run (← xs))
| .sup .., ⟨_, xs⟩ => do run (← xs)

def ManyT.run [Monad m] (xs : ManyT m α) : m (List α)
  := do VecT.run (← xs.val)

instance [Monad m] : Monad (ManyT m) where
  pure x := .more' x .none
  bind := .bind

instance [Monad m] : MonadLift m (ManyT m) where
  monadLift x := .more x .none

def ManyT.fromList [Monad m] : List α → ManyT m α
| [] => .none
| x :: xs => .more' x (fromList xs)


variable {α : Type}

abbrev M := ManyT <| StateT (List Nat) <| Id

-- Runs the monad, starting with a state of `[]`, and returns only the
-- resulting state.
def M.run : M α → List Nat
| x => (Id.run <| StateT.run (ManyT.run x) []).snd

def log (n : Nat) : M Unit := modify (· ++ [n])

def x : M Nat         := .fromList [1, 2]
def f : Nat → M Unit  := log
def g : Unit → M Unit := (fun () => .fromList [10, 20] >>= log)

#eval M.run <| (x >>= f) >>= g
-- [1, 10, 20, 2, 10, 20]

#eval M.run <| x >>= (f · >>= g)
-- [1, 10, 20, 2, 10, 20]

[Jakub Nowak]

Derrik Petrin said:

the characterization of the exercise as "less trivial than intended" is almost certainly accurate. :)

Maybe the exercise meant to implement the non-lawful version of ManyT?

[Derrik Petrin]

Construct a monad transformer ManyT based on the definition of Many, with a suitable Alternative instance. Check that it satisfies the Monad contract.

Nope! It certainly asks the reader to prove it is lawful.