Structures can't refer to their own type?

Stream: general

[Marvin]

structure Node where
  children : List Node -- unknown identifier 'Node'

There are many scenarios like this - and where you don't want to use inductive, because there are dozens of fields and you want it to count as a type and you are using it as a base structure for inheritance etc..

Is there no way to have this working? I thought perhaps the mutual keyword, but that seems to only work for inductives.

[Snir Broshi]

Works for me in the playground, where are you seeing this error?

[Snir Broshi]

FWIW I was going to point out that this might be related to Curry's paradox, but then the error didn't reproduce

[Aaron Liu]

see lean4#2512

[Violeta Hernández]

You want an inductive type that isn't an inductive? Huh?

[Violeta Hernández]

It's perhaps worth noting that structures in Lean are just a special case of inductive types, namely, those with a single constructor. So whatever you think you're avoiding, you really are not.

[Marvin]

Violeta Hernández said:

You want an inductive type that isn't an inductive? Huh?

I want a Record where one of the fields is a list of more of its kind. I am trying to create a faithful binding for javascript DOM.

structure Node where
  nodeName : String
  childNodes : List Node
structure Element extends Node where
  innerHTML : String

structure HTMLElement extends Element

[Weiyi Wang]

Your code runs fine on latest Lean. Are you on a very old version of Lean?

[Marvin]

Weiyi Wang said:

Your code runs fine on latest Lean. Are you on a very old version of Lean?

Yes, 4.6.1 as that has a web assembly build. Looking online now, im not finding any recent versions with this

[James E Hanson]

Marvin said:

Weiyi Wang said:

Your code runs fine on latest Lean. Are you on a very old version of Lean?

Yes, 4.6.1 as that has a web assembly build. Looking online now, im not finding any recent versions with this

Does this work? It's essentially the same thing.

inductive Node
| mk : List Node → Node

def Node.children (n : Node) : List Node :=
match n with
| mk l => l

[Kyle Miller]

Marvin said:

I want a Record where one of the fields is a list of more of its kind. I am trying to create a faithful binding for javascript DOM.

structure Node where
  nodeName : String
  childNodes : List Node
structure Element extends Node where
  innerHTML : String

structure HTMLElement extends Element

Others have already pointed out that Lean does have recursive structures (they've existed since Lean 4.14 I believe; they work in mutual blocks too).

However, even on a newer version this particular set of structures won't do what you intend: when you extend, it will still be a childNodes : List Node field. Presumably you want this to be a childNodes : List HTMLElement field in HTMLElement?

You have to do something like this to make the node type parametric, then use an auxiliary type to "close the loop":

structure Node' (N : Type) where
  nodeName : String
  childNodes : List N
structure Element' (N : Type) extends Node' N where
  innerHTML : String

structure HTMLElement' (N : Type) extends Element' N

inductive HTMLElement where
  | mk (el : HTMLElement' HTMLElement)

This should work even in older Lean versions; this is the pattern Lean core used before recursive structures. If this were 4.14 onward, you'd be able to use a structure instead of inductive.

I should also warn you that extends isn't for object-oriented-style polymorphism for structures. There are some limited facilities for auto-projecting to parent structures for resolving dot notation. Maybe this N parameter will be enough for you, but possibly you'll need some typeclasses too, depending on what kind of polymorphism you're wanting to achieve.

If you ever go to a more recent Lean, it's worth knowing you can do recursion in the extends clause. This means dot notation on HTMLElement can resolve in the Node', Element', and HTMLElement' namespaces.

structure Node' (N : Type) where
  nodeName : String
  childNodes : List N
structure Element' (N : Type) extends Node' N where
  innerHTML : String

structure HTMLElement' (N : Type) extends Element' N

structure HTMLElement extends HTMLElement' HTMLElement

(@James E Hanson Defining an inductive might be essentially the same thing, but practically you lose out on {...} notation and extends.)

[Marvin]

Is there no way to say

structure Node (N : Type <: Node) where

Basically, not just "some Type", but "some Type extending Node"
in Scala you can do

class Node[N <: Node](var childNodes : Set[N])

class Element extends Node[Element]

[Kyle Miller]

No, not with structure. There's no subtyping or inheritance.

It's possible to use classes to do some kinds of inheritance though, but you need to define classes and structures in parallel to simulate inheritance. The idea is you'd have a NodeClass class that defines what you need to implement for something to be a Node, then you make implementations of this class for everything in the Node hierarchy.

[Kyle Miller]

(A class in Lean isn't like class in Scala. You can think of Lean's as being just the vtable, minus the object, if you want.)

[Kyle Miller]

Here's an example of just the class part.

class Node N where
  nodeName : N -> String
  childNodes : N -> List N
class Element N extends Node N where
  innerHTML : N -> String
class HTMLElement N extends Element N where

def numChildNodes {N : Type} [Node N] (node : N) : Nat :=
  (childNodes node).length

[Kyle Miller]

You'd then need to add some concrete implementation to actually use it, but the point is that numChildNodes will work for a type where you've implemented an HTMLElement instance.

[Kyle Miller]

I guess Java interfaces are a reasonable comparison point.

[Violeta Hernández]

Rust's instances are basically one to one