Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML, and include:
module EvenOdd data Even : Nat -> Type where EZ : Even Z ES : Even n -> Even (S (S n)) total ee : Even n -> Even m -> Even (n + m) ee EZ m = m ee (ES n) m = ES (ee n m)
What I like about it is that I am able to solve the challenges in a TDD way working in a environment that I am familiar (my own PC not a browser IDE) and the cherry on the top of the cake is that I have access to code reviews.
These are a few of the 5 exercises on the Idris track. You can see all the exercises here.