This is a non-official tutorial for learning the Idris Language (http://www.idris-lang.org).
Idris is a functional programming language with dependent types. In the words of Edwin Brady - the creator of Idris - the goal was to create a programming language that would be like "Haskell if it had dependent types from the beginning"
That is, if you know Haskell you should have no problems with the syntax Idris.
More details about Idris can be found at
- the Idris homepage
- the github page
- the official tutorial that comes with Idris
We won't go into the details of the system requirements, installation and basic usage, since all that is explained in detail on the official pages.
We also won't go into the whys and wherefores of functional programming per se, since that also is covered elsewhere in detail.
This tutorial is mainly written to explain Idris to myself. Any errors, omissions and mistakes are entirely caused by myself.
Also note, that this is work in progress and may change at any time and also is not complete.
Many of the examples are pirated from other sources like
- Software Foundations which is an introduction to coq and dependent types
- Dependently Typed Programming in Idris: A Demo by David Raymond Christiansen
- Edwin Brady's Copenhagen talks
- and many more