A minimal state monad?

Stream: new members

[Eduardo Ochs]

Hi all,

I am trying to write minimal versions of some of the examples from FPiL, and this is an attempt to build a minimal state monad without using the monad transformers from this section:

universe u
universe v

def S (α : Type u) : Type u := String × α   -- "S" stands for both "State" and "String"

instance : Monad S where                    -- or just: bind sa f := ...
  pure o := ⟨"", o⟩
  bind {α : Type u} {β : Type u}
       (sa : S α) (f : α → S β) : S β :=
    let state := sa.fst
    let a     := sa.snd
    ⟨state, (f a).snd⟩

#check                   do return 42
#check show S Nat from   do return 42
#eval  show S Nat from   do return 42

Now how do I add "get" and "set" methods to S? In theory it should be possible to do that either by making S an instance of MonadState or by making S an instance of a new class with methods "get" and "set"... the answer should be trivial, but I can't get the syntax right... :cry:

[Henrik Böving]

What you have there is not a state monad, the state monad with a string as state is defined through def S (a : Type) : Type := String -> Prod String a, you are missing the input string parameter.

[Eduardo Ochs]

Fixed - but now both instance : Monad S where and instance : Monad (S α) where give errors. Try:

universe u
universe v

def S (α : Type) : Type := String → String × α   -- "S" stands for both "State" and "String"

-- instance : Monad S where      -- invalid fields and constructors
instance : Monad (S α) where     -- application type mismatch
  pure o := ⟨"", o⟩
  bind ma f :=
    let state := ma.fst
    let a     := ma.snd
    ⟨state, (f a).snd⟩

#check                   do return 42
#check show S Nat from   do return 42
#eval  show S Nat from   do return 42

[Henrik Böving]

it needs to be instance : Monad S and you need to put a bit more effort into writing your pure and bind than what you currently have

[Eduardo Ochs]

I'll try! Thanks! =)