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)
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:
Exercism is a great website where I was able to have some very interesting challenges.
These are a few of the 5 exercises on the Idris track. You can see all the exercises here.