The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Vladimir,

> Yes, I agree, sorry for raising a vague objection. But the question of what
> precisely the syntax of a "match" is, to me, remains. What is the arity of
> "match" in the sense of, e.g., nominal signatures? 

I believe we have to distinguish between two levels: the core language
supported by the kernel, and the high-level language provided to the
user.

On the contrary, say, of Agda, the kernel core level "match" has a
simple syntax which is described in section 4.5 of the reference
manual:

  match m as x in I _.._ a1..an return P with
  ...
  | ci xi1..xipi => fi
  ...
  end

However, there is a high-level pattern-matching compilation algorithm
which supports inputs from a larger language whose syntax is described
in section 2.2 of the reference manual. In particular, it can match
sequences of arguments against arbitrary deeply nested patterns. Also,
the compilation of "match x with y => 0 end" is 0, simply because the
high-level "match" is not the primitive "match" but syntactic sugar
for a (possibly degenerate) nesting of primitive "match" (you can show
the result of the compilation by using "Set Printing All."). As evoked
on the list, this is a direct consequence of how the compilation
algorithm is implemented but it is accordingly counterintuitive and it
might be better to change it eventually.

Regarding the kernel core construction, there are different ways to
describe its syntax and typing. Taking into account that contexts can
contain "let-in"s, my favorite presentation is the following:

  Γ ⊢ m : I a1..an u1..up
  Γ, Ω, x: I a1..an |Ω| ⊢ P : s'
  Γ, Δi ⊢ fi : P[Ω:=ui1..uipi;x:=Ci a1..an ui1..uipi]
  s' is allowed elimination sort for I a1..an u1..up
  ——————————————————————————————————————————————————
  Γ ⊢ match m as x in I _.._ a1..an return P with
      ...
      | ci xi1..xipi => fi
      ...
      end
      : P[Ω:=u1..up;x:=m]

where I has signature of parameters Δ (possibly including let-ins),
has arity A which weakly βιδ-reduces to ΠΩ.s (hence keeping let-ins),
and has constructors Ci of arity ΠΔi.I |Δ| ui1..uipi in context Δ
(with |Δ| the subset of names of non let-ins declarations in Δ); also
substitution P[Ω:=v1..vp] means instantiation of the non let-ins names
of Ω with v1..vp and of names of let-ins of Ω by their values.

> How many arguments it has? How many variables each argument binds?

For an inductive type with n constructors, it has n+2 arguments. Using
the parametric view above, the 1st argument (m) binds no variables,
the 2nd argument (P) binds as many variables as there are declarations
in Ω, plus one, the (i+2)-th argument (fi) binds as many variables as
there are declarations in Δi. But you might prefer to consider a
variant where these contexts are abstracted over the arguments (which
requires your theory to already have a λ), in which case, all n+2
arguments bind no variables at all (this is the variant given in
chapter 4 of the reference manual).

Hugo

PS: The bug with "y+2" in position of pattern is not related to
the semantics of "match" but to the use of notations in position
of pattern (writing "plus y 2" instead would give an appropriate
error message - I'm gonna fix the bug anyway soon).