Poll: coding style - constructor parameters

Using Coq
1

I recently had a discussion with some of my colleagues about the coding style. Compare

Inductive A :=
| A0 (x:nat): A.

vs:

Inductive A:=
| A0: forall (x:nat), A.

I personally favor the 1st version, for several reasons:

  1. It is terser

  2. It resembles “match” syntax for this type:

    match a with
    | A0 x => x
    end.

  3. Arguably, it is a bit closer to Haskell and OCaml syntax.

  4. I tend to think about “x” as a “parameter” of a constructor

I am just curious, what is your preference? Why?

Vadim

  • Always use forall
  • Never use forall
  • It depends…

0 voters

1 Like
2

I like forall because it has a simpler syntactic structure, or rather, it reuses the complexity that’s already in the syntax of terms, and in the end it doesn’t look really different from the other style:

| <name> : <term>

(* instead of *)

| <name> <binder> ... : <term>
3

I avoid forall when possible, even in lemmas: Lemma foo {A} (a: A) : a = a. Proof. easy. Qed., because it’s terser, and Coq’s already pretty verbose for my Haskeller habits.

4

For me it would depend. If I’m describing a simple type and want to give names to the constructors for them to become clearer I would go with the first… almost. I wouldn’t ascribe the type as it is redundant in that case:

Inductive A :=
| c1 (x : nat)
| c2.