Type of `let mut`

Stream: new members

[Josh Cohen]

I am reading through "Functional Programming in Lean" and I tried the following, which surprisingly typechecks:

def two (m: Type -> Type) [Monad m] : m Nat  := do
  let mut x := 0
  x := x + 1
  x := x + 1
  return x

Namely, why can the type of this be any Monad? From the explanation in the text, I would think that the let mut restricts us to the state monad (or at least a StateT transformer), but the overall expression inside the do block has no such restriction. How does let mut work?

[David Renshaw]

Monads are primarily used via do-notation, which is an embedded language for programming in an imperative style. It provides familiar syntax for sequencing effectful operations, early return, local mutable variables, loops, and exception handling. All of these features are translated to the operations of the Monad type class, with a few of them requiring addition instances of classes such as ForIn that specify iteration over containers.

Sebastian Ullrich and Leonardo de Moura, 2022. “do Unchained: Embracing Local Imperativity in a Purely Functional Language”. In Proceedings of the ACM on Programming Languages: ICFP 2022.

https://lean-lang.org/doc/reference/latest//Functors___-Monads-and--do--Notation/Syntax/#do-notation

[Josh Cohen]

Thanks for the pointer. So it seems from the paper (Figure 5) that let mut desugars to a local StateT instance that is then evaluated by StateT.run', is this correct?

[David Renshaw]

that's consistent with my understanding

[Aaron Liu]

clearly that's not what happens since #print two gives

def two : (m : Type → Type) → [Monad m] → m Nat :=
fun m [Monad m] =>
  have x := 0;
  have x := x + 1;
  have x := x + 1;
  pure x

[Aaron Liu]

no local instance here

[Henrik Böving]

Josh Cohen said:

Thanks for the pointer. So it seems from the paper (Figure 5) that let mut desugars to a local StateT instance that is then evaluated by StateT.run', is this correct?

The paper is not at all what is currently implemented in Lean and more of an ideal world type of situation.

[Josh Cohen]

Aaron Liu said:

clearly that's not what happens since #print two gives

def two : (m : Type → Type) → [Monad m] → m Nat :=
fun m [Monad m] =>
  have x := 0;
  have x := x + 1;
  have x := x + 1;
  pure x

In this case, what does the let mut give beyond just have?

[Aaron Liu]

it gives nothing (in this case)

[Aaron Liu]

but you can do stuff with it if you mutate inside a loop