Finger trees/polymorphic recursion

Stream: lean4

[Stuart Geipel]

Hey, I want to implement finger trees in lean4. I'm told this kind of recursive structure is called polymorphic recursion. Here is a smaller reproduction of my problem:

-- container which only admits 2^n elements for any n
inductive PowTree (a : Type) where
  | Unit (v : a)
  | Double (d : PowTree (a × a))

It says (kernel) arg #2 of 'PowTree.Double' contains a non valid occurrence of the datatypes being declared. I saw a similar error in this this topic but I'm hoping because I'm not parameterized on m : Type u → Type u like his example that this is actually possible - can you implement finger trees in lean4?

[Arthur Paulino]

Untested:

...
  | Double (d d' : PowerTree a)

I'm not on my PC, but I think your Double constructor doesn't work because of an universe bump

[Arthur Paulino]

Maybe the error message could be clearer on why the datatype is non valid

[Patrick Johnson]

inductive PowTree : Type → Type 1
| Unit {α : Type} : α → PowTree α
| Double {α : Type} : PowTree (α × α) → PowTree α

[James Gallicchio]

there's also some discussion in this thread, it seems like the Lean kernel requires a universe bump here even though Coq does not

[James Gallicchio]

but indeed you can make finger trees in lean4: https://github.com/JamesGallicchio/LeanColls/blob/main/LeanColls/FingerTree/FingerTree.lean

[Alex Keizer]

Note that, besides the universe bump discussion, you're also defining an inductive family here, using the syntax Lean uses for inductive types. That is, when you write

inductive PowTree (a : Type) where
  ...

Then your constructors may only depend on PowTree a, not PowTree (a x a), PowTree Nat or any other value for the parameter.

Inductive families are defined by moving the argument to the type, like Patrick showed, so

inductive PowTree : Type -> Type _ where
   ...

If you write it like this, the index is allowed to change. The underscore in Type _ tells the compiler to figure out the resulting universe for you, so you don't have to think about when you do or don't need a universe bump.

[Stuart Geipel]

Thank you everyone! I learned a lot about lean today.