tree using pointers

Stream: general

[Frederick Pu]

I'm trying to make a tree/graph using pointers and I'm getting mutually inductive type error. Does anyone have any suggestions on how I should implement it?

-- (kernel) mutually inductive types must live in the same universe
inductive AutoDiffNode (α : Type) (β : Type) : Type
| mk
    (outShape : List Nat)
    (parents : Array (ST.Ref IO.RealWorld (AutoDiffNode α β)))
    : AutoDiffNode α β

[Edward van de Meent]

i'm pretty sure inductive types already use pointers...

[Edward van de Meent]

that aside, this looks to me like a lean bug...

[Arthur Adjedj]

Not a bug. When the kernel translates this nested inductive type into a mutual type, AutoDiffNode appears nested into Nonempty in ST.Ref, which lives in Prop (and thus, so does it’s auxiliary inductive translation), leading to this error.

[Frederick Pu]

im trying to create a computation graphs where you can have multiple nodes pointing to the same node

[Frederick Pu]

are refs the wrong approach for this

[Daniel Weber]

Frederick Pu said:

im trying to create a computation graphs where you can have multiple nodes pointing to the same node

If it's acyclic then you should be able to directly use inductive types

[Frederick Pu]

but if u have some node x and y = mk _ #[x] and you modify the value of y, how can u guarantee that your variable x will be changed? wouldnt u still need some sort of ref system?

[Frederick Pu]

i think the best approach is just to store pointers to the data of the tree nodes rather than the tree nodes themselves, since my main goal is for multiple recursive calls to be able to modify the same trees data values:

inductive AutoDiffNode where
| mk
    (outShape : ST.Ref IO.RealWorld (List Nat))
    (parents  : Array AutoDiffNode)
    : AutoDiffNode

[Sebastian Ullrich]

For mutable graphs you'll likely want to use an index-based data structure like one would in Rust https://smallcultfollowing.com/babysteps/blog/2015/04/06/modeling-graphs-in-rust-using-vector-indices/

[Frederick Pu]

is the IO.RealWorld based ref slower?