@@ -13,6 +13,21 @@ as such includes higher level programming constructs such as type classes and
13do notation. Idris also supports tactic based theorem proving, and has a
13do notation. Idris also supports tactic based theorem proving, and has a
14lightweight Hugs/GHCI style interface.
14lightweight Hugs/GHCI style interface.
16+Is Idris production ready?
17+--------------------------
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!
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.
16Why does Idris use eager evaluation rather than lazy?
31Why does Idris use eager evaluation rather than lazy?
17-----------------------------------------------------
32-----------------------------------------------------
@@ -58,6 +73,32 @@ You can make control structures using the special Lazy type. For example,
58The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will
73The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will
59only be evaluated if they are used, that is, they are evaluated lazily.
74only be evaluated if they are used, that is, they are evaluated lazily.
76+Evaluation at the REPL doesn't behave as I expect. What's going on?
77+-------------------------------------------------------------------
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.
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:
96+ Idris> \n, m => (S n) + m
97+ \n => \m => S (plus n m) : Nat -> Nat -> Nat
99+ Idris> \n, m => n + (S m)
100+ \n => \m => plus n (S m) : Nat -> Nat -> Nat
61When will Idris be self-hosting?
102When will Idris be self-hosting?
62--------------------------------
103--------------------------------