@@ -0,0 +1,89 @@
1+==========================
2+Frequently Asked Questions
3+==========================
4+
5+What are the differences between Agda and Idris?
6+------------------------------------------------
7+
8+The main difference is that Idris has been designed from the start to support
9+verified systems programming through easy interoperability with C and high
10+level language constructs to support domain specific language implementation.
11+Idris emphasises general-purpose programming, rather than theorem proving, and
12+as such includes higher level programming constructs such as type classes and
13+do notation. Idris also supports tactic based theorem proving, and has a
14+lightweight Hugs/GHCI style interface.
15+
16+Why does Idris use eager evaluation rather than lazy?
17+-----------------------------------------------------
18+
19+Idris uses eager evaluation for more predictable performance, in particular
20+because one of the longer term goals is to be able to write efficient and
21+verified low level code such as device drivers and network infrastructure.
22+Furthermore, the Idris type system allows us to state precisely the type
23+of each value, and therefore the run-time form of each value. In a lazy
24+language, consider a value of type ``Int``:
25+
26+.. code-block:: idris
27+
28+ thing : Int
29+
30+What is the representation of ``thing`` at run-time? Is it a bit pattern
31+representing an integer, or is it a pointer to some code which will compute
32+an integer? In Idris, we have decided that we would like to make this
33+distinction precise, in the type:
34+
35+.. code-block:: idris
36+
37+ thing_val : Int
38+ thing_comp : Lazy Int
39+
40+Here, it is clear from the type that ``thing_val`` is guaranteed to be a
41+concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an
42+``Int``.
43+
44+How can I make lazy control structures?
45+---------------------------------------
46+
47+You can make control structures using the special Lazy type. For example,
48+``if...then...else`` is defined as follows in the library:
49+
50+.. code-block:: idris
51+
52+ boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a
53+ boolElim True t e = t
54+ boolElim False t e = e
55+
56+ syntax if [test] then [t] else [e] = boolElim test t e
57+
58+The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will
59+only be evaluated if they are used, that is, they are evaluated lazily.
60+
61+When will Idris be self-hosting?
62+--------------------------------
63+
64+It’s not a priority, though not a bad idea in the long run. It would be a
65+worthwhile effort in the short term to implement libraries to support
66+self-hosting, such as a good parsing library.
67+
68+Does Idris have Universe Polymorphism? What is the type of ``Type``?
69+--------------------------------------------------------------------
70+
71+Rather than Universe polymorphism, Idris has a cumulative hierarchy of
72+universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
73+Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
74+provided that ``n <= m``.
75+
76+What does the name ‘Idris’ mean?
77+--------------------------------
78+
79+British people of a certain age may be familiar with this
80+`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
81+that doesn’t help, maybe you can invent a suitable acronym :-) .
82+
83+Where can I find more answers?
84+------------------------------
85+
86+There is an `Unofficial FAQ
87+<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on
88+github which answers more technical questions and may be updated more often.
89+