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