# Why inductive types (or variants) are so rigid in terms of the set of constructors

An inductive type definition normally carries a set of constructors C, but I am not so sure why the set of constructors C is always once-for-all statically defined. For instance:

Inductive list : Type :=
| nil : list
| cons : A -> list -> list.

Inductive non_empty : Type :=
| cons : A -> list -> non_empty.

So every time I need a definition of a non-empty using the list definition I have to write a proposition that forbids a list to be empty x:= x <> []. Even though non_empty is clearly a subtype of list. I have only seen one type theory that relaxes this restriction by allowing a type construction to be defined by a computable function, but self-types are very complex compared to the usual definition of inductive types.

I have experimented subtyping in type constructor by implementing a proof assistant and this seems feasible. My question is why this approach is the most common one? Is there any mathematical implication if we relax this and handle inductive types with subtyping or a computable set of C constructors? Is there any work/formalization on this?

• Subtyping is generally a can of worms. Is $P = (\textrm{list} \to X)$ a subtype of $Q = (\textrm{non-empty} \to X)$? If so, does it mean it is possible to have $f \ne g : P$ despite the fact that $f = g : Q$?
– Trebor
Commented Nov 1, 2023 at 10:37
• @Trebor yes, and yes. Even if subtyping is implicit, $f : Q$ is simply not the same object as $f : P$. In particular, most interesting forms of subtyping are not injective. That being said, I agree that this makes implicit subtyping somewhat frightening/non-intuitive. Commented Nov 1, 2023 at 10:44