Agda-2.3.2.2: notes/design/fixities
Some thoughts on fixities
-------------------------
** The target of a fixity declaration
When you declare a fixity it should refer to a particular binding of that
name, not (as in Haskell) the name in general. The reason for this is: it's a
good design. A particular name might mean different things at different times,
and so you should be able to assign it different fixities.
One option then is to somehow attach the fixity declaration to the binding
site of the name. An argument against this is that it's very nice to give all
the fixity information in one place:
infixl 8 +, -
infixl 10 *, /
Instead of attaching it to the different definitions.
** The scope of a fixity declaration
So the question is then what declaration are we referring to when we say
infix 5 <>
A simple answer is: the <> in scope. Consider then the following example:
suc x + y = suc (x + y)
infixl 10 +
What's the fixity of + in the body? It clearly has to be infixl 10, since how
else would you declare it? This illustrates that fixity declarations follow
different scoping rules from normal declarations.
If we accept that the scoping for fixity declarations is weird, would there be
any problems in allowing the fixity to appear before the definition of the
name?
infixl 10 +
suc x + y = suc (x + y)
Not really. We just get weird scoping in a different way.
** Local fixity declarations
The examples, so far has been about fixities of declared names. You could also
imaging declaring fixities for bound names:
\(+) -> let infixl 9 + in 1 + 2 + 3
We'll get back to that shortly.
Another thing to consider is whether it should be possible to redefine the
fixity of a function. Let's look at the consequences:
Yes:
We should be able to write something like the following
infixl 10 +
(+) = ...
foo = 1 + 2 + 3
where
infixr 8 +
So far nothing strange. What about this example:
infixl 10 +
(+) = ...
foo = let infixr 8 +
x = 1 + 2 + 3
(+) = ...
y = 4 + 5 + 6
in x + y
Following what we've said the fixity of + in x should be infixl 10, but this
looks really weird, considering that we declare the fixity of + in the line
above x to be infixr 8. In fact it's not even clear which definition of +
this fixity declaration refers to.
No:
Considering the example above this seems like the best choice. There is a
problem with declaring the fixity of bound names, though. For declared names
the restriction is simply that the fixity declaration must appear at the
same level (same module/abstract/private/mutual/let-block), for bound names
it's not that simple. For instance, we would expect the example above to be
correct:
\(+) -> let infixl 9 + in 1 + 2 + 3
But then we get into the same problem as if we allow redefinition of
fixities:
\(+) -> let infixl 9 +
foo = 1 + 2 + 3
x + y = ...
bar = 4 + 5 + 6
in foo + bar
Which + are we declaring the fixity of? To solve this problem we don't allow
fixity declarations for bound names.
The same block
Actually the restriction on where the fixity declaration can appear isn't that
simple as let on above. As mentioned in the beginning it's nice to group the
fixity declarations of related functions. If some of these functions are
abstract, private or mutually recursive you wouldn't be able to do this. The
solution is to use the scoping rule for the blocks. If a name declared inside
a block is visible outside the block, then the fixity declaration can appear
outside the block. This means that you can pull fixity declarations out of
abstract, private, and mutual blocks, but not out of modules of local
definitions.
A natural question is if we are allowed to push fixities inside these blocks:
(+) = ...
private infixl 10 +
There's not really a problem with doing this except that since the declaration
modifiers (private/abstract/mutual) doesn't affect fixity declarations the
example above could give you the wrong idea (that the fixity isn't exported
outside the module). For this reason, the example above is disallowed.
Conclusions
You can declare the fixity of a declared name (but not a bound name). The
fixity declaration has to appear on the same level as the declaration. The
only exception to this rule is that fixity declarations can be lifted out of
abstract, private and mutual blocks.
The following would be OK:
infixl 8 +, -
abstract (+) = ...
(-) = ...
--
abstract (+) = ...
(-) = ...
infixl 8 +, -
--
abstract infixl 8 +
(+) = ...
infixl 8 -
(-) = ...
but the following would not be
abstract infixl 8 +, -
(+) = ...
(-) = ...
--
infixl 8 +
module Plus where
(+) = ...
vim: sts=2 sw=2 tw=80