@@ -253,36 +253,33 @@ Will there be support for Unicode characters for operators?
254There are several reasons why we should not support Unicode operators:
254There are several reasons why we should not support Unicode operators:
256−- It's hard to type (this is important if you're using someone else's
256+- It's hard to type (this is important if you're using someone else's code, for
257− code, for example). I know various editors have their own input
257+ example). Various editors have their own input methods, but you have to know
258− methods, but you have to know what they are.
258+ what they are.
259−- Not every piece of software easily supports it. It doesn't render
259+- Not every piece of software easily supports it. Rendering issues have been
260− properly on my phone email client, for example, occasionally messes
260+ noted on some mobile email clients, terminal-based IRC clients, web browsers,
261− up the terminal I run my IRC client in, doesn't always render
261+ etc. There are ways to resolve these rendering issues but they provide a
262− properly in my browser, etc. All of these are things I can fix but to
263− have to do so as a barrier to entry to using a programming language
262+ barrier to entry to using Idris.
264− doesn't seem to be a good idea to me.
265−- Even if we leave it out of the standard library (which we will in any
263+- Even if we leave it out of the standard library (which we will in any case!)
266− case!) as soon as people start using it in their library code, others
264+ as soon as people start using it in their library code, others have to deal
267− have to deal with it.
265+ with it.
268−- Too many characters look too similar. We had enough trouble with
266+- Too many characters look too similar. We had enough trouble with confusion
269− confusion between 0 and O without worrying about all the different
267+ between 0 and O without worrying about all the different kinds of colons and
270− kinds of colons and brackets.
268+ brackets.
271−- There seems to be a tendency to go over the top with use of Unicode.
269+- There seems to be a tendency to go over the top with use of Unicode. For
272− For example, using sharp and flat for delay and force (or is it the
270+ example, using sharp and flat for delay and force (or is it the other way
273− other way around?) in Agda seems gratuitous. I really don't want to
271+ around?) in Agda seems gratuitous. We don't want to encourage this sort of
274− encourage this sort of thing, when words are often better.
272+ thing, when words are often better.
276−I know that used with care it can make things look pretty. But so can
274+With care, Unicode operators can make things look pretty but so can ``lhs2TeX``.
277−``lhs2TeX``. And I'm sure that in a few years time things will be
275+Perhaps in a few years time things will be different and software will cope
278−different and software will cope better and it will make sense to
279−revisit this. For now, however, I would prefer not to allow arbitrary
276+better and it will make sense to revisit this. For now, however, Idris will not
280−Unicode symbols in operators.
277+be offering arbitrary Unicode symbols in operators.
282This seems like an instance of `Wadler's
279This seems like an instance of `Wadler's
283Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
280Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
285−This answer is taken from Edwin Brady's response in the following
282+This answer is based on Edwin Brady's response in the following
286`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`__.
283`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`__.