How to make custom state monad

Stream: lean4

[Ian Benway]

I'm asking this kind of naively, but looking at some Lean 3 code, I'm thinking I should be able to do something like

structure myStruct : Type :=
(var1 : Nat)
(var2 : Nat)

def CoolM : Type → Type :=
StateT myStruct (ExceptT Nat id)

and then I'm hoping to use it like

def getVar1 : CoolM Nat := do
  CoolM.var1 (← get)

or something like that. I get an error on the do saying it can't tell that CoolM is a monad. What would a custom state monad like this look like?

[Henrik Böving]

The issue here is that you are using def, defs are not transparent to type class synthesis, meaning that when searching for an instance Moand CoolM Lean will not attempt to unfold CoolM but instead only check whether this instance exists right away which is not the case, what you want to do is use abbrev instead of def which does allow this behaviour (it essentially boils down to tagging the def with @[reducible])

[Henrik Böving]

And just style wise, the usual way we write types right now is CamelCase, variables and functions lowerCamelCase and proofs snek_case. The style for declaring structures also changed to:

structure MyStruct where
  var1 : Nat
  var2 : Nat

[Ian Benway]

Ah I see what you're saying about defs. I'm still getting this error on the do, though. Do I have to specify that CoolM is a monad, maybe using derives?
Screen-Shot-2022-04-27-at-7.11.30-PM.png

[Henrik Böving]

No, there is one more thing, you are using id here which is the identity function but what you actually want is the Id identity monad, this is what's blocking Lean from finding the instance.

[Henrik Böving]

structure MyStruct where
  x : Nat
  y : Nat
abbrev CoolM := StateT MyStruct (ExceptT Nat Id)
#synth Monad CoolM

[Ian Benway]

Oh that's funny, but I see why it makes sense. Thank you!