Lean's Reference Counting and Cycle and Unsafe

Stream: lean4

[EDJ]

Background
Lean uses reference counting for memory management. In pure dependent type theory—using inductive types and monadic programming—cycles in the underlying memory representation are simply absent, so this setting is quite safe.

But what about unsafe programs (for the sake of a more general purposed usage), for example

unsafe inductive LinkList (A : Type 0) where
  | nil : LinkList A
  | cons : A -> IO.Ref (LinkList A) -> LinkList A

unsafe def createCycle : IO (IO.Ref (LinkList String)) := do
  let tailRef ← IO.mkRef LinkList.nil
  let headNode := LinkList.cons "*cycle*" tailRef
  tailRef.set headNode
  return tailRef

-- Recursive traversal through IO.Ref
unsafe def printcycle (n : Nat) (s : LinkList String) : IO String := do
  match n, s with
  | 0, _ => return "..."
  | _, .nil => return "nil"
  | n + 1, .cons val ref => do
      let next ← ref.get
      let rest ← printcycle n next
      return s!"{val} -> {rest}"

unsafe def hello2 : IO Unit := do
  let cycler : IO.Ref (LinkList String) ← createCycle
  let cycle : LinkList String ← cycler.get
  let s ← printcycle 5 cycle
  IO.println s

Such program can be compiled and run in the current Lean 4.

Questions

1. In this example, have we actually constructed a cycle (and thus a potential memory leak under reference counting)?
   If not, more generally, can Lean cause memory leaks in general purposed programming situation (using unsafe)?

2. What is the community’s view on this kind of program?

• (a) Are such unsafe usages considered non-idiomatic Lean programming, and therefore problems like this are the responsibility of the programmer?

• (b) Or, since Lean aims to be a general-purpose language, the community has plan or interest in supporting such "algebraic data types"—and thus including, cyclic data structures—in a principled way? (e.g. Swift's weak reference, or something else sorry I am not a GC/RC expert)

[Henrik Böving]

Like in other languages like Rust, once you use the unsafe keyword the guard rails are off and it is your responsibility to take care of things, in this case taking care of resolving the cycle. There are no near term plans to change anything about this.

[Jakub Nowak]

Isn't the question also about how to resolve the cycle? I would be interested in learning how too.

[Henrik Böving]

Can one not do it by simply taking an IORef in the cycle and setting it to a nil instead, then dropping the reference to that cons node.