Zulip Chat Archive

Stream: new members

Topic: PIL state monad


cbailey (Feb 28 2019 at 11:41):

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 (Feb 28 2019 at 11:56):

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

Patrick Massot (Feb 28 2019 at 11:56):

What do you actually want to do?

Patrick Massot (Feb 28 2019 at 11:59):

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

Patrick Massot (Feb 28 2019 at 12:17):

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 (Feb 28 2019 at 12:18):

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

Patrick Massot (Feb 28 2019 at 12:20):

Hold on, I'll update my update

Rob Lewis (Feb 28 2019 at 12:21):

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 (Feb 28 2019 at 12:23):

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 (Feb 28 2019 at 12:24):

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

Patrick Massot (Feb 28 2019 at 12:25):

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

Patrick Massot (Feb 28 2019 at 12:26):

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 (Feb 28 2019 at 12:28):

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 (Feb 28 2019 at 12:29):

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

Kevin Buzzard (Feb 28 2019 at 12:44):

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 (Feb 28 2019 at 12:48):

Simon and Jerery are working on it

cbailey (Feb 28 2019 at 12:51):

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

Mario Carneiro (Feb 28 2019 at 15:21):

https://github.com/avigad/programming_in_lean

Mario Carneiro (Feb 28 2019 at 15:22):

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

cbailey (Feb 28 2019 at 21:38):

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

Koundinya Vajjha (Feb 28 2019 at 21:43):

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

cbailey (Mar 01 2019 at 08:17):

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

cbailey (Mar 01 2019 at 11:02):

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 (Mar 01 2019 at 11:46):

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 (Mar 01 2019 at 14:55):

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 (Mar 01 2019 at 15:33):

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 (Mar 01 2019 at 15:34):

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 (Mar 01 2019 at 16:00):

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 (Mar 01 2019 at 16:08):

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


Last updated: Dec 20 2023 at 11:08 UTC