[Agda] Re: Floatpoint priorities (to wish list)

[Nils Anders Danielsson]

On 2010-06-28 13:57, Serguey Zefirov wrote:
> What I get from
> http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-mixfix.pdf
> is that there are plans to specify priorities as directed acyclic
> graph.

I am currently leaning towards dropping the requirement of acyclicity.
Consider the following example:

   module A where

     _●_ and _○_ are unrelated.

   module B where

     open import A

     _↑_ binds weaker than _○_ but tighter than _●_.
     (_●_ and _○_ are still unrelated.)

   module C where

     open import A

     _↓_ binds weaker than _●_ but tighter than _○_.

   module D where

     open import B
     open import C

     Here we have the following precedence graph:

     _●_ < _↑_ < _○_ < _↓_ < _●_

If we require precedence graphs to be acyclic, then we have a problem in
module D. There are several possible solutions to this
problem:

• Disallow D. This would mean that one could break a program by changing
   a fixity declaration for an unused operator, so this seems like a bad
   choice.

• Disallow fixity declarations which place operators between
   previously defined operators. I suspect that this would be too
   inflexible.

• Disallow a given expression if the precedence graph, restricted to
   the particular operator name parts in the expression, is cyclic. I am
   not too fond of this choice, because there is no one-to-one
   correspondence between operators and operator name parts.

• Allow cyclic precedence graphs. Cyclic precedence graphs easily lead
   to ambiguous grammars, but we expressly forbid ambiguous /parses/.
   This solution is rather flexible. For instance, as long as the
   operators _↑_ and _↓_ are not used in the same expression we won't
   encounter any ambiguity in the example above.

--
/NAD