Defining tree with dependent branching factor

Stream: lean4

[Phil Nguyen]

Suppose I want to model terms of a (first-order, untyped) language, but still want to statically track that applications have the right arities:

/-- Functions / base constants -/
structure Const (arity : Nat) where
  name : String

/-- A term is either a variable, or an application of a function symbol to sub-terms -/
inductive Term where
| app : Const n → {args : Array Term // args.size = n} → Term
| var : String → Term

But I'll get an error:

(kernel) invalid nested inductive datatype 'Subtype', nested inductive datatypes parameters cannot contain local variables.

How should I fix this problem? Thanks!!

[Aaron Liu]

Using Fin n → Term works

[Phil Nguyen]

That works great thanks! I needed a few coersion instances to make things look nice but that's neat.

Is this problem fundamental, or more of a current implementation quirk that may eventually be improved? Thanks!

[Yury G. Kudryashov]

Note that n is an autoimplicit parameter here, so app has type ∀ {n : Nat}, ...

[Yury G. Kudryashov]

Also, why do you need a structure Const that takes arity but doesn't use it in any way?

[Yury G. Kudryashov]

See https://github.com/leanprover/lean4/issues/1964

[Phil Nguyen]

Thanks Yury for the issue link!

The arity was to avoid simple errors mis-applying the constant/function to the wrong number of arguments. For example:

abbrev MkTerm : Nat → Type
| 0     => Term
| n + 1 => Term → MkTerm n

-- For nicer term construction
instance : Coe String Term where coe := Term.var
instance : CoeFun (Const n) (λ _ => MkTerm n) where coe := /- omitted -/

def pair : Const 2 := ⟨"pair"⟩
def nil : Const 0 := ⟨"nil"⟩
def example : Term :=  pair (pair "x" "y") nil

Also, independent of whether I'll actually need to use the n at runtime for this example, is there in general a way to mark an index as "compile-time only", so if I accidentally retain it at runtime, I'll get an error, similar to multiplicities in Idris? Thanks!!

[Phil Nguyen]

Ohh now I realized Yury's question was why I hadn't done it this way, which would reuse the arity in Const and avoid the implicit n in Term.app. Thanks!!

structure Const where
  name : String
  arity : Nat

inductive Term where
| app : (c : Const) → (Fin c.arity → Term) → Term
| var : String → Term

[Yury G. Kudryashov]

Note that this is nice for proving theorems but it's bad for writing computable code.

[Yury G. Kudryashov]

I mean, Fin _ → _ isn't stored as an array in memory.

[Yury G. Kudryashov]

I tried to give a mutual inductive definition that stores children in an Array but failed.