@@ -13,6 +13,21 @@ as such includes higher level programming constructs such as type classes and
1313do notation. Idris also supports tactic based theorem proving, and has a
1414lightweight Hugs/GHCI style interface.
1515
16+Is Idris production ready?
17+--------------------------
18+
19+Idris is primarily a research tool for exploring the possibilities of software
20+development with dependent types, meaning that the primary goal is not (yet) to
21+make a system which could be used in production. As such, there are a few rough
22+corners, and lots of missing libraries. Nobody is working on Idris full time,
23+and we don't have the resources at the moment to polish the system on our own.
24+Therefore, we don't recommend building your business around it!
25+
26+Having said that, contributions which help towards making Idris suitable
27+for use in production would be very welcome - this includes (but is not
28+limited to) extra library support, polishing the run-time system (and ensuring
29+it is robust), providing and maintaining a JVM back end, etc.
30+
1631Why does Idris use eager evaluation rather than lazy?
1732-----------------------------------------------------
1833
@@ -58,6 +73,32 @@ You can make control structures using the special Lazy type. For example,
5873The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will
5974only be evaluated if they are used, that is, they are evaluated lazily.
6075
76+Evaluation at the REPL doesn't behave as I expect. What's going on?
77+-------------------------------------------------------------------
78+
79+Being a fully dependently typed language, Idris has two phases where it
80+evaluates things, compile-time and run-time. At compile-time it will only
81+evaluate things which it knows to be total (i.e. terminating and covering all
82+possible inputs) in order to keep type checking decidable. The compile-time
83+evaluator is part of the Idris kernel, and is implemented in Haskell using a
84+HOAS (higher order abstract syntax) style representation of values. Since
85+everything is known to have a normal form here, the evaluation strategy doesn't
86+actually matter because either way it will get the same answer, and in practice
87+it will do whatever the Haskell run-time system chooses to do.
88+
89+The REPL, for convenience, uses the compile-time notion of evaluation. As well
90+as being easier to implement (because we have the evaluator available) this can
91+be very useful to show how terms evaluate in the type checker. So you can see
92+the difference between:
93+
94+.. code-block:: idris
95+
96+ Idris> \n, m => (S n) + m
97+ \n => \m => S (plus n m) : Nat -> Nat -> Nat
98+
99+ Idris> \n, m => n + (S m)
100+ \n => \m => plus n (S m) : Nat -> Nat -> Nat
101+
61102When will Idris be self-hosting?
62103--------------------------------
63104