Best practices for global state in libraries

Stream: lean4

[Kiran]

I'm currently playing around with writing a library. As part of this library I'd like to have some global state that my functions will make use of. Naturally then, I suppose I must use a state monad, but as I'd like my library to be general and composable with client code making use of other monads, I'll have to use a StateT monad transformer?

I'm a little new to monad transformers as I haven't used them before. I've put together the following that kinda works, but it fails to typecheck if I don't appropriately annotate certain terms:

-- Library Code

-- Some Global State, A counter
structure GlobalState where
   counter: Nat
deriving Inhabited

abbrev GlobalStateT M V := StateT GlobalState M V

namespace GlobalState

def run {M T} [Monad M] (d: GlobalStateT M T) : M T := d |>.run default |> Functor.map (fun ⟨v,_⟩ => v)

def incr {M} [Monad M] : GlobalStateT M Unit := do
   let data <- get
   set {data with counter := data.counter + 1}
   return

def counter_value {M} [Monad M] : GlobalStateT M Nat := do
   let data <- get
   return data.counter

end GlobalState


-- Client code
-- User decides to define their own String state
abbrev StringDataT M := StateT String M
namespace StringData
def run {M T} [Monad M] (d: StringDataT M T) : M T := do
    let ⟨res, _⟩ <- StateT.run d default
    return res
end StringData

def getString {M} [Monad M] : StringDataT M String := do
    let s <- get
    return s


-- client code, using
def main : IO Unit := GlobalState.run $ StringData.run do
   GlobalState.incr -- fails to typecheck unless I add a type annotation
   let data <- GlobalState.counter_value
   let s <- getString
   return

What am I doing wrong? Is this the correct model of what I should expect client code to look like? am I missing some instances?
Thanks!

[Kim Morrison]

Just to clarify here, GlobalState.incr fails with

type mismatch
  GlobalState.incr
has type
  GlobalStateT ?m.1859 Unit : Type ?u.1858
but is expected to have type
 StringDataT (GlobalStateT IO) PUnit : Type

and the type annotation that succeeds is show GlobalStateT IO Unit from GlobalState.incr. I'd also like to know if there is a better way!

[Kiran]

sorry if this question is too simple, I am a beginner and quite unfamiliar to idiomatic uses of monad transformers. I would really appreciate any help.

From looking at code online, I guess the best way of doing it is using MonadStateOf?

structure GlobalState where
  counter: Nat
deriving Inhabited

namespace GlobalState
  @[always_inline]
  instance [Monad M] [MonadStateOf GlobalState M] : MonadStateOf Nat M where
    get
      := do let self <- get
            pure self.counter
    set counter
      := do let self <- get
            set { self with counter }
    modifyGet f
      := do let self <- get
            let (out, counter) := f self.counter
            set { self with counter }
            pure out
end GlobalState


class Global (M: Type -> Type)
  extends
    Monad M,
    MonadStateOf GlobalState M
  where

namespace Global
  @[always_inline, inline]
  def getState [Global M]: M GlobalState
    := MonadStateOf.get

  @[always_inline, inline]
  def getCounter [Global M] : M Nat
    := do let self <- get
          return self.counter

  @[always_inline, inline]
  def incrCounter [Global M] : M Unit
    := do let self <- get
          set {self with counter := self.counter + 1}

  @[always_inline]
  instance CanonicalInstance [Monad M] [MonadStateOf GlobalState M] : Global M where

  @[always_inline]
  instance LiftInstance [Monad M] : MonadLift M (StateT GlobalState M) where
    monadLift f := (StateT.lift f)

end Global


namespace GlobalState
  @[always_inline, inline]
  def run [Monad M]  (f: {M': Type -> Type} -> [Global M'] -> [MonadLift M M'] -> M' X): M (X × GlobalState)
  := StateT.run f  (default : GlobalState)

  @[always_inline, inline]
  def run' [Monad M] (f: {M': Type -> Type} -> [Global M'] -> [MonadLift M M'] -> M' X): M X
    := StateT.run' f (default : GlobalState)
end GlobalState

This seems to do what I want, and seems to be composable with other monad transformers, but I wonder if it's overkill?

[Mario Carneiro]

I think the issue with GlobalState.incr is usually solved in lean core by having a typeclass for monads that extend GlobalStateT

[Kiran]

Kim Morrison said:

Just to clarify here, GlobalState.incr fails with

type mismatch
  GlobalState.incr
has type
  GlobalStateT ?m.1859 Unit : Type ?u.1858
but is expected to have type
 StringDataT (GlobalStateT IO) PUnit : Type

and the type annotation that succeeds is show GlobalStateT IO Unit from GlobalState.incr. I'd also like to know if there is a better way!

Yep, this is exactly the problem I'm having. I can kinda see that lean is having some kinof difficulty working out that ?m.1859 should be IO and then invoking monadLift, but I don't quite have a good enough model of what exactly's going on to understand why this inference is failing, and like where the annotation overhead should be placed in terms of clients vs. libraries

[Mario Carneiro]

A MonadStateOf Nat instance is a bad idea, that type is too general and will cause conflicts with other state monads in the stack

[Kiran]

Mario Carneiro said:

I think the issue with GlobalState.incr is usually solved in lean core by having a typeclass for monads that extend GlobalStateT

ah, so could I ask for like user defined libraries, what would be the recommendation of the way to composably define like global state? or do I just have to tell clients of my library that they may need to add annotations?

[Mario Carneiro]

this also works with MonadLift like so:

class MonadEnv (m : Type → Type) where
  getEnv    : m Environment
  modifyEnv : (Environment → Environment) → m Unit

export MonadEnv (getEnv modifyEnv)

@[always_inline]
instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
  getEnv    := liftM (getEnv : m Environment)
  modifyEnv := fun f => liftM (modifyEnv f : m Unit)

[Mario Carneiro]

no annotations are needed

[Kiran]

Mario Carneiro said:

this also works with MonadLift like so:

could you give an example of what the client code using it would look like? I'm going to try it out now, but if you have it off the top of your head, that might be faster.

[Mario Carneiro]

this basically just works

structure GlobalState where
   counter: Nat
deriving Inhabited

abbrev GlobalStateT M V := StateT GlobalState M V

namespace GlobalState

def run {M T} [Monad M] (d: GlobalStateT M T) : M T := d |>.run default |> Functor.map (fun ⟨v,_⟩ => v)

def incr {M} [Monad M] [MonadStateOf GlobalState M] : M Unit := do
   let data ← get
   set {data with counter := data.counter + 1}
   return

def counter_value {M} [Monad M] [MonadStateOf GlobalState M] : M Nat := do
   let data ← get
   return data.counter

end GlobalState


-- Client code
-- User decides to define their own String state
abbrev StringDataT M := StateT String M
namespace StringData
def run {M T} [Monad M] (d: StringDataT M T) : M T := do
    let ⟨res, _⟩ ← StateT.run d default
    return res
end StringData

def getString {M} [Monad M] : StringDataT M String := do
    let s ← get
    return s


-- client code, using
def main : IO Unit := GlobalState.run $ StringData.run do
   GlobalState.incr
   let data ← GlobalState.counter_value
   let s ← getString
   return

[Mario Carneiro]

from what I've seen of lean core metaprogramming though, it's pretty rare for a library to provide a monad transformer instead of just a monad of its own

[Mario Carneiro]

you would need whatever your core algorithm is to depend on user code in the wrapped monad for it to be worth it

[Mario Carneiro]

I think in general you would want to avoid that, in the same way that in haskell you try to avoid having your whole program live in IO if you can do most of the work in pure functions

[Mario Carneiro]

carrying around additional user state everywhere is just overhead if you aren't doing anything with it

[Kiran]

Ahh, thanks thanks, this works exactly! So I guess the recommended way is to use MonadStateOf with a specific enough type that it doesn't clash with other things.

In my case, this isn't for a metaprogramming application, but a (non-metaprogramming, non-proof related) lean library , I just want the library to have some global state that gets manipulated over time without constraining the user to a particular monad stack.

[Mario Carneiro]

also, if you want literally global state you can also use initialize

[Mario Carneiro]

I know you aren't asking about metaprogramming, but a lot of the issues and design questions around library design for programming in lean have already come up in lean core somewhere because it's a big compiler program with several identifiable subcomponents that service each other and user code

[Mario Carneiro]

The MonadEnv approach can be thought of as a slightly more specific version of MonadStateOf Environment, which avoids the issues with clashing types, shortens the name, and hides more implementation details around what state you are tracking

[Kiran]

Sorry my monad programming is a little rusty, but at least for the example I've given above, with the mix of a user defined string state monad and the library's global state, isn't the monad transformer the most ergonomic way to ensure that both can be composed?

[Kiran]

Mario Carneiro said:

The MonadEnv approach can be thought of as a slightly more specific version of MonadStateOf Environment, which avoids the issues with clashing types, shortens the name, and hides more implementation details around what state you are tracking

Ahh, okay, I guess I'll use the MonadEnv approach instead. You mentioned that MonadStateOf Nat would clash with other monads in the stack --- I guess that's because Nat is a generic enough type that if the client were also using this encoding, then they might also add instances for MonadStateOf Nat leading to conflicts? or are there parts of vanilla lean even that would clash with this?

[Mario Carneiro]

maybe? The code doesn't really do anything so it's difficult to say if this is the best way to accomplish the goal

[Mario Carneiro]

Yes you understood my point about MonadStateOf Nat correctly. The kind of data hiding that MonadStateOf MyType still lacks is that this is a state monad and not a reader or exception monad etc

[Mario Carneiro]

the MonadEnv approach lets you decide what functions you actually need for the implementation, and it need not even be public API to construct an instance

[Kiran]

awesome, thanks for the advice! I think I kinda understand how to best monadically encode global state for a library