The Coq mailing list

[Lauri Alanko <la AT iki.fi>]

On Tue, Jan 06, 2004 at 07:17:26PM +0100, Christine Paulin wrote:
>   Secondly, Coq version 8.0 comes with a completely new syntax of
> terms, and a slightly revised syntax for tactics and commands. Besides
> a better uniformity and a simplification of the syntax, the purpose is
> to allow the use of high-level comforts, such as implicit types in
> quantification and notations for standard arithmetical notions
> (e.g. +, *, <, <=) without conflicts with the rest of the syntax. A new
> notion of "interpretation scopes" allows also to reuse the same
> notations in different contexts of formalisation (e.g. +, * are valid
> on nat, Z, R, types, etc).

I very much like the new uniform infix syntax, and most of all I like
the fact that the precedences have been adjusted so that it's no longer
necessary to litter all formulas with parentheses.

However, I'm a bit dismayed by the new syntax for binders. Pi and lambda
are the most fundamental operations in the Calculus of Constructions. 
They shouldn't be so awkward to use. Maybe "fun" is still a bearable
syntax for lambda (though I like Haskell's \x->e better), but "forall"
for Pi is just too verbose at least for my taste. I can understand it as
syntactic sugar (like "exists"), but it shouldn't be primitive syntax.

In addition, it seems a bit confusing that in binders, simple
juxtaposition (even within parentheses) is meant to separate variables,
since everywhere else juxtaposition means _application_. In most
functional languages, the syntax for formal parameters is exactly the
same as for patterns, and I think it would be nice if the same were true
in Coq, so you could do eg.

Definition swap A B (a,b:A*B) := (b,a).

and the like.

I was rather fond of the neat minimalism of Coq 7's "[x]e" lambdas and
"(A)t" foralls (although, granted, ordinary parentheses were maybe not
the best choice). Could something like them be added to Coq 8, too?

Or alternatively, could they be implemented using Coq's syntax extension
mechanism? It's not obvious to me how to transform binder lists of
arbitrary length.


Lauri Alanko
la AT iki.fi