monadic side-computation

Stream: new members

[Rob Simmons]

This is mostly an unfamiliarity-with-monad-y-functional programming question.

inductive Tree where
| node : String → Tree → Tree → Tree
| leaf : Tree

def height
| Tree.leaf => 0
| Tree.node _str t1 t2 => Nat.max (height t1) (height t2)

If I want height to return a "side computation" that is a HashSet of all the strings in the tree — I think the return type would be something like State (HashSet String) Nat instead of Nat — what's the right/idiomatic way to go about that?

[Aaron Liu]

docs#StateM

[Aaron Liu]

also don't use Nat.max

[Aaron Liu]

you should just write max instead

[Rob Simmons]

Right, the max was just a standin for what I'm really doing

[Rob Simmons]

interesting — the state monad does more than I actually want; it allows reads and writes (sequentalizing computation) — there's a read-only specialization of state and a write-only specialization of state that are conceptually more "parallel" — this is maybe Appliciative in Haskell? — but is that not Lean-standard style?

[Aaron Liu]

docs#ReaderM
docs#Writer

[Aaron Liu]

there's also the monad transformer versions if you want to add functionality to an existing monad

[Rob Simmons]

Okay, so with StateT it looks like this is the move, am I missing any idiomatic improvments?

import Std.Data.HashSet
open Std

inductive Tree where
| node : String → Tree → Tree → Tree
| leaf : Tree

def height : Tree → StateM (HashSet String) Nat
| Tree.leaf => pure 0
| Tree.node str t1 t2 => do
  let _ ← set (HashSet.insert (← get) str)
  Nat.max <$> height t1 <*> height t2

[Aaron Liu]

import Std.Data.HashSet
open Std

inductive Tree where
| node : String → Tree → Tree → Tree
| leaf : Tree

def height : Tree → StateM (HashSet String) Nat
| Tree.leaf => pure 0
| Tree.node str t1 t2 => do
  modify fun s => s.insert str
  max <$> height t1 <*> height t2

[Aaron Liu]

it makes sure you avoid copying the hash set

[Rob Simmons]

thank you!