git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/docs/faq/faq.rst
161 lines 7.0 kB history raw
1**************************
2Frequently Asked Questions
3**************************
5What are the differences between Agda and Idris?
6================================================
8The main difference is that Idris has been designed from the start to support
9verified systems programming through easy interoperability with C and high
10level language constructs to support domain specific language implementation.
11Idris emphasises general-purpose programming, rather than theorem proving, and
12as such includes higher level programming constructs such as type classes and
13do notation. Idris also supports tactic based theorem proving, and has a
14lightweight Hugs/GHCI style interface.
16Is Idris production ready?
17==========================
19Idris is primarily a research tool for exploring the possibilities of software
20development with dependent types, meaning that the primary goal is not (yet) to
21make a system which could be used in production. As such, there are a few rough
22corners, and lots of missing libraries. Nobody is working on Idris full time,
23and we don't have the resources at the moment to polish the system on our own.
24Therefore, we don't recommend building your business around it!
26Having said that, contributions which help towards making Idris suitable
27for use in production would be very welcome - this includes (but is not
28limited to) extra library support, polishing the run-time system (and ensuring
29it is robust), providing and maintaining a JVM back end, etc.
31Why does Idris use eager evaluation rather than lazy?
32=====================================================
34Idris uses eager evaluation for more predictable performance, in particular
35because one of the longer term goals is to be able to write efficient and
36verified low level code such as device drivers and network infrastructure.
37Furthermore, the Idris type system allows us to state precisely the type
38of each value, and therefore the run-time form of each value. In a lazy
39language, consider a value of type ``Int``:
41.. code-block:: idris
43 thing : Int
45What is the representation of ``thing`` at run-time? Is it a bit pattern
46representing an integer, or is it a pointer to some code which will compute
47an integer? In Idris, we have decided that we would like to make this
48distinction precise, in the type:
50.. code-block:: idris
52 thing_val : Int
53 thing_comp : Lazy Int
55Here, it is clear from the type that ``thing_val`` is guaranteed to be a
56concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an
57``Int``.
59How can I make lazy control structures?
60=======================================
62You can make control structures using the special Lazy type. For example,
63``if...then...else`` is defined as follows in the library:
65.. code-block:: idris
67 boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a
68 boolElim True t e = t
69 boolElim False t e = e
71 syntax if [test] then [t] else [e] = boolElim test t e
73The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will
74only be evaluated if they are used, that is, they are evaluated lazily.
76Evaluation at the REPL doesn't behave as I expect. What's going on?
77===================================================================
79Being a fully dependently typed language, Idris has two phases where it
80evaluates things, compile-time and run-time. At compile-time it will only
81evaluate things which it knows to be total (i.e. terminating and covering all
82possible inputs) in order to keep type checking decidable. The compile-time
83evaluator is part of the Idris kernel, and is implemented in Haskell using a
84HOAS (higher order abstract syntax) style representation of values. Since
85everything is known to have a normal form here, the evaluation strategy doesn't
86actually matter because either way it will get the same answer, and in practice
87it will do whatever the Haskell run-time system chooses to do.
89The REPL, for convenience, uses the compile-time notion of evaluation. As well
90as being easier to implement (because we have the evaluator available) this can
91be very useful to show how terms evaluate in the type checker. So you can see
92the difference between:
94.. code-block:: idris
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
102When will Idris be self-hosting?
103================================
105It’s not a priority, though not a bad idea in the long run. It would be a
106worthwhile effort in the short term to implement libraries to support
107self-hosting, such as a good parsing library.
109Does Idris have Universe Polymorphism? What is the type of ``Type``?
110====================================================================
112Rather than Universe polymorphism, Idris has a cumulative hierarchy of
113universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
114Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
115provided that ``n <= m``.
117Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
118===================================================================================
120Historically the C language and many other languages have used the
121names ``Float`` and ``Double`` to represent floating point numbers of
122size 32 and 64 respectivly. Newer languages such as Rust and Julia
123have begun to follow the naming scheme described in `IEE Standard for
124Floating-Point Arithmetic (IEEE 754)
125<http://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes
126single and double precision numbers as ``Float32`` and ``Float64``;
127the size is described in the type name.
129Due to developer familiarity with the older naming convention, and
130choice by the developers of Idris, Idris uses the C style convention.
131That is, the names ``Float`` and ``Double`` are used to describe
132single and double precision numbers.
134What is -ffreestanding?
135=======================
137The freestanding flag is used to build Idris binaries which have their
138libs and compiler in a relative path. This is useful for building binaries
139where the install directory is unknown at build time. When passing this
140flag, the IDRIS_LIB_DIR environment variable needs to be set to the path
141where the Idris libs reside relative to the idris executable. The
142IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,
143Idris will use that path to find the C compiler.
145Example:
146.. code-block::
147 IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
149What does the name ‘Idris’ mean?
150================================
152British people of a certain age may be familiar with this
153`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
154that doesn’t help, maybe you can invent a suitable acronym :-) .
156Where can I find more answers?
157==============================
159There is an `Unofficial FAQ
160<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on
161github which answers more technical questions and may be updated more often.