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

Question

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?

Answer 1

There are two components to your question.

The first, corresponds to the idea of constructor subtyping (actually, non-empty lists are the first example of the paper). I don't think there are any hard reasons for it not to be included in proof assistants, except that mixing subtyping and dependent types is not easy, and ends up making the type theory quite more complex. This is why some form of subtyping is often obtained after the fact, as part of elaboration, using mechanisms like implicit coercions or type classes. Moreover, implicit subtyping in a dependently typed setting can become non-intuitive (see the comments under your question).

Finally, at some level this question hits the expression problem, which as of today does not have a clear and definite answer, especially in the dependently-typed setting (see eg Coq à la Carte for a partial attempt). So it raises a lot of design questions, which are not easy to answer.

As for your second question, regarding computing inductive types and their constructors. The radical version of this is given by a universe of datatype description, as introduced in The gentle art of levitation. With such a universe, one can compute and manipulate datatypes descriptions in an arbitrary way. But making such a system usable is hard (see for instance the current state of the art in Agda). At a high level, such datatype universes usually require a lot of encoding, and force you to lose a lot of tooling support that works for “standard” inductive types exactly because they are second-class, statically defined. Making the best out of both worlds is difficult.