ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #2074 from jfdm/docs/faq-float-names

Browse Source 
Resolves #379 on names for floating point numbers.
This commit is contained in:
Edwin Brady 2015-03-31 00:03:53 +01:00
commit 5c8c1d316c
1 changed files with 21 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
docs/faq/faq.rst
View File

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