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 fantastic in learning new languages but that is not the extent of it. If you are a "more experienced" programmer you may have encountered impostor syndrome: the idea you don't really know what you think you know. Exercism lets you solve problems and put them in the space of open feedback which is a tremendous learning opportunity to explore the depth of your own knowledge. Even if you have been programming in a language for awhile it is worth checking into Exercism to see where you stand with current implementation practices.
These are a few of the 5 exercises on the Idris track. You can see all the exercises here.