@@ -28,7 +28,7 @@ for use in production would be very welcome - this includes (but is not
28limited to) extra library support, polishing the run-time system (and ensuring
28limited to) extra library support, polishing the run-time system (and ensuring
29it is robust), providing and maintaining a JVM back end, etc.
29it is robust), providing and maintaining a JVM back end, etc.
31−Why does Idris use eager evaluation rather than lazy?
31+Why does Idris use eager evaluation rather than lazy?
32-----------------------------------------------------
32-----------------------------------------------------
34Idris uses eager evaluation for more predictable performance, in particular
34Idris uses eager evaluation for more predictable performance, in particular
@@ -110,14 +110,31 @@ Does Idris have Universe Polymorphism? What is the type of ``Type``?
110--------------------------------------------------------------------
110--------------------------------------------------------------------
112Rather than Universe polymorphism, Idris has a cumulative hierarchy of
112Rather than Universe polymorphism, Idris has a cumulative hierarchy of
113−universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
113+universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
114−Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
114+Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
115provided that ``n <= m``.
115provided that ``n <= m``.
117+Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
118+------------------------------------------------------------------------------------
120+Historically the C language and many other languages have used the
121+names ``Float`` and ``Double`` to represent floating point numbers of
122+size 32 and 64 respectivly. Newer languages such as Rust and Julia
123+have begun to follow the naming scheme described in `IEE Standard for
124+Floating-Point Arithmetic (IEEE 754)
125+<http://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes
126+single and double precision numbers as ``Float32`` and ``Float64``;
127+the size is described in the type name.
129+Due to developer familiarity with the older naming convention, and
130+choice by the developers of Idris, Idris uses the C style convention.
131+That is, the names ``Float`` and ``Double`` are used to describe
132+single and double precision numbers.
117What does the name ‘Idris’ mean?
134What does the name ‘Idris’ mean?
118--------------------------------
135--------------------------------
120−British people of a certain age may be familiar with this
137+British people of a certain age may be familiar with this
121`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
138`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
122that doesn’t help, maybe you can invent a suitable acronym :-) .
139that doesn’t help, maybe you can invent a suitable acronym :-) .
@@ -127,4 +144,3 @@ Where can I find more answers?
127There is an `Unofficial FAQ
144There is an `Unofficial FAQ
128<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on
145<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on
129github which answers more technical questions and may be updated more often.
146github which answers more technical questions and may be updated more often.