Make fixity declaration consistent with module syntax

[andrevidela]

• [x] I have read CONTRIBUTING.md.
• [x] I have checked that there is no existing PR/issue about my proposal.

Summary

Fixity declarations are important to facilitate code readability, they allow the user to inherit existing notions of syntax from other programming language (like ++ and >>=), from domain-specific knowledge (like / for file paths), or from mathematics (like |> for $\rhd$ or |- for turnstile).

However they suffer from being a second-class citizen in the language since they have no proper presence in the module system. As part of program parsing they are more akin to syntactic macros than to proper functions. This aims to outline a plan to introduce fixity as a proper construction that's consistent and integrated with the rest of the feature set from the language.

Implementation progress

• [x] Stage 1: Hide fixities #2997
• [ ] Stage2 : Accessibility modifiers for fixities
  • [x] Allow them to be private #3011
  • [ ] Add warning for unlabelled fixities, update existing fixity declarations in std lib & other libs with access modifier #3234
• [ ] Stage 3: Make conflicting fixities error
  • [ ] make unlabelled fixities private
  • [ ] make conflicting fixity imports an error
  • [ ] make conflicting fixity declarations an error

Motivation

There has been multiple issues and problem related to fixity and operators in the past, in recent memory #2832 and #2889 come to mind. But other languages have have their own share of issues like Haskell or Swift. One of the strength of Idris that comes with dependent types is the ability to write embedded DSL with strong type guarantees. Those DSL make heavy use of operators with custom fixities, for example preorder reasoning URIs and records.

However, the current implementation exposes some unexpected behaviors:

1. All fixities are always exported
2. Parsing depends on the import order, see #2889, #2832
3. Conflicting fixities are unresolvable

Fixities are always exported

Here is a proper example of this phenomenon:

module Lib

infixl 3 !>
infixl 2 #>

-- run with aribtrary scheduler
(!>) : (s : Scheduler t m) => (() -> m a) -> m a

-- run with default scheduler
public
(#>) : (() -> a) -> Promise a
(#>) = (!>) {s = defaultScheduler}

... -- code using !> for different purposes

Now if a user imports this library, they can write:

module User

import Lib

-- can use this with fixity infixl 3
(!>) : (a -> b) -> (b -> c) -> a -> c 

This is bad because the library author never intended to release !> outside the scope of their module and they have no recourse to stop this from happening.

The proposal

In a nutshell, the proposal is to integrate the syntax for modules with fixity declaration.

Fixities are private by default

This is the biggest breaking change from this proposal. Just like any other top-level definitions, fixities should be private by default. This means writing:

infixl 5 +

Only exposes the fixity at a file-level, to export the fixity for users the following is required:

export
infixl 5 +

This fixes problem (1).

The rationale is to avoid accidentally polluting the fixity namespace of packages and to remain consistent with other definitions which are exposed by the module system.

This breaks the current user expectation that writing infixl 5 + will expose the fixity. To help library designers, a warning should be emitted when the fixity is not provided either private or export modifiers. Finally, both export and public export should be accepted to render a fixity visible outside it's current module.

Conflicting fixities are now errors

This fixes problem (2), making it impossible to rely on import order to change the semantics of the program. This should also trigger an error at declaration-site if one tries to declare two conflicting fixities in the same namespace.

Fixities can be hidden like namespaced names

This fixes problem (3) by allowing to control which fixities are being used in the file, it also provides a resolution mechanism for errors due to conflicting fixities. This introduce the ability to identify a fixity using the familiar namespace mechanism.

import Lib

%hide Lib.infixl.(+)

Technical implementation

I've started working on a prototype and there are a couple of details making the implementation more complicated than one might think.

The core of the issue is that, because of their macro-like nature, fixities cannot be resolved at the same time as module imports. They have to be dealt with as part of parsing. Because of this, they will need special treatment. Thanks to a series of fortunate coincidences, this special case can easily be identified. Indeed, namespaced fixity identifiers are uniquely defined as: infix[l|r].(op) or prefix.(op). In terms of parsing, it is important to note that namespaces do not allow uncapitalised identifiers. This extensions to parsing does not break this rule because it introduces a reserved keyword as part of a namespace component. Because the name is reserved, it cannot appear as a standalone definition, and therefore will never conflict with a fixity identifier. Similarly, since we are using fixities as reserved keywords there is never going to be ambiguity with postfix projection: We cannot have .infix as a valid function call. Another fortunate coincidence is that, because %hide pragmas appear before the program is typechecked, we can perform any fixity-namespacing confidently before the syntax tree is re-associated, removing any potential staging issues. All the information we need is available upfront form the import list and the %hide directives.

One could argue that their syntactic similarity with modules is actually a lie, they behave completely differently from modules, even though they share the same syntax. I think this change is justified because the behaviour is reasonably consistent, and it does not introduce new cognitive overhead even though the implementation mechanisms are entirely different. This means users do not have to learn a new syntax or a new module system to manage fixities and can directly apply their knowledge of library modules. However it might raise some unanswerable questions like "what is the difference between public export infixl and export infixl?". Because fixities are not definitions, there is no difference between the two.

Implementing this proposal in one go will result in massive breaking of source-code due to making the existing syntax private and making the existing warning errors. Because of this I suggest implementing it using the following stages:

Stage 1 (non-breaking): Implement %hide and fixity identifiers. This will allow existing warnings about conflicting fixities to be resolved. It should also give us enough time to perform those changes across popular packages such as the ones we can find on pack Stage 2 (non-breaking): Provide a warning about unlabelled fixities and implement access modifiers for them. By providing a new warning for unexported we can repeat the strategy employed in the first stage to detect cases where the fixity is not exported and provide the appropriate export modifier. Stage 3 (breaking): Convert conflicting fixities into errors. Make un-labelled fixities private by default. The hope is that after updating libraries in stage 1 and 2, this should only break a small amount of them.

Alternatives considered

Do not export any fixities

This would be a valid implementation which removes the complexity of handling fixities at the module system and force the user of a library to re-declare a set of fixities that is consistent with the libraries they import. However, in some ways, this is a usability downgrade since every library documentation must contain the information "you must add those fixities after import for the library to work as intended" and could create confusion when sharing code snippets online from the same library imported with different fixities

Keep it as is

The current state is not unusable but leaves questions like #2832 hanging. The new policy could be that the warnings are good enough to discourage misuse while allowing "power-users" to achieve their goals by rearanging imports. It is my humble opinion that the motivation section provides enough evidence that the current state needs to be addressed.

Keep the unlabelled fixities public

This is the most reasonable objection to this proposal however it comes with the following shortcomings:

• It suffers from the same free-for-all that %access public suffered in Idris1
• It is inconsistent with the rest of the module system which does keep every top-level definition private by default
• Introducing inconsistency goes against the goal of inheriting knowledge about the module system for users of the language.

Finally I would argue that emitting a warning saying "please indicate if you mean this fixity as private or public" is a much better outcome than the current state where someone types out a fixity declaration and does not know what the consequences are in terms of scoping or exports.

Conclusion

While not entirely truthful to the module story, this approach fixes the three shortcomings mentioned, while providing a familiar framework to interact with fixities in a predictable way.

Other goodies:

• Provide a strategy to implement #1976 by providing a way to directly identify a fixity in scope :doc Ops.infixl.(+) would give you the precedence level of the fixity declared in the module Ops. Similarly :browse Ops would surface all the fixities exported by the module
• A good time to make Operators their own Name

[ohad]

This is really cool and I like the flexibilty this mechanism offers in how it solves the existing issues! Thanks!

Two comments:

1. I suggest we use the word export instead of public since it's consistent with existing usage (add a name to a namespace, rather than add a definition to the context).

2. I suggest we keep the default to be export but issue a warning for 1 release. In 2 releases, we make the default private. This way we're not (yet) breaking existing code, and 1 release later we'll have both mechanisms consistent.

[andrevidela]

Thank you for the feedback, this is what I intended to communicate so I'll amend the text to reflect this more clearly

edit: I've fixed the example and modified this part of the technical implementation:

Stage 1 (non-breaking): Implement %hide and fixity identifiers https://github.com/idris-lang/Idris2/pull/2997. This will allow existing warnings about conflicting fixities to be resolved. It should also give us enough time to perform those changes across popular packages such as the ones we can find on pack Stage 2 (non-breaking): Provide a warning about unlabelled fixities and implement access modifiers for them. By providing a new warning for unexported we can repeat the strategy employed in the first stage to detect cases where the fixity is not exported and provide the appropriate export modifier. Stage 3 (breaking): Convert conflicting fixities into errors. Make un-labelled fixities private by default. The hope is that after updating libraries in stage 1 and 2, this should only break a small amount of them.