Self type?

Stream: lean4

[Alok Singh]

I'm defining a QuadTree, and ran into this issue: how do I refer to a type in its fields?

structure Point where
  x : Float
  y : Float

structure Body where
  pos : Point
  mass : Float

structure QuadTree where
  center : Point
  size : Float
  totalMass : Float
  centerOfMass : Point
  bodies : List Body
  NW : Option QuadTree
  NE : Option QuadTree
  SW : Option QuadTree
  SE : Option QuadTree

here the last 4 fields

[Eric Wieser]

This works:

inductive QuadTree
| mk
  (center : Point)
  (size : Float)
  (totalMass : Float)
  (centerOfMass : Point)
  (bodies : List Body)
  (NW : Option QuadTree)
  (NE : Option QuadTree)
  (SW : Option QuadTree)
  (SE : Option QuadTree)

[Eric Wieser]

But then you have to write all the projections by hand

[James Gallicchio]

In my head this is one of the places where QPFs could help us metaprogram our way to victory -- but I am not confident in that claim or how much work it would take to get there...

[Eric Wieser]

It looks to me like this is just a missing feature in the structure command? Unless I'm missing something, I would assume all the same projections could be generated

[Eric Wieser]

Maybe the issue here is structure eta, which is no longer possible?

[Mario Carneiro]

There is an exploit: Although you can't define recursive structures, you can get structures to appear in nested inductive types

[Mario Carneiro]

structure QuadTree' (A : Type) where
  center : Point
  size : Float
  totalMass : Float
  centerOfMass : Point
  bodies : List Body
  NW : Option A
  NE : Option A
  SW : Option A
  SE : Option A

inductive QuadTree where
  | mk : QuadTree' QuadTree → QuadTree

[Kyle Miller]

Eric Wieser said:

It looks to me like this is just a missing feature in the structure command?

I think we'll see recursive structures at some point, but it's not among the highest priority features at the moment.

(What's the issue with structure eta for recursive structures? I haven't thought at all about how recursive structures would interact with defeq.)

[Eric Wieser]

My limited understanding was that structure eta just greedily expands things, which no longer works if structures are recursive

[Eric Wieser]

(I said "missing feature" and not "bug" precisely because I think this is low priority)

[Kyle Miller]

Oops, I meant to be more explicit: recursive structures have a non-zero priority for the FRO, with a priority inversely proportional to implementation difficulty :smile:

My rough understanding, having not looked into it too deeply, is that for elaboration the command needs to be able to support it, and ideally it would support mutual blocks too. It'd be good to know if there are any kernel issues to be aware of, but looking at the kernel source, I don't think so, because the kernel sees any non-recursive one-constructor index-free inductive type as being a "structure" (is_structure_like). I don't know if the elaborator's type checker works with structures or "structures".

[Alok Singh]

this came up again but with typeclass constraints:

inductive Value
| mk
  (data : Float)
  (grad : Unit → Float)
  (_backward : Unit → Option Float := fun () ↦ .none)
  (_children : Lean.HashSet Value := .empty)
  (_op : String := "")

from karpathy's micrograd in python. the hashset is the problem, it demands BEq Value (and hashable for that matter). but defining beq after won't work and I can't use deriving. _children should form a DAG since it's supposed to be a computation graph

[Sebastian Ullrich]

You should take a look at the new Std.HashSet.Raw https://github.com/leanprover/lean4/blob/3efd0e4e1feae93e0fb5956492a2e32b2aa14821/src/Std/Data/HashSet/Raw.lean#L35-L36