Idris is a:
functional programming language, supporting expressions and functions;
Dependent types enables types to depend on values which we use to reason about code. Again, CS886 delves into this aspect of Idris.
pure language, which means we are not free to communication with the outside world at will; if we wish to communicate with the outside world (i.e. printing and reading) then we have to do so under controlled conditions;
total language, which means that the compiler is equipped with various checkers to reason about program execution, namely, coverage and totality. We will look at what coverage is when we look at pattern matching. The totality checker, will check to see if your programmes are likely to terminate, and will prevent you from compiling partial programmes. (We can control what Idris checks.)
statically typed, meaning types are checked at compile time; although Idris has type inference in is limited due to dependent types;
Idris’ syntax ostensibly takes from the Haskell-family of languages, with differences here and there. Where possible we will explain the differences.
Idris uses:
- single line comments marked
--; - block comments starting with
{--};
Idris is a compiled language, meaning we compile our programs down to an executable from which we can run our programs. A very cool feature of Idris is that it supports multi-language code generation, enabling Idris programs to be ‘compiled’ down to different languages. For example, the Idris compiler can create versions of your program in Chez Scheme, Racket, Javascript, Java, PHP, and Python.
As a language, Idris is relatively simple. The compiler, and other features of the language implementation, however, is rich with functionality. We will not explore all of what Idris has to offer here. Any features required for this course, that are not documented here, will be introduced as required.