logo

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 [1] 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.

Installation

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 PATH variable

1
$ 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.

1
2
3
4
5
6
7
8
9
10
$ brew update
$ brew install coreutils gmp
$ curl -sSL https://www.idris-lang.org/idris2-src/idris2-0.5.1.tgz -o idris2.tgz
$ tar -xvzf idris2.tgz
$ export PREFIX=$HOME/.idris2
$ export PATH=$PATH:$PREFIX/bin
$ export DYLD_LIBRARY_PATH=$PREFIX/lib
$ export IDRIS2_CG=racket
$ make bootstrap-racket
$ make install

Optionally, you can build a documentation by invoking yet another make target and opening index.html within your browser

1
2
$ make install-libdocs
$ open `idris2 --libdir`/docs/index.html

Validating installation

To check whether everything works properly you can launch an extensive set of unittests with the command

1
$ 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

tests

Add to PATH and install autocompletion

In order to get autocompletion edit your .zshrc file (or .bashrc for Bash users)

1
2
3
autoload -U +X compinit && compinit  # remove this line for bash
autoload -U +X bashcompinit && bashcompinit
eval "$(idris2 --bash-completion-script idris2)"

Hello, World!

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

1
2
main : IO ()
main = putStrLn "Hello, World!"

Save the file, compile the program and run the resulting executable

1
2
3
$ idris2 hello.idr -o hello
$ ./build/exec/hello
Hello, World!

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.

Resources