The Coq mailing list

["Perry E. Metzger" <perry AT piermont.com>]

On Sat, 9 Nov 2013 23:53:55 -0500 Jason Gross 
<jasongross9 AT gmail.com>
wrote:
> Is there a good explanation somewhere of the level requirements for
> notations to factor properly?  For example, what level do I have
> can I substitute in for "L" in the following to make the code
> type-check?
> 
> Delimit Scope foo_scope with foo.
> Notation "x , y" := (prod x y) (at level L, no associativity) :
> foo_scope. Check (_, _). (* should be pair *)
> Local Open Scope foo_scope.
> Check _, _. (* should be prod *)
> 
> I've tried L = 200, and then the second check fails.  I've tried L
> = 199, and then the first check fails.  Is there any way to make
> this work?

Not an answer to your question (unfortunately I have none), but a
side comment.

The idea of expressing the precedence of operators and notations by
integers, although very simple, strikes me as a not very
expressive and especially not human-friendly way to do things.

In fact, the precedence of various notations forms a DAG of sorts,
and it seems to me that it would be better to say "operator B should
be higher precedence than A but below C" through some explicit
notation.

That is, there should be some textual way to just express
what the hierarchy is intended to be instead of arbitrarily assigning
integers to various levels. If you then wanted to insert a new
notation between two others, you would just say "this notation is
supposed to have higher precedence than notation X but
lower precedence than notation Y" or "this notation should have
identical precedence to this other notation".

Integers are simple, of course, but any assignment of levels to
integers is completely arbitrary and inexpressive (we don't mean to
say that "+" is at integer X, we mean to say it binds less tightly
than "*" but exactly as tightly as "-"), and bad in that we may run
out of integers between two operators so we're forced to pick large
numbers to express precedences, and these large numbers are not very
readable either.

A very similar problem shows up in Unix init scripts. System V chose
to express the ordering of initialization scripts by integers, which
makes it difficult to understand, say, that X comes before Y because Y
depends on X. In NetBSD, some colleagues of mine and I created a
system where init scripts explicitly described their dependencies
instead, which made everything far more readable. People seemed to
greatly prefer the new mechanism over integers, and it was quickly
adopted by other BSD Unix variants.

Perry
-- 
Perry E. Metzger                
perry AT piermont.com