# A question of understanding the paper "Parametric Higher-Order Abstract Syntax for Mechanized Semantics"

Hi, I am reading the paper “Parametric Higher-Order Abstract Syntax for Mechanized Semantics” and have a question.

The paper says “Figure 5 shows Coq code for this syntax formalization scheme.
We use Coq’s “sections” facility to parameterize the term type
with a type family var without needing to mention var repeatedly
within the definition.” I cannot understand the sentence. Why we do not need to mention `var` repeatedly within the definition? I think `term` receives an element of type `type`. Does it mean `term` also need to an argument of type `var`?

See https://coq.inria.fr/refman/language/core/sections.html ; Coq `Section`s are a way to introduce variables in the context of a family of definitions without mentioning them repeatedly in signatures. A bit as if you wrote “all the following theorems are quantified on n, which we omit for brevity”.

For example here’s a section from `List.v` in Coq’s library:

``````Section Map.
Variables (A : Type) (B : Type).
Variable f : A -> B.

Fixpoint map (l:list A) : list B :=
match l with
| [] => []
| a :: t => (f a) :: (map t)
end.

Lemma map_cons (x:A)(l:list A) : map (x::l) = (f x) :: (map l).
Proof.
reflexivity.
Qed.
``````

Notice how the Fixpoint and the Lemma don’t repeat the variables “A”, “B”, and “f”.
Yet at the end of the section the signature of map is `map : forall [A B : Type], (A -> B) -> list A -> list B`, so these variables get “generalized” eventually.

2 Likes

Thank you most sincerely! I undetstand now!