@@ -17,6 +17,7 @@ Idris supports multiple back ends (C and JavaScript by default, with the
17ability to add more via plugins) and has a reference run time system, written
17ability to add more via plugins) and has a reference run time system, written
18in C, with a garbage collector and built-in message passing concurrency.
18in C, with a garbage collector and built-in message passing concurrency.
20Is Idris production ready?
21Is Idris production ready?
21==========================
22==========================
@@ -32,6 +33,7 @@ for use in production would be very welcome - this includes (but is not
32limited to) extra library support, polishing the run-time system (and ensuring
33limited to) extra library support, polishing the run-time system (and ensuring
33it is robust), providing and maintaining a JVM back end, etc.
34it is robust), providing and maintaining a JVM back end, etc.
35Why does Idris use eager evaluation rather than lazy?
37Why does Idris use eager evaluation rather than lazy?
36=====================================================
38=====================================================
@@ -60,6 +62,7 @@ Here, it is clear from the type that ``thing_val`` is guaranteed to be a
60concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an
62concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an
63How can I make lazy control structures?
66How can I make lazy control structures?
64=======================================
67=======================================
@@ -77,6 +80,7 @@ Booleans is defined as follows in the library:
77The type ``Lazy a`` for ``t`` and ``e`` indicates that those arguments will
80The type ``Lazy a`` for ``t`` and ``e`` indicates that those arguments will
78only be evaluated if they are used, that is, they are evaluated lazily.
81only be evaluated if they are used, that is, they are evaluated lazily.
80Evaluation at the REPL doesn't behave as I expect. What's going on?
84Evaluation at the REPL doesn't behave as I expect. What's going on?
81===================================================================
85===================================================================
@@ -156,6 +160,7 @@ letter, which will never be implicitly bound:
156As a convention, if a name is intended to be used as a type synonym, it is
160As a convention, if a name is intended to be used as a type synonym, it is
157best for it to begin with a capital letter to avoid this restriction.
161best for it to begin with a capital letter to avoid this restriction.
159I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
164I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
160=============================================================================================
165=============================================================================================
@@ -180,6 +185,7 @@ If you have a function which you believe to be terminating, but Idris does
180not, you can either restructure the program, or use the ``assert_total``
185not, you can either restructure the program, or use the ``assert_total``
183When will Idris be self-hosting?
189When will Idris be self-hosting?
184================================
190================================
@@ -187,6 +193,7 @@ It’s not a priority, though not a bad idea in the long run. It would be a
187worthwhile effort in the short term to implement libraries to support
193worthwhile effort in the short term to implement libraries to support
188self-hosting, such as a good parsing library.
194self-hosting, such as a good parsing library.
190Does Idris have universe polymorphism? What is the type of ``Type``?
197Does Idris have universe polymorphism? What is the type of ``Type``?
191====================================================================
198====================================================================
@@ -198,8 +205,9 @@ cannot be specified explicitly. The REPL command ``:type Type 1`` will
198result in an error, as will attempting to specify the universe level
205result in an error, as will attempting to specify the universe level
199of any type.
206of any type.
201Why does Idris use ``Double`` instead of ``Float64``?
209Why does Idris use ``Double`` instead of ``Float64``?
202−===================================================================================
210+=====================================================
204Historically the C language and many other languages have used the
212Historically the C language and many other languages have used the
205names ``Float`` and ``Double`` to represent floating point numbers of
213names ``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.
215That is, the name ``Double`` is used to describe double precision
223That is, the name ``Double`` is used to describe double precision
216numbers, and Idris does not support 32 bit floats at present.
224numbers, and Idris does not support 32 bit floats at present.
218What is -ffreestanding?
227What is -ffreestanding?
219=======================
228=======================
@@ -230,6 +239,7 @@ Example::
231 IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
240 IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
233What does the name ‘Idris’ mean?
243What does the name ‘Idris’ mean?
234================================
244================================
@@ -237,6 +247,45 @@ British people of a certain age may be familiar with this
237`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
247`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
238that doesn’t help, maybe you can invent a suitable acronym :-) .
248that doesn’t help, maybe you can invent a suitable acronym :-) .
251+Will there be support for Unicode characters for operators?
252+===========================================================
254+There 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
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.
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.
282+This seems like an instance of `Wadler's
283+Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
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>`__.
240Where can I find more answers?
289Where can I find more answers?
241==============================
290==============================