Frequently Asked Questions¶
What are the aims of the Idris project?¶
Idris aims to make advanced type-related programming techniques accessible to software practitioners. An important philosophy that we follow is that Idris allows software developers to express invariants of their data and prove properties of programs, but will not require them to do so.
Many of the answers in this FAQ demonstrate this philosophy, and we always bear this in mind when making language and library design decisions.
Idris is primarily a research project, led by Edwin Brady at the University of St Andrews, and has benefited from SICSA (https://www.sicsa.ac.uk) and EPSRC (https://www.epsrc.ac.uk/) funding. This does influence some design choices and implementation priorities, and means that some things are not as polished as we’d like. Nevertheless, we are still trying to make it as widely usable as we can!
Where can I find libraries? Is there a package manager?¶
We don’t yet have a package manager, but you can still find a source of libraries on the wiki: https://github.com/idris-lang/Idris2/wiki/Libraries
Fortunately, the dependencies are currently not that complicated, but we’d still like a package manager to help! There isn’t an official one yet, but two are in development:
Can Idris 2 compile itself?¶
Why does Idris 2 target Scheme? Surely a dynamically typed target language is going to be slow?¶
You may be surprised at how fast Chez Scheme is! Racket, as an alternative target, also performs well. Both perform better than the Idris 1 back end, which is written in C but has not had the decades of engineering effort by run time system specialists that Chez and Racket have. Chez Scheme also allows us to turn off run time checks, which we do.
As anecdotal evidence of the performance improvement, we compared the performance of the Idris 2 runtime with the Idris 1 runtime, using a version of the compiler built with the Chez runtime and the same version built with the bootstrapping Idris 2. On a Dell XPS 13 running Ubuntu, with the versions of 23rd May 2020, the performance was:
- Idris 2 (with the Chez Scheme runtime) checked its own source in 93 seconds.
- The bootstrapping Idris 2 (compiled with Idris 1) checked the same source in 125s.
- Idris 1 checked the bootstrapping Idris 2’s source (the same as the above, but with minor variations due to the syntax changes) in 768 seconds.
Unfortunately we can’t repeat this experiment with the latest version, since the bootstrapping Idris 2 is no longer able to build the current version.
This is, nevertheless, not intended to be a long term solution, even if it is a very convenient way to bootstrap.
Like Idris 1, Idris 2 supports plug-in code generation to allow you to write a back end for the platform of your choice.
What are the main differences between Idris 1 and Idris 2?¶
The most important difference is that Idris 2 explicitly represents erasure in types, so that you can see at compile time which function and data type arguments are erased, and which will be present at run time. You can see more details in Multiplicities.
Idris 2 has significantly better type checking performance (perhaps even an order of magnitude!) and generates significantly better code.
Also, being implemented in Idris, we’ve been able to take advantage of the type system to remove some significant sources of bugs!
You can find more details in Section Changes since Idris 1.
Why aren’t there more linearity annotations in the library?¶
In theory, now that Idris 2 is based on Quantitative Type Theory (see Section Multiplicities), we can write more precise types in the Prelude and Base libraries which give more precise usage information. We have chosen not to do that (yet) however. Consider, for example, what would happen if we did:
id : (1 _ : a) -> a id x = x
This is definitely correct, because
x is used exactly once. However, we
map : (a -> b) -> List a -> List b
We can’t guarantee that the function passed to
map is linear in its
argument in general, and so we can no longer say
map id xs since the
id doesn’t match the multiplicity of the function passed
Eventually, we hope to extend the core language with multiplicity polymorphism which will help resolve these problems. Until then, we consider linearity an experimental new feature in the type system, and therefore we follow the general philosophy that if you don’t want to use linearity, its presence mustn’t impact the way you write programs.
How do I get command history in the Idris2 REPL?¶
The Idris2 REPL does not support readline in the interest of
keeping dependencies minimal. A useful work around is to
install rlwrap, this
utility provides command history simply by invoking the Idris2
repl as an argument to the utility
The goal, eventually, is to use the IDE mode or the Idris API as the basis of an implementation of a sophisticated REPL, developed independently from the Idris 2 core. As far as we know, nobody is yet working on this: if you’re interested, please get in touch and we can help you get started!
Why does Idris use eager evaluation rather than lazy?¶
Idris uses eager evaluation for more predictable performance, in particular
because one of the longer term goals is to be able to write efficient and
verified low level code such as device drivers and network infrastructure.
Furthermore, the Idris type system allows us to state precisely the type
of each value, and therefore the run-time form of each value. In a lazy
language, consider a value of type
thing : Int
What is the representation of
thing at run-time? Is it a bit pattern
representing an integer, or is it a pointer to some code which will compute
an integer? In Idris, we have decided that we would like to make this
distinction precise, in the type:
thing_val : Int thing_comp : Lazy Int
Here, it is clear from the type that
thing_val is guaranteed to be a
thing_comp is a computation which will produce an
How can I make lazy control structures?¶
You can make control structures using the special Lazy type. For
example, one way to implement a non-dependent
would be via a function named
ifThenElse : Bool -> (t : Lazy a) -> (e : Lazy a) -> a ifThenElse True t e = t ifThenElse False t e = e
Lazy a for
e indicates that those arguments will
only be evaluated if they are used, that is, they are evaluated lazily.
By the way: we don’t actually implement
if...then...else... this way in
Idris 2! Rather, it is transformed to a
case expression which allows
Evaluation at the REPL doesn’t behave as I expect. What’s going on?¶
Being a fully dependently typed language, Idris has two phases where it evaluates things, compile-time and run-time. At compile-time it will only evaluate things which it knows to be total (i.e. terminating and covering all possible inputs) in order to keep type checking decidable. The compile-time evaluator is part of the Idris kernel, and is implemented as an interpreter in Idris. Since everything is known to have a normal form here, the evaluation strategy doesn’t actually matter because either way it will get the same answer! In practice, it uses call by name, since this avoids evaluating sub-expressions which are not needed for type checking.
The REPL, for convenience, uses the compile-time notion of evaluation. As well as being easier to implement (because we have the evaluator available) this can be very useful to show how terms evaluate in the type checker. So you can see the difference between:
Main> \n, m => S n + m \n, m => S (plus n m) Main> \n, m => n + S m \n, m => plus n (S m)
If you want to compile and execute an expression at the REPL, you can use
:exec command. In this case, the expression must have type
a, although it won’t print the result).
Why can’t I use a function with no arguments in a type?¶
If you use a name in a type which begins with a lower case letter, and which is not applied to any arguments, then Idris will treat it as an implicitly bound argument. For example:
append : Vect n ty -> Vect m ty -> Vect (n + m) ty
ty are implicitly bound. This rule applies even
if there are functions defined elsewhere with any of these names. For example,
you may also have:
ty : Type ty = String
Even in this case,
ty is still considered implicitly bound in the definition
append, rather than making the type of
append equivalent to…
append : Vect n String -> Vect m String -> Vect (n + m) String
…which is probably not what was intended! The reason for this rule is so
that it is clear just from looking at the type of
append, and no other
context, what the implicitly bound names are.
If you want to use an unapplied name in a type, you have three options. You
can either explicitly qualify it, for example, if
ty is defined in the
Main you can do the following:
append : Vect n Main.ty -> Vect m Main.ty -> Vect (n + m) Main.ty
Alternatively, you can use a name which does not begin with a lower case letter, which will never be implicitly bound:
Ty : Type Ty = String append : Vect n Ty -> Vect m Ty -> Vect (n + m) Ty
As a convention, if a name is intended to be used as a type synonym, it is best for it to begin with a capital letter to avoid this restriction.
Finally, you can turn off the automatic binding of implicits with the directive:
In this case, you can bind
m as implicits, but not
append : forall n, m . Vect n ty -> Vect m ty -> Vect (n + m) ty
Why don’t the
Monad and other interfaces include the laws?¶
On the face of it, this sounds like a good idea, because the type system allows us to specify the laws. We don’t do this in the prelude, though, for two main reasons:
- It goes against the philosophy (above) that Idris allows programmers to prove properties of their programs, but does not require it.
- A valid, lawful, implementation may not necessarily be provably lawful within the Idris system, especially if it involves higher order functions.
There are verified versions of the interfaces in
extend interfaces with laws.
I have an obviously terminating program, but Idris says it possibly isn’t total. Why is that?¶
Idris can’t decide in general whether a program is terminating due to the undecidability of the Halting Problem. It is possible, however, to identify some programs which are definitely terminating. Idris does this using “size change termination” which looks for recursive paths from a function back to itself. On such a path, there must be at least one argument which converges to a base case.
- Mutually recursive functions are supported
- However, all functions on the path must be fully applied. In particular, higher order applications are not supported
- Idris identifies arguments which converge to a base case by looking for
recursive calls to syntactically smaller arguments of inputs. e.g.
kis syntactically smaller than
S (S k)because
kis a subterm of
S (S k), but
(k, k)is not syntactically smaller than
(S k, S k).
If you have a function which you believe to be terminating, but Idris does
not, you can either restructure the program, or use the
Does Idris have universe polymorphism? What is the type of
Idris 2 currently implements
Type : Type. Don’t worry, this will not be the
case forever! For Idris 1, the FAQ answered this question as follows:
Rather than universe polymorphism, Idris has a cumulative hierarchy of
Type : Type 1,
Type 1 : Type 2, etc.
Cumulativity means that if
x : Type n and
n <= m, then
x : Type m. Universe levels are always inferred by Idris, and
cannot be specified explicitly. The REPL command
:type Type 1 will
result in an error, as will attempting to specify the universe level
of any type.
What does the name “Idris” mean?¶
British people of a certain age may be familiar with this singing dragon. If that doesn’t help, maybe you can invent a suitable acronym :-) .