Coq: Would adding "inline inductive definition expressions" introduce inconsistency?

Question

Scenario: new ind syntax

As far as I know, in Coq, you cannot create new inductive types by only using expressions. You must use commands--namely, the Inductive command.

Suppose we want to turn Coq into a language with only expressions, and no commands. This requires us to remove the Inductive command (as well as all the other commands, of course). In its place, we introduce an ind expression. The syntax might look like

ind <name> <params> : <arity> with
| case1 <args> : <name> <indices>
| case2 <args> : <name> <indices>
| <...>
end

We also introduce syntax for accessing constructors: <ind_exp>::<constr_name>.

Example

To make things clear, here's a more concrete example. Suppose we have the existing Coq code:

Inductive nat : Set := | zero | succ (pred : nat).
Definition one := succ zero.
Definition ident := fun (n : nat) => n.

If we use the new syntax, the code for the expressions one and ident respectively become:

• one:

  (ind nat' : Set with
  | zero : nat'
  | succ (pred : nat') : nat'
  end)::succ
  
  (ind nat' : Set with
  | zero : nat'
  | succ (pred : nat') : nat'
  end)::zero
  

• ident:

  fun(
       n : (ind nat' : Set with
            | zero : nat'
            | succ (pred : nat') : nat'
            end)
  ) => n
  

Question

Does this new "inline inductive definition expression" syntax introduce any logical inconsistencies? Assume that the same restrictions that apply to the old Inductive syntax (e.g., universe consistency, strict positivity) also apply to the new ind syntax.

EDIT: Background info (for context).

This section might be TMI, as some parts are only distantly related to the above question. You can skip it if you want. But if you're curious, read on.

I'm designing a programming language (as a personal project) where everything is an expression. Going the "everything is an expression" route was a somewhat arbitrary design choice--mostly a matter of personal preference.

The language will be a very simple "kernel" language. The main goal is maximizing the ease of compiler implementation. This language will serve as a target language for higher level languages I write in the future. Since code in this language will be computer generated, the language does not need to be "human friendly".

Regarding Andrej Bauer's answer:

How are inductive types compared for equality? With named inductive types we just compare the names.

Two inductive types are equal iff they are identical after normalization. Internally, the language uses De Bruijn indices, and constructors are represented with numbers instead of names. Thus, names are irrelevant.

This has the drawback of making ind bool with true | false end equal to ind pole with north | south end. To fix this, ind expressions have a "discriminator string". Even after names are converted to numbers, the discriminator strings are left intact. This lets us distinguish between ind bool "bool" with true | false end and ind pole "pole" with north | south end.

So the true ind syntax is actually

ind <name> "<discrim_str>" <params> : <arity> with
| case1 <args> : <name> <indices>
| case2 <args> : <name> <indices>
| <...>
end

However, since this detail isn't relevant to the question, I elided it in the original post, to keep things simple.

---

Do you expect the user to always write 〈huge-expression〉:: cow?

Yes. But since the code is computer-generated, this is not a problem.

---

Should we worry about inefficiency, because types might become very large? At the very least we need to make sure there is lots of common subexpression sharing, and we must avoid checking the same equalities over and over.

You bring up a great point! The compiler makes heavy use of caching (or I should say, it will, once I'm done building it). Most of the time, it just compares hashes instead of comparing the entire (massive) expression. It uses shared references to avoid exponential memory consumption.

---

By the way, inductive type definitions are used not only for definitions of (inductive) recursive types, but also for simple sums ... If we take these away, we should consider expression-style sum types.

As far as I can tell, ind expressions already cover this case. If we translate your OCaml code to our new hypothetical language, we obtain:

(* sum *)
fun (A B : Set) => ind sum with
| inl (a : A) : sum
| inr (b : B): sum
end

(* tree *)
fun (A : Set) => ind tree with
| empty : tree
| inl (a : A) (left right : tree) : tree
end

Answer 1

No inconsistencies are introduced, but there will be some questions regarding the implementation.

How are inductive types compared for equality? With named inductive types we just compare the names.

With expression-style inductive types, the constructors are not defined globally. So suppose you see an identifier cow, which is not currently in the context (was not introduced by a binder), so it might be a constructor of an inductive type. How will you find the inductive type that cow might belong to? Do you expect the user to always write 〈huge-expression〉:: cow?

Should we worry about inefficiency, because types might become very large? At the very least we need to make sure there is lots of common subexpression sharing, and we must avoid checking the same equalities over and over.

By the way, inductive type definitions are used not only for definitions of (inductive) recursive types, but also for simple sums, such as

Inductive sum (A B : Set) : Set :=
  | inl : A → sum A B
  | inr : sum A B.

If we take these away, we should consider expression-style sum types. One way to implement this is OCaml-style polymorphic variants, so the above sum would be something like:

λ (A B : Set) → [ `inl : A | `inr : B ]

(Note that there is special syntax for constructors, they're preceded by a backtick.) With this notation an inductive type of binary trees might look like this:

λ (A : Set) → ind tree [ `empty | `inl : A × tree × tree ] 

The general notation for inductive types would be ind X E where E is an acceptable type expression involving X. The defining equation is ind X E ≡ E[(ind X E)/x].