PIL state monad

Stream: new members

[cbailey]

Can anyone provide an example of how to properly define an instance of the state monad in Lean? I'm having trouble figuring out how exactly Lean wants it. The examples in Programming in Lean seem to have outdated definitions of read/write and no longer work.

[Patrick Massot]

What do you mean "define an instance"? state is not a class

[Patrick Massot]

What do you actually want to do?

[Patrick Massot]

For instance, what is the part of PIL (which is indeed outdated) that you'd like to get to work?

[Patrick Massot]

I just had a quick look at section 7.3 of PIL called "The state monad" and I'm confused because it doesn't seem to use anything, it builds everything from scratch. The equivalent of the example at the end using Lean core library is:

def read_x : state (ℕ × ℕ × ℕ) ℕ :=
do s ← get,
   return s.1

def read_y : state (ℕ × ℕ × ℕ) ℕ :=
do s ← get,
   return s.2.1


def read_z : state (ℕ × ℕ × ℕ) ℕ :=
do s ← get,
   return s.2.2

def write_x (n : ℕ) : state (ℕ × ℕ × ℕ) unit :=
do s ← get,
   put (n, s.2.1, s.2.2),
   return ()

def write_y (n : ℕ) : state (ℕ × ℕ × ℕ) unit :=
do s ← get,
   put (s.1, n, s.2.2),
   return ()

def write_z (n : ℕ) : state (ℕ × ℕ × ℕ) unit :=
do s ← get,
   put (s.1, s.2.1, n),
   return ()

def foo : state (ℕ × ℕ × ℕ) ℕ:=
do write_x 5,
   write_y 7,
   x ← read_x,
   write_z (x + 3),
   y ← read_y,
   z ← read_z,
   write_y (y + z),
   y ← read_y,
   return (y + 2)

#reduce foo.run (0, 0, 0)

[Patrick Massot]

No I'm wrong, it does hide a use of the library state in the middle

[Patrick Massot]

Hold on, I'll update my update

[Rob Lewis]

For any type σ, state σ is the state monad where the state is of type σ. If m is a monad, state_t σ m is the monad that augments m with additional state. If you define my_monad := state (ℕ × ℕ × ℕ), you should either make it reducible or explicitly define the monad instance (using state_t.monad).

[Patrick Massot]

structure registers : Type := (x : ℕ) (y : ℕ) (z : ℕ)

def init_reg : registers := registers.mk 0 0 0

@[reducible] def reg_state := state registers

def read_x : reg_state ℕ :=
do s ← get, return (registers.x s)

def read_y : reg_state ℕ :=
do s ← get, return (registers.y s)

def read_z : reg_state ℕ :=
do s ← get, return (registers.z s)

def write_x (n : ℕ) : reg_state unit :=
do s ← get,
   put (registers.mk n (registers.y s) (registers.z s))

def write_y (n : ℕ) : reg_state unit :=
do s ← get,
   put (registers.mk (registers.x s) n (registers.z s))

def write_z (n : ℕ) : reg_state unit :=
do s ← get,
   put (registers.mk (registers.x s) (registers.y s) n)


def foo : reg_state ℕ:=
do write_x 5,
   write_y 7,
   x ← read_x,
   write_z (x + 3),
   y ← read_y,
   z ← read_z,
   write_y (y + z),
   y ← read_y,
   return (y + 2)

#reduce foo.run ( registers.mk 0 0 0)

[Patrick Massot]

This is the updated example. Basically read was renamed get and write was renamed put

[Patrick Massot]

Note that you can also replace all those explicit calls to register.mk by the angle bracket anonymous constructor notation

[Patrick Massot]

structure registers : Type := (x : ℕ) (y : ℕ) (z : ℕ)

def init_reg : registers := ⟨0, 0, 0⟩

@[reducible] def reg_state := state registers

def read_x : reg_state ℕ :=
do s ← get, return (registers.x s)

def read_y : reg_state ℕ :=
do s ← get, return (registers.y s)

def read_z : reg_state ℕ :=
do s ← get, return (registers.z s)

def write_x (n : ℕ) : reg_state unit :=
do s ← get,
   put ⟨n, registers.y s, registers.z s⟩

def write_y (n : ℕ) : reg_state unit :=
do s ← get,
   put ⟨registers.x s, n, registers.z s⟩

def write_z (n : ℕ) : reg_state unit :=
do s ← get,
   put ⟨registers.x s, registers.y s, n⟩


def foo : reg_state ℕ:=
do write_x 5,
   write_y 7,
   x ← read_x,
   write_z (x + 3),
   y ← read_y,
   z ← read_z,
   write_y (y + z),
   y ← read_y,
   return (y + 2)

#reduce foo.run init_reg

[cbailey]

Ah, that's a huge help, thank you. I guess 'the idiomatic way of defining a monad for (s -> (a x s))' is the goal. I spent a bunch of time trying to create a state_t instance and when I eventually satisfied it, I got 'state_t is not a class' which was unfortunate.

[cbailey]

The error from the renaming of 'read' and 'get' is what originally sent me down the rabbit hole.

[Kevin Buzzard]

Yes, unfortunately Programming In Lean needs a major update so that the code actually runs in Lean 3.4.2. I would imagine that PR's fixing chunks of it would be welcome! (but I can't remember where the repo is :-/ )

[Patrick Massot]

Simon and Jerery are working on it

[cbailey]

The github page for PIL 404s and it's not listed on the lean website anymore :working_on_it:

[Mario Carneiro]

https://github.com/avigad/programming_in_lean

[Mario Carneiro]

it got relocated approximately the same time as mathlib's relocation

[cbailey]

Thanks! I made a pull request with the changes suggested by @Patrick Massot

[Koundinya Vajjha]

@cbailey could you link your PR? I am interested in seeing this

[cbailey]

@Koundinya Vajjha https://github.com/avigad/programming_in_lean/pull/1#issue-257237337

[cbailey]

Sorry to resurrect this, but is there any particular reason why the registers example fails to evaluate when nat is replaced with string or char? Reduced example:

structure registers : Type := (x : string) (y : string) (z : string)

def init_reg : registers := ⟨"a", "b", "c"⟩

@[reducible] def reg_state := state registers

def read_x : reg_state string :=
do s ← get, return (registers.x s)

def foo : reg_state string :=
do s ← read_x,
       return s

#reduce foo.run init_reg
/-
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)
-/

[Rob Lewis]

Yes, #reduce means kernel normalization. Chars (and thus strings) include proofs of inequalities over nat, reducing them produces huge proof terms. You should use #eval instead (and you'll need to make a has_repr instance for registers).

[cbailey]

I see, thank you. Is that because of the field on character structs showing that their value is in the correct character id range? I still had quite a struggle getting it to work; I had to import system.io and define a reader from id (string × registers) to io unit to finally get #eval to display it properly.

def rho : (string × registers) → io unit
| (a, b) := put_str (repr b)

def reg_reader := reader_t.mk rho

#eval (reg_reader.run (foo.run init_reg))

[Rob Lewis]

Yes, that's why. If you reduce char.val a, you're asking Lean to normalize a proof that 97 < 55296, which is approximately 55200 nested applications.

[Rob Lewis]

There's definitely no need to touch io. In this case, there's an annoying hiccup with id not reducing, but it's not bad.

structure registers : Type := (x : string) (y : string) (z : string)

instance : has_repr registers :=
⟨λ r, "⟨" ++ r.x ++ ", " ++ r.y ++ ", " ++ r.z ++ "⟩"⟩

instance {α : Type*} [has_repr α] : has_repr (id α) := by dsimp; apply_instance

def init_reg : registers := ⟨"a", "b", "c"⟩

@[reducible] def reg_state := state registers

def read_x : reg_state string :=
do s ← get, return (registers.x s)

def foo : reg_state string :=
do s ← read_x,
       return s

#eval foo.run init_reg

[cbailey]

Ah yeah, that's definitely a better way of doing it. Is there any reason for using Type* instead of just Type in the instance declaration?

[Rob Lewis]

It's more general and it doesn't hurt, that's all.