FAQ

What are the differences between Agda and Idris?

The main difference is that Idris has been designed from the start to support verified systems programming through easy interoperability with C and high level language constructs to support domain specific language implementation. Idris emphasises general-purpose programming, rather than theorem proving, and as such includes higher level programming constructs such as type classes and do notation. Idris also supports tactic based theorem proving, and has a lightweight Hugs/GHCI style interface.

Why does Idris use eager evaluation rather than lazy? How can I make lazy control structures?

Idris uses eager evaluation for more predictable performance. You can still make control structures, however, using laziness annotations. For example, if...then...else is defined as follows in the library:

boolElim : Bool -> |(t : a) -> |(e : a) -> a
boolElim True  t e = t
boolElim False t e = e

syntax if [test] then [t] else [e] = boolElim test t e

The vertical bar before the t and f arguments indicates that those arguments will only be evaluated if they are used, that is, they are evaluated lazily.

I get surprising results from the totality checker. What’s wrong?

The totality checker is known to be weak, at the moment, since it has only had a small amount of work put into it, so please don’t rely on it for anything important. Nevertheless, it is still useful to know if you find any specific bugs with it. It would be even more useful for volunteers to improve it!

I get compilation errors when trying to build Idris

You probably need to make sure the GMP and libffi libraries are installed. They are available in MacPorts and all major Linux distributions, and should install painlessly from source. On a Mac, we recommend installing both from source.

When will Idris be self-hosting?

It’s not a priority, though not a bad idea in the long run. It would be a worthwhile effort in the short term to implement libraries to support self-hosting, such as a good parsing library.

Does Idris have Universe Polymorphism? What is the type of Set?

Rather than Universe polymorphism, Idris has a cumulative hierarchy of universes; Set : Set 1, Set 1 : Set 2, etc. Cumulativity means that if x : Set n then also x : Set m, provided that n <= m.

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 .

Where can I find more answers?

There is an Unofficial FAQ on the wiki on github which answers more technical questions and may be updated more often.