@@ -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,45 @@ 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
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.
281+
282+This seems like an instance of `Wadler's
283+Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
284+
285+This answer is taken from Edwin Brady's response in the following
286+`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`__.
287+
288+
240289Where can I find more answers?
241290==============================
242291