Getting started with Idris 2
Idris is awesome functional programming language with dependent types. Version 2 is mostly backwards compatible with the previous release, but it is based on a slightly different
Quantitative Type Theory  concept. Another major change introduced is that the language is self-hosted now.
NOTE: This tutorial is written specifically for the MacOS and was tested on Big Sur 11.6 version. Although some of the commands might apply to the different platforms, please refer to the official documentation to properly install it on other systems.
There is a dependency on Racket programming language, so make sure you have downloaded and installed it first (it’s a straightforward installation using
.dmg file). Build process relies on Racket binaries, so don’t forget to make them available by adjusting your
$ export PATH=$PATH:"/Applications/Racket v8.3/bin"
Now download archive with a source code (or clone latest version from Github) alongside with installing required tools and setting proper environment variables.
$ brew update
Optionally, you can build a documentation by invoking yet another make target and opening
index.html within your browser
$ make install-libdocs
To check whether everything works properly you can launch an extensive set of unittests with the command
$ make test
The process might take a while and you should see a bunch of
success steps on the way as well as
472/472 tests successful message in the very end
In order to get autocompletion edit your
.zshrc file (or
.bashrc for Bash users)
autoload -U +X compinit && compinit # remove this line for bash
Obviously, there is no reason to install a new programming language if we are not going to write a program in it. So create a text file
hello.idr and open it in your favourite text editor
main : IO ()
Save the file, compile the program and run the resulting executable
$ idris2 hello.idr -o hello
That’s it, check this website to get started with some basic code examples in Idris or scroll down to the resources to get to tutorials and other useful links.