Idris is an experimental functional programming language with full dependent types. This tutorial is intended as a brief introduction to the language, and is aimed at readers already familiar with a functional language such as Haskell or OCaml. In particular, a certain amount of familiarity with Haskell syntax is assumed, although most concepts will at least be explained briefly.
The tutorial is, at present, more of a "crash course", intended to cover as many features as quickly as possible. Hopefully over time it will grow and include more detailed illustrative examples. Suggestions for improvements (e.g. more examples, more details, exercises) are welcome, and since the tutorial is in the darcs repository, suggestions for improvements with patches are even more welcome.
Idris is very much a work in progress, and new features are being added all the time. As a result, there are always likely to be features which are not documented here, although I will do my best to keep it up to date.
Note:This version of the tutorial requires at least Idris version
0.1.5. The only syntactic difference between this and earlier
versions is that Set, the type of types,
was rendered as # up to version 0.1.4.
Dependent types allow types to be predicated
on values. For example, rather than giving a type List
Int for lists of integers, we could be more precise and give a
type List Int n for lists of integers of
length n. As we will see throughout the tutorial, this
allows us to give much more precise types to programs, and even to
prove certain properties of programs.
The tutorial consists of a number of example programs with explanations. Each of the following chapters is generated from an Idris source file, so that you can download each one and experiment.
Further chapters will be added as time permits.
Edwin Brady -- eb@cs.st-andrews.ac.uk
29th November 2009