Defining mutable rose trees

Stream: lean4

[Jannis Limperg]

I'm trying to define a data structure that, in slightly simplified form, amounts to a mutable rose tree, where nodes carry references to their children and a reference back to their parent. I've found a way to do it (see below), but it's a bit cumbersome. Is there a more elegant way?

My construction:

unsafe inductive MutRoseTreeImp (α : Type) : Type
| mk
  (parent : Option (IO.Ref (MutRoseTreeImp α)))
  (children : Array (IO.Ref (MutRoseTreeImp α)))
  (payload : α)

structure MutRoseTreeSpec (α : Type) where
  MutRoseTree : Type
  construct :
    Option (IO.Ref MutRoseTree) →
    Array (IO.Ref MutRoseTree) →
    α →
    MutRoseTree
  parent : MutRoseTree → Option (IO.Ref MutRoseTree)
  children : MutRoseTree → Array (IO.Ref MutRoseTree)
  payload : MutRoseTree → α
  -- We could add equations relating `construct` and the field accessors.

open MutRoseTreeImp in
unsafe def MutRoseTreeSpecImp α : MutRoseTreeSpec α where
  MutRoseTree := MutRoseTreeImp α
  construct := MutRoseTreeImp.mk
  parent | (mk x _ _) => x
  children | (mk _ x _) => x
  payload | (mk _ _ x) => x

@[implementedBy MutRoseTreeSpecImp]
constant mutRoseTreeSpec α : MutRoseTreeSpec α := {
  MutRoseTree := α
  construct := fun _ _ a => a
  parent := fun _ => arbitrary
  children := fun _ => arbitrary
  payload := fun a => a
}

def MutRoseTree α :=
  (mutRoseTreeSpec α).MutRoseTree

namespace MutRoseTree

variable {α : Type}

def mk := (mutRoseTreeSpec α).construct
def parent := (mutRoseTreeSpec α).parent
def children := (mutRoseTreeSpec α).children
def payload := (mutRoseTreeSpec α).payload

end MutRoseTree

Some questions you might have:

• Why is MutRoseTreeImp unsafe in the first place? Because apparently the kernel doesn't know that IORefs are strictly positive, so without the unsafe it complains about an invalid occurrence of MutRoseTreeImp in a constructor argument.
• Can you generalise to STRef? No, this gives error "(kernel) mutually inductive types must live in the same universe". This seems like a bug. I imagine Lean tries to compile the data type as a nested type and introduces some universe issue during that. (But why doesn't the same happen with IORef?)
• Why do you need the type to be non-unsafe in the first place? I don't really, this is for a tactic so I guess I could just leave everything unsafe. But where's the fun in that?

[Mario Carneiro]

Regarding Q2:

abbrev Ref := ST.Ref

unsafe inductive MutRoseTreeImp (σ α : Type) : Type
| mk
  (parent : Option (Ref σ (MutRoseTreeImp σ α)))
  (children : Array (Ref σ (MutRoseTreeImp σ α)))
  (payload : α)

[Mario Carneiro]

very strange

[Jannis Limperg]

Ah, that's a nice workaround for now. Thanks!

[Mario Carneiro]

I'm not sure it's a good idea, but you can use the type unsafety mechanism I just posted about in order to avoid unsafe here, by storing effectively void* pointers in the inductive (which means it doesn't need to be recursive) and casting them to rose tree pointers for the API

[Jannis Limperg]

Evil (but delightful?). This would make the construction a lot shorter, but I guess the STRefs will become opaque at some point so I won't rely on it.