nested inductive type error

Stream: general

[Vaibhav Karve]

I am trying to define terms in a first-order language but am encountering a nested inductive type error.
MWE:

import tactic

constant vars : Type

structure lang :=
(funcs : ℕ → Type)
(consts : Type)

/- We define terms in a language to be constants, variables or
   functions acting on terms.-/
inductive term (L : lang) : Type
| const_term : L.consts → term
| var_term   : vars → term
| func_term  (n : ℕ) (f : L.funcs n) (v : vector term n) : term

Full error message

nested inductive type compiled to invalid inductive type
nested exception message:
nested occurrence 'subtype.{1} (_nest_1_1.list.term L) (fun (l : _nest_1_1.list.term L), (eq.{1} nat (list.length.{0} (_nest_1_1.term L) l) n))' contains variables that are not parameters

[Adam Topaz]

I think if you replace vector term n with fin n -> term it should work.

[Adam Topaz]

I don't know if that's what you would want to do though.

[Vaibhav Karve]

Thanks. That does work. I was using vector _ n as replacement of fin n -> term anyway. Should I always use fin n instead?

[Adam Topaz]

It's up to you, of course, but I think the fin n api is more developed.

[Vaibhav Karve]

Thanks. Also, do you know why it accepts fin n but not vector. What's the cause behind the nested inductive type error. Understanding that might help me debug this issue in the future.

[Adam Topaz]

@Mario Carneiro :up: ?

[Mario Carneiro]

Because it's a nested inductive type

[Adam Topaz]

Ah, so the problem is that vector is inductive?

[Mario Carneiro]

The problem is that a plain inductive only allows recursive occurrences of the type being defined, possibly behind some pis, in arguments to the constructor

[Mario Carneiro]

anything else and it will go through the hacky nested inductive compiler

[Adam Topaz]

Gotcha.

[Mario Carneiro]

so mk : (A -> T) -> T is okay but mk : set T -> T is not (it's inconsistent) and neither is mk : vector T n -> T (because lean isn't smart enough to distinguish it from the second case)

[Vaibhav Karve]

I also noticed that this issue is not encountered if using list term

[Mario Carneiro]

the nested inductive compiler can handle that, at least, although I don't recommend it because the induction principle is wrong

[Mario Carneiro]

but no one considered dependent nested inductive types when writing the compiler

[Mario Carneiro]

The QPF framework being developed primarily by Simon Hudon can handle these to some extent

[Vaibhav Karve]

Thanks

[Adam Topaz]

Unrelated to foundational issues, @Vaibhav Karve you might be interested in the first order logic developed in the flypitch project
https://github.com/flypitch/flypitch/blob/master/src/fol.lean

[Vaibhav Karve]

Thanks for the link Adam. That is indeed very useful.

[Adam Topaz]

(Also note that $0$-ary functions are constants :) )

[Yakov Pechersky]

There is some nice API in vector that isn't in fin, however. You can get back to fin n -> R from my_vector.nth.

[Yakov Pechersky]

And from fin n \to R to vector n R using vector.of_fn

[Floris van Doorn]

Mario Carneiro said:

but no one considered dependent nested inductive types when writing the compiler

I don't think that is quite true, the following "works":

universe variable u
inductive dvector (α : Type u) : ℕ → Type u
| nil {} : dvector 0
| cons : ∀{n} (x : α) (xs : dvector n), dvector (n+1)

inductive term : Type
| func_term  (n : ℕ) (v : dvector term n) : term

The problem is that vector is a subtype, which are not supported, and not an inductive family.
Of course I don't disagree with your point that one should avoid nested inductive types, including the one above.