Idris, unlike Haskell, is strict, which has the general effect of making Idris' performance a bit more predictable, and a bit more like programming in other lan

Idris, unlike Haskell, is strict, which has the general effect of making Idris' performance a bit more predictable, and a bit more like programming in other languages. However, GHC is a phenomenal compiler, and can outperform Idris for many things; this is natural, as it's seen a lot of interest in terms of producing performant code. There are still some gotchas in Idris code. The biggest one that I can think of is indexing some type with data that doesn't manage to get erased (the usual type erasure algorithm is pretty aggressive, but it can't remove everything). Some of the most useful types for programming (as in, proving theorems about the code) are wonderfully inefficient (as an example, the inductive definition of natural number is an empty linked list - taking up plenty of space in pointers, and killing your cache whenever it's accessed - Idris knows about Nat, but not about other types). Operations on the data, which might look very efficient, can also end up operating on the indices, which might not be. Here's the docs explaining the possible hiccup with erasure: http://docs.idris-lang.org/en/latest/reference/erasure.html http://docs.idris-lang.org/en/latest/reference/erasure.html