Getting started with Idris

Idris is an experimental programming language with a lot of fancy features, most importantly dependent types and quantities. In this document I will provide basic information about how to use Idris and show what's neat about it

A note about installation

This will not cover how to install idris. For this refer to the installation instructions. There is a video tutorial about how to do it for windows.

Installing Idris can sometimes not work for a lot of various reasons, every computer is different and the team isn't big enough to catch all possible edge cases. So if you have a problem with installation, head to the idris Discord server.

Types and functions

Idris being a functional programming language it deals with two basic concepts: Types and functions.

Type tell what the program is supposed to do, functions implement what the types say:

sayHello : (personName : String) -> String
sayHello personName = "hello \{personName}!"

This is an example of a function, it takes a piece of text, which is described by the type String and returns a new piece of text. This is described by the type (name : String) -> String. Notice on the left of the arrow, the type has personName written in front of it. This is to give a name to the argument of the function. The function itself has a name sayHello. The first line sayHello : (personName : String) -> String declares the type of the function and the second line sayHello personName = "hello \{personName}!" declares the implementation of the function.

Running programs

The example above is fairly basic but actually does something, provided we can run it. For this we are going to need to do the following:

• Create a file called "Main.idr"
• Write a main function
• Compile and run our program using the Idris compiler

Create a main function

For tidiness purposes we are going to put our files in a folder, so create one and call it Tutorial. Then go inside it and create the file Main.idr. Add the line module Main at the top and then paste the code :

sayHello : (personName : String) -> String
sayHello personName = "hello \{personName}!"

Which is the same we've seen above.

Writing a main function

The main function is the one that will be called when the program starts. Just like our previous function it needs both a Type and an implementation. The type of the main function is IO (), that is the type of interactive programs. The implementation will be a program that prints the content of the text of the sayHello function into the console. For this we use the printLn (it stands for "print line") function. Here is the code:

main : IO ()
main = printLn (sayHello "Susan")

We will see later how to make those programs interactive.

Build & run our program

To see the result of our work, we need to compile our program first. This will check our program for mistakes and will generate an executable file that your computer can run. For this we need two commands:

idris2 -o main Main.idr

This will compile the program and generate the executable.

build/exec/main

This will run the program we just compiled.

If everything goes well, the line "hello Susan!" should appear on the screen.

Making our program interactive

The natural next step is to be able to write our own name and have the compter greet us! The simplest way to achieve this is to replace "Susan" by !getLine. The main function looks like this now:

main : IO ()
main = printLn (sayHello !getLine)

nb: Some of your familiar with other programing languages might have learned that ! is an operator that flip boolean values, but here it allows to combine multiple interactive programs together. We will see that later

If you run your program using the same technique as before, you will get…Nothing!

That's because the computer is waiting for you to type some text and then hit the enter key to send it to the program. So if we type

John

And hit enter, we get:

$ "hello John!"

The computer responded and gave the correct name!