Steps to take to replace StateT with StateRefT

Stream: new members

[Kevin Cheung]

From this message https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Manipulating.20custom.20tactic.20state/near/357172828, I got the impression that StateRefT can be a drop-in replacement for StateT. But I think I'm missing something. For example, I replaced StateT with StateRefT in the following

def fibS (n : Nat) : Nat :=
  if n < 2 then n
  else
    Id.run $ ( do
        let rec helper (n : Nat) : StateT (Nat × Nat) Id Nat :=
          match n with
          | 0 => do
                    let (x, _) <- StateT.get
                    return x
          | k + 1 => do
                       let (x, y) <- StateT.get
                       StateT.set (y, x + y)
                       helper k
        helper n
    ).run' (0, 1)

#eval fibS <$> List.range 11

to obtain

def fibS' (n : Nat) : Nat :=
  if n < 2 then n
  else
    Id.run $ ( do
        let rec helper (n : Nat) : StateRefT (Nat × Nat) Id Nat :=
          match n with
          | 0 => do
                    let (x, _) <- StateRefT.get
                    return x
          | k + 1 => do
                       let (x, y) <- StateRefT.get
                       StateRefT.set (y, x + y)
                       helper k
        helper n
    ).run' (0, 1)

But the fifth line (at StateRefT (Nat × Nat) Id) is underlined with the following error:

failed to synthesize
  STWorld ?m.1132 Id

How does one go about fixing the code? Help greatly appreciated.

[Kyle Miller]

Basically, you need to use it within a monad that has IO access (it can be used a bit more generally than just IO, but that's a reasonable approximation)

[Kevin Cheung]

So, something like this?

def fibS'' (n : Nat) : IO Nat :=
  if n < 2 then pure n
  else (do
          let rec helper (n : Nat) : StateRefT (Nat × Nat) IO Nat :=
            match n with
            | 0 => do
                      let (x, _) <- get
                      return x
            | k + 1 => do
                         let (x, y) <- get
                         set (y, x + y)
                         helper k
          helper n).run' (0, 1)

#eval List.mapM fibS'' $ List.range 11

[Kyle Miller]

Yeah, exactly.

[Kevin Cheung]

Basically, StateRefT is not really a replacement for StateT in general. Maybe if one is looking for performance, ST.Ref is a better choice?

[Kyle Miller]

Yeah, I think StateRefT is supposed to be a more-performant version of StateT when you have access to ST.Ref

[Kevin Cheung]

It is possible to make StateRefT have access to ST.Ref?

[Kyle Miller]

Yeah, by using monads such as IO that provide the ability to use it.

[Kyle Miller]

Unless you mean something else?

[Kevin Cheung]

More concretely, if I want to modify my fibS'' to use ST instead of IO while sticking to StateRefT, is there a way to do it? Because for a function like this, I don't want it to be trapped in IO.

[Kyle Miller]

No, the point is that ST.Ref is a mutable reference, and you need an "STWorld" (a.k.a. some access to the runtime environment itself) to manage these mutable references.

[Kevin Cheung]

I managed to cook up the following from the Haskell version:

-- Adapted from https://wiki.haskell.org/Monad/ST#A_few_simple_examples
def fibST (n : ℕ) : ℕ :=
  if n < 2 then n
  else
    runST (fun σ => do
            let rec fibST' (n : ℕ) (x y : ST.Ref σ ℕ) :=
              match n with
              | 0 => x.get
              | k + 1 => do
                          let x' <- ST.Ref.get x
                          let y' <- y.get
                          ST.Ref.set x y'
                          y.set (x' + y')
                          fibST' k x y
            let x <- ST.mkRef 0
            let y <- ST.mkRef 1
            fibST' n x y
          )

#eval fibST <$> List.range 11

So, the magic here is in runST?

[Kyle Miller]

Oh, neat, I didn't know about that, sorry for the wrong information.

[Kevin Cheung]

Now, I'm confused. :sweat_smile:

[Kyle Miller]

It looks like the deal is that getting and setting values from this reference can't be reasoned about, but you're allowed to make use of ST.Ref in pure code by using runST

[Mario Carneiro]

yes, and I believe (although I don't have a proof) that the obvious axioms on ST expressions are inconsistent

[Mario Carneiro]

ST really doesn't mesh well with lean's semantics, it's brilliant in haskell but it doesn't make that much sense in a dependent type theory with ZFC like semantics

[Kevin Cheung]

Then, is it reasonable to say that one should avoid ST in writing verified software and just stick to StateT?