Recursive Structures

Stream: lean4

[Mac]

Why is recursion forbidden in structures?

I ran into this limitation again today while refactoring Lake (to make the dependencies of Package the resolved packages rather than just the declarative specification). Thus, I either need to refactor Package into an inductive (and lose nice things like the structure syntax) or work around the type system with the via OpaquePackage. Both seem less than ideal, so I am curious as to the rational behind forbidding recursion.

[Mario Carneiro]

Observation: a recursive one-arg constructor supports the anonymous constructor notation, but not foo.1 syntax; however the kernel accepts foo.1 primitive projections:

import Lean
inductive Foo
| mk : Foo → Foo

example (f : Foo) : Foo := f.1 -- failed

open Lean Elab Term
elab "mk_foo" : command =>
  addDecl $ .defnDecl {
    name := `test
    levelParams := []
    type := .forallE `x (mkConst ``Foo) (mkConst ``Foo) .default
    value := .lam `x (mkConst ``Foo) (.proj ``Foo 0 $ .bvar 0) .default
    hints := .opaque
    safety := .safe }

mk_foo -- ok

[Sebastian Ullrich]

Mac said:

Both seem less than ideal, so I am curious as to the rational behind forbidding recursion.

I think the direct reason is that the structure elaborator does not use the inductive elaborator, so it can only support simple kernel inductive decls. It sounds like you instead want a nested inductive as a structure?
I imagine, without hard evidence, that combining the structure and inductive elaborator would be like putting the two in a particle collider and marveling at the fun bugs resulting from the collision.

[Mac]

Sebastian Ullrich said:

so it can only support simple kernel inductive decls. It sounds like you instead want a nested inductive as a structure?

I'm sorry, but my grasp of type theory jargon is not what it should be. What is the difference between a simple inductive and a nested inductive?

[Sebastian Ullrich]

If you want something like

structure Package :=
  deps : List Package
  ...

then that is a nested occurrence of Package inside the inductive type List. The inductive elaborator has to define Package as a mutually inductive type together with a specialized copy of List in this case.

[Yuri de Wit]

Thank you, for the link to the previous discussion about this.

[Kevin Buzzard]

Maybe use an inductive? Structures are not recursive.

[Yuri de Wit]

Yes, that is the approach I am taking but bumping into the nice conveniences (as Mac puts it) of the structure syntax etc that I am missing. For instance, being able to use .. in pattern matching.

[Mario Carneiro]

you should be able to use Value.mk (data := d) .. as a pattern even if it's an inductive constructor