I am reading http://adam.chlipala.net/cpdt/html/Hoas.html and I am trying to understand this Coq code regarding parametric HOAS (Higher Order Abstract Syntax):
Inductive Closed : forall t, Exp t -> Prop :=
| CConst : forall n,
Closed (Const n)
| CPlus : forall E1 E2,
Closed E1
-> Closed E2
-> Closed (Plus E1 E2)
| CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
Closed E1
-> Closed E2
-> Closed (App E1 E2)
| CAbs : forall dom ran (E1 : Exp1 dom ran),
Closed (Abs E1).
I have several questions regarding it:
Closed inside the bodies of constructors? Is this some kind of recursive declaration (without the starting of ending condition?)? Or maybe Inductive definitions come in two flavours: 1) usual type definitions; 2) some kind of statement about type? And this code is statement about type, not definition.Closed? Usually I can imagine that parametric HOAS is about enhancing of initial types. So, I expect, that Closed is more enhanced type and I could define constant John : Closed. But actually it is derived from Exp t -> Prop and so, it seems to me, that this is not enhancement of initial type but this is statement (predicate) about expressions of initial type. And the structure of this predicate reflects the structure of the terms of initial type and that is why it can be somehow used for structural induction.I am also reading https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html#coq:cmd.definition chapter "Simple annotated inductive types" but I can not understand how it is possible to use type name inside the constructors.
Repeating the name of the type is perfectly fine in Coq; this is simply defining a recursive data type. Consider the definition of the natural numbers in the standard library:
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
This says that the nat type is generated by two constructors O and S. The recursive occurrence in the type of S means that we can use previously built natural numbers to construct other natural numbers; e.g.
Definition zero : nat := O.
Definition one : nat := S zero.
Definition two : nat := S one.
etc. The example that you gave, Closed, is a bit different, because it defines an inductive family of propositions instead of a typical data type like natural numbers or lists. This family is indexed by terms of type Exp t for any t. Besides these differences, the recursive occurrences behave pretty much the same as the case of nat. For instance, the CPlus constructor says that, in order to show that Closed (Plus E1 E2) holds, we need to show that Closed E1 and Closed E2 hold.
I do not understand what you mean by "enhancing a type" or "initial type", but as far as I can tell Closed E is a proposition stating that the expression E : Exp t does not have free variables.