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?