RFC: Add mathematical/arrows unicode operator support

[fabianhjr]

Major change:

• Support Mathematical Operators and Arrows as Symbols/Operators

From a commit in this repo:

While we're at it, Idris 1 supports unicode identifiers (although we don't encourage it :)) so this allows any characeter >127 in an identifier.

Though from Idris 1 FAQ [2013]:

Perhaps in a few years time things will be different and software will cope better and it will make sense to revisit this. For now, however, Idris will not be offering arbitrary Unicode symbols in operators.

This doesn't allow any arbitrary unicode, it adds the following 2 blocks:

• Mathematical Operators
• Arrows

This is a work in progress. I want to add a pragma or compiler option to enable this (So that this extra operators are opt-in) however since there is the possibility that unicode operators (even non-arbitrary) aren't desirable I would leave this as currently is for people to evaluate before implementing flags/pragmas to control this feature.

[edwinb]

I know some people are keen on this sort of thing (I'm occasionally asked about it). Usually the reasoning is about wanting to make the code look more like the maths that's being modelled. It's a reasonable thing to want, although not something that Idris is generally targetted towards. So, I'm going to have to think about what has changed since the FAQ entry you refer to. I think it's right to revisit the issue, but I would still like to be careful.

The bug fix is definitely necessary - thanks for spotting that! Could it be in a PR on its own instead, though?

There are two things I'd definitely require:

• At least for now, a flag to enable it (as you mention)
• No unicode operators in any of the libraries distributed with Idris

I'm also a bit worried about what will happen to external library code, but I'd hope some reasonable conventions would emerge based on what the standard libraries do, and based on needing a flag to enable support.

[fabianhjr]

Ah yes, the minor unicode identifier fixes are on #290, I forgot to put that in the PR description.

[petithug]

My 2 cents: As a software developer, the mathematical notation is puzzling -- there is no standard for that representation, and it is quite usual that math papers start by defining the notation that will be used in the rest of the paper.
Conversely in software engineering we are used that a name or symbol has one single meaning, at least per programming language.

So I think that it is fine that packages would choose to use a mathematical notation, using Unicode symbol or names, with the possibility of renaming names from the Prelude and Base packages as Unicode names and symbols. But to build on what Edwin said, I would forbid to use any Unicode name or symbol in the Prelude and Base, e.g. by adding a flag in the package ipkg that permits to verify this when parsed.

Then there would be the issue of the implication and equality symbols. Here I would define a directive to alias these, such as they could be renamed on a package per package basis.

[petithug]

http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/squiggol-history.pdf

[nightscape]

As a side note: Scala allowed Unicode operators, but deprecated and now forbid them. The problem is that if person A starts with Unicode, but person B working on the same code cannot easily type them, you get a mix of both which is not nice.
Also, fonts with ligatures allow you to display operators in a nice looking fashion while still being just ordinary Ascii characters.