Reader Monad porting

Stream: lean4

[Chris Lovett]

Porting https://mmhaskell.com/monads/reader-writer it talks about calling a monad from "pure code" where it calls readerFunc1 and readerFunc2 and so on pure code, do we call these monadic functions pure code or does the monad make it impure? What is the definition of pure code ?

def readerFunc1 : Reader Environment Float := do
  let env ← read
  let l1 := env.path.length
  let l2 := env.home.length * 2
  let l3 := env.user.length * 3
  return (l1 + l2 + l3).toFloat * 2.1

def readerFunc2 : Reader Environment Nat := do
  let f ← readerFunc1 |>.run
  return 2 + f.floor.toUInt32.toNat

def readerFunc3 : Reader Environment String := do
  let n ← readerFunc2 |>.run
  return "Result: " ++ (toString n)

def main2 : IO Unit := do
  let env ← loadEnv
  let str := readerFunc3 |>.run env
  IO.println str

[Mario Carneiro]

The term "pure code" is not rigorously defined, and I would say it is a matter of perspective. It generally means code that does not have "side effects" or refers to "external state", and whether the state in a Reader is considered external depends on your point of view. The only monad I would say is unambiguously impure is IO; most others are built out of pure pieces so you can deconstruct it into a pure function of some kind

[Chris Lovett]

Thanks, I will consider all these then to be pure, except the main and loadEnv functions which uses IO.

[Chris Lovett]

Porting https://mmhaskell.com/monads/state looks like Haskell has associative arrays, what is the best replacement in Lean, I found HashMap... ?

[Mario Carneiro]

I don't see HashMap on that page

[Mario Carneiro]

Lean has a HashMap type

[Chris Lovett]

sorry my bad typo, I meant to say haskell is using A.Array, and so sounds like HashMap is the way to go - thanks. Also do you know how to initialize the lean random generator with a good random seed (like current tick count or something) ?

def fred : IO Unit := do
  let gen ← IO.stdGenRef.get
  let (x, gen) := randNat gen 0 100
  IO.println x
  let (x, gen) := randNat gen 0 100
  IO.println x
  let (x, gen) := randNat gen 0 100
  IO.println x

#eval fred

Right now fred is very boring:

48
29
28

[Mario Carneiro]

If you are talking about A.Array:

• Lean does not have a type like A.Array i a, which allows you to choose your own indexing type. In the example it's using it to make a 2D array. IIRC @Tomas Skrivan has a mechanism for doing n-D arrays with a generic indexing type.
• The nearest equivalent to the A.array function is Array.ofFn, which I can't find but I thought @Gabriel Ebner had an implementation somewhere in mathlib4
• A.assocs is similar to Array.toList, but we should have a version that returns the indexes too.
• A.// is just Array.set iterated

[Mario Carneiro]

fred works at the command line, but IO.stdGenRef is deterministic in interactive mode

[Chris Lovett]

But this works right?

def initBoard :HashMap TileIndex TileState :=
  HashMap.ofList [((0,0), TileState.HasX), ((0,1), TileState.HasO), ((0,2), TileState.HasX) ...]

#eval initBoard.find? (0,0)   -- some (TileState.HasX)

#eval (initBoard.insert (0,0) TileState.Empty).find? (0,0)    -- some (TileState.Empty)

[Mario Carneiro]

yes, you could also do map.findD i .Empty to get a default value out of range

[Chris Lovett]

Also seems Haskell has list comprehensions let openSpots = [ fst pair | pair <- A.assocs (board game), snd pair == Empty] what's the easiest way to implement that on HashMap ?

[Chris Lovett]

Well this isn't too bad I suppose:

def findOpen (board: HashMap TileIndex TileState) : List TileIndex :=
  let i := board.toList.map (λ (x: TileIndex × TileState) => if x.2 == TileState.Empty then x.1 else (5,5))
  i.filter (λ x: TileIndex => x ≠ (5,5))

[Mario Carneiro]

you could do this:

def findOpen (board: HashMap TileIndex TileState) : List TileIndex :=
  board.toList.filterMap fun (i, x) => guard (x == TileState.Empty) *> pure i

[Mario Carneiro]

with a monad instance on List you can do this:

instance : Monad List where
  pure := List.pure
  bind := List.bind

instance : Alternative List where
  failure := []
  orElse a b := a.append (b ())

def findOpen (board : HashMap TileIndex TileState) : List TileIndex := do
  let (i, x) ← board.toList
  guard (x == TileState.Empty)
  pure i

[Mario Carneiro]

which is the nearest thing we have to list comprehensions

[Chris Lovett]

Cool - I will steal some of this and include it in my section on States: https://github.com/leanprover/lean4/pull/1505/files
It also is a great example of seqRight, which I can use in applciatives.lean, so thanks for that too.

PS: it is curious that "Option" is the option monad, "Reader" is the reader monad, but "StateM" is the state monad... why the naming difference?

[Mario Carneiro]

Because State collides with too many other things. In particular, it is conventional, when the local monad FooM is a ReaderT on top of a StateT, to call the state object Foo.State and the reader object Foo.Context. For example, CoreM, MetaM, TermElabM, TacticM, CommandElabM all follow this pattern

[Mario Carneiro]

Note that the option monad used to be called OptionM back when there was a reason to keep it separate from Option

[Mario Carneiro]

There are a whopping 64 hits for structure State in the lean 4 codebase (and 50 hits for structure Context)

[Mario Carneiro]

In other words, the M is not a requirement in the naming convention for monads, but it is used for disambiguation when something else has the short name

[Chris Lovett]

Ok, makes sense, one last question to flip it around, if there is a pretty consistent naming convention around adding "M" to the monad class name, why not make it ReaderM ? I understand why Option and List would no go there because those have a life outside of monads, whereas the Reader doesn't really... and it could easily clash with "streaming" classes which is what I assumed it was originally before I learned what it really was... I'd almost like "ReadStateM" better or something...

[Sebastian Ullrich]

Yes, I think ReaderM would be more consistent. It's not used anywhere in core anyway, we can rename it.

[Patrick Massot]

I also wondered why Reader was not ReaderM.

[Henrik Böving]

Most likely because Haskell doesn't do the M suffix here either