Puzzled by MonadState and Pure

Stream: new members

[Nicolas Rouquette]

Lean4 has an interesting implementation of strongly connected components in Util/SCC.lean that begins like this:

import Std.Data.HashMap
namespace Lean.SCC
/-
  Very simple implementation of Tarjan's SCC algorithm.
  Performance is not a goal here since we use this module to
  compiler mutually recursive definitions, where each function
  (and nested let-rec) in the mutual block is a vertex.
  So, the graphs are small. -/
open Std

section
variable (α : Type) [BEq α] [Hashable α]

structure Data where
  index?   : Option Nat := none
  lowlink? : Option Nat := none
  onStack  : Bool       := false

structure State where
  stack     : List α := []
  nextIndex : Nat := 0
  data      : Std.HashMap α Data := {}
  sccs      : List (List α) := []

abbrev M := StateM (State α)
end

variable {α : Type} [BEq α] [Hashable α]

private def getDataOf (a : α) : M α Data := do
  let s ← get
  match s.data.find? a with
  | some d => pure d
  | none   => pure {}

When I read getDataOf, it is unclear to me how this code typechecks properly.
VSCode seems to have determined somehow that M is an instance of MonadState
so that get is really MonadState.get and that M is also an instance of Pure so that pure is really Pure.pure.

Can someone explain this?

It would be really nice if the VS Code tooling could explain what makes a reference resolve the way it does and why some code typechecks properly.

[Kyle Miller]

Here's the instance definition for StateM being a MonadStateOf (which gives MonadState by another instance). Click "source" to the right to see where it is inside the prelude.

[Kyle Miller]

These docs also have lists of instances when you go to a class, so that can help you find where things are actually defined.

[Matt Diamond]

VSCode seems to have determined somehow that M is an instance of MonadState

My guess is that the determination is based on abbrev M := StateM (State α)

[Kyle Miller]

It's helpful to know some Haskell to be able to deal with this part of the library, since it's still rather light on documentation, and these are all Haskell-like idioms.

[Chris Bailey]

I think it's just typeclass inference. StateT has an instance of MonadStateOf, which is MonadState where the state type is set as an output parameter.

[Chris Bailey]

Oh they beat me to it.

[Kyle Miller]

The point of StateM is that you can use get to get the "current" State α value and then put to change it for code that runs "after." It's a functional programming trick to get something like mutable state.

[Chris Bailey]

There are some spartan trace facilities, like set_option trace.Meta.synthInstance and some other ones discoverable via autocomplete if you type set_option trace.

[Kyle Miller]

Concretely, StateM is a way to concisely write code for functions that have types like σ → α × σ, where σ is the type for some state that you'd otherwise have to thread through everything manually.

[Kyle Miller]

(Making things more complicated, StateM is defined in terms of StateT, a so-called "monad transformer," where you can compose multiple monad transformers to achieve multiple effects.)