@@ -17,6 +17,7 @@ Idris supports multiple back ends (C and JavaScript by default, with the
1717ability to add more via plugins) and has a reference run time system, written
1818in C, with a garbage collector and built-in message passing concurrency.
1919
20+
2021Is Idris production ready?
2122==========================
2223
@@ -32,6 +33,7 @@ for use in production would be very welcome - this includes (but is not
3233limited to) extra library support, polishing the run-time system (and ensuring
3334it is robust), providing and maintaining a JVM back end, etc.
3435
36+
3537Why does Idris use eager evaluation rather than lazy?
3638=====================================================
3739
@@ -60,6 +62,7 @@ Here, it is clear from the type that ``thing_val`` is guaranteed to be a
6062concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an
6163``Int``.
6264
65+
6366How can I make lazy control structures?
6467=======================================
6568
@@ -77,6 +80,7 @@ Booleans is defined as follows in the library:
7780The type ``Lazy a`` for ``t`` and ``e`` indicates that those arguments will
7881only be evaluated if they are used, that is, they are evaluated lazily.
7982
83+
8084Evaluation at the REPL doesn't behave as I expect. What's going on?
8185===================================================================
8286
@@ -156,6 +160,7 @@ letter, which will never be implicitly bound:
156160As a convention, if a name is intended to be used as a type synonym, it is
157161best for it to begin with a capital letter to avoid this restriction.
158162
163+
159164I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
160165=============================================================================================
161166
@@ -180,6 +185,7 @@ If you have a function which you believe to be terminating, but Idris does
180185not, you can either restructure the program, or use the ``assert_total``
181186function.
182187
188+
183189When will Idris be self-hosting?
184190================================
185191
@@ -187,6 +193,7 @@ It’s not a priority, though not a bad idea in the long run. It would be a
187193worthwhile effort in the short term to implement libraries to support
188194self-hosting, such as a good parsing library.
189195
196+
190197Does Idris have universe polymorphism? What is the type of ``Type``?
191198====================================================================
192199
@@ -198,8 +205,9 @@ cannot be specified explicitly. The REPL command ``:type Type 1`` will
198205result in an error, as will attempting to specify the universe level
199206of any type.
200207
208+
201209Why does Idris use ``Double`` instead of ``Float64``?
202−===================================================================================
210+=====================================================
203211
204212Historically the C language and many other languages have used the
205213names ``Float`` and ``Double`` to represent floating point numbers of
@@ -215,6 +223,7 @@ choice by the developers of Idris, Idris uses the C style convention.
215223That is, the name ``Double`` is used to describe double precision
216224numbers, and Idris does not support 32 bit floats at present.
217225
226+
218227What is -ffreestanding?
219228=======================
220229
@@ -230,6 +239,7 @@ Example::
230239
231240 IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
232241
242+
233243What does the name ‘Idris’ mean?
234244================================
235245
@@ -237,6 +247,42 @@ British people of a certain age may be familiar with this
237247`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
238248that doesn’t help, maybe you can invent a suitable acronym :-) .
239249
250+
251+Will there be support for Unicode characters for operators?
252+===========================================================
253+
254+There are several reasons why we should not support Unicode operators:
255+
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.
278+
279+This seems like an instance of `Wadler's
280+Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
281+
282+This answer is based on Edwin Brady's response in the following
283+`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`__.
284+
285+
240286Where can I find more answers?
241287==============================
242288