Idris for Non-Programmers: Part 1

Posted on July 13, 2017
Tags:

Welcome to Idris for Non-Programmers! I’ve always wanted to help people learn my favourite programming language, Idris, but almost all of the other tutorials I’ve seen are aimed at people who already know not only programming, but a specific kind of programming, as well as a bunch of maths.

This tutorial assumes only the following:

If something here isn’t clear to you, or you need help with any of it for any reason, feel free to contact me (my email address can be found here).

Why learn programming?

Programming is all about expressing ideas. Firstly, you want to express ideas to the computer - if you can get the computer to understand what you want, you can create a program that does stuff! Secondly, you want to express ideas to other people - if other people can understand what you’ve expressed, then they can help you, and you can help them.

Ultimately, programming allows you to get your computer to:

Why learn Idris?

Idris gives you the qualities of other programming languages, but also:

Old version

One idea I’ve had for a while is to make some tutorials for the programming language Idris. I love idris, but it’s very hard to get into - all the tutorials I can find for the language assume that you already know not only programming, but a specific kind of programming, and also understand a whole bunch of maths. This tutorial is different.

This tutorial assumes that you know very little - that you can use your computer, understand basic arithmetic (plus, minus, times, divide) and are willing to learn. The biggest challenge is actually installing the language. It can be hard to install, depending on your computer, but luckily I have made some instructions for you!

You’ll also need a text editor - if you’re not following my installation instructions, see the appendix for details.

If you need any help with anything related to this tutorial or installing idris, send me an email (my address can be found here)!

What is programming?

Programming is all about expressing ideas, in 2 different ways:

We need to achieve both of these goals. If a person can’t understand you, then it’s going to be very hard for you - no-one can assist you if you have problems, and you can’t collaborate with anyone else. If the computer can’t understand you, it won’t be able to turn what you wrote into a program.

In the early days, programming was done with machine code - a language computers can understand, but almost incomprehensible to people. Machine code is just a sequence of numbers that tells the computer to do very small tasks. We don’t want to write machine code because it’s very hard for people to understand, and it’s also very easy to make a mistake - there’s nothing to help you if you make an error.

After these trying times, people started to make programming languages, with the goal to allow humans to easily read and write code. “Code” means “the human readable text that defines a program”. Unfortunately, computers can only understand machine code, so all code written in the idris language (or any other language) must be converted to machine code before it can be used as a program.

Early programming languages were often complicated and difficult, and it was easy to make a mistake in them. But over time, people have been creating languages that are more readable, and can catch more and more mistakes before they cause problems. Idris is, to a certain extent, the culmination of these efforts.

Your First Idris Code

I’m assuming you’ve managed to set up idris at this point. If you haven’t installed it yet, that’s ok! You can still keep reading - however, the best way to learn something new is with practice.

If you do have it installed, I want you to make a file called MyFirstIdris.idr and open it in a text editor (not a word processor - idris code has no bold text, or fonts. Trying to add those would just confuse the computer). If you don’t have a text editor, see the appendix.

Write the following into the file:

x : Integer
x = 5

Load this up into idris by first launching idris. You should see something like this:

     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris>

Then type :load path/to/MyFirstIdris.idr (where path/to/MyFirstIdris.idr is the full filename (including folders and drives)) to load the file. On most computers, you won’t have to type it all out directly, instead, you can just type :load, then a space, then drag and drop the file onto the program. Press enter to run the load command. You should see this:

Type checking ./MyFirstIdris.idr
*MyFirstIdris>

You can type various commands at the prompt. Try typing x + 3, and see what comes up. If you want to quit the interactive idris program, type :quit (or :q for short).

Let’s go over what every part of the code we typed into the file means. The most important part of this, surprisingly, is the equals symbol. The equals sign just means “any time you see the stuff to the left hand side of the equals sign, you can replace it with the stuff on the right hand side (and visa versa)”. So line 2 here means “any time you see x, you can replace it with the numeral 5”.

The important part of line 1 is the symbol ‘:’. You should read this as “is of type”, so that together the two lines can be read as:

x is of type Integer, and any time you see it you can replace it with the numeral 5

(Integer, for those who don’t know, just means “whole number”).

“But,” you ask, “what does ‘type’ mean?” Good question! Types are one of the most powerful and useful things in Idris, and we’ll be figuring them out in detail later. For now, you can consider them to be categories. The reason why you want types is that the idris program has a typechecker - a typechecker goes through any code you write, and make sure that all of the types make sense.

To demonstrate this, change the code to read the following:

-- The typechecker won't like this
fruit : Integer
fruit = "banana"

The first line, which starts with --, is a comment - these are ignored by the computer, but can be very useful for helping people understand what you’re saying.

Now reload the file in idris, by either typing :reload (:r for short) if you still have it open, or by typing idris MyFirstIdris.idr again. You should see something like this:

1
2
3
4
5
6
7
8
9

Type checking ./MyFirstIdris.idr
MyFirstIdris.idr:3:7:When checking right hand side of fruit with expected type
        Integer

Type mismatch between
        String (Type of "banana")
and
        Integer (Expected type)
Holes: Main.fruit

Blah! A huge error! What could it mean? Let’s go through it line by line:

  1. Type checking - that’s good, that’s what we want it to do
  2. An error! - This line says that it happened in the file MyFirstIdris.idr, on line 3, at the 7th character. It then says some other stuff.
  3. (continued from previous line)
  4. (blank)
  5. Aha! “Type mismatch” - This means that the type that idris was expecting to see didn’t match the type of the thing we actually wrote.
  6. The type we actually wrote was String - idris knows that anything you put in “quotes” is actually a String (a string of text, that is).
  7. and…
  8. The type idris expected - Integer. Why did it expect Integer? Because we said that fruit was going to be an Integer.
  9. Holes - a useful feature for developing a program, but not relevant right now.

To fix this error, simply change fruit : Integer to fruit : String, then reload.

We can define as many things as we want in a file:

fruit : String
fruit = "banana"

a : Integer
a = 3

b : Integer
b = a + 5

You’ll notice that in the above example, that b is defined in terms of a. Remember above, when I said that the equals sign just means “any time you see the left hand side, replace it with the right hand side”? You can just do that here.

But only defining static values is a little boring - for one thing, programs are supposed to actually do stuff, but everything we’ve written so far is just saying that this thing is the same as that thing. In Part 2, we’ll be covering how you write code that actually does stuff.

Quiz

At the end of each part, there will be a quiz - don’t worry, you’re not being marked! Having to answer questions about what you’ve learnt has been shown to make learning significantly easier - especially when you get it wrong. The important thing is to try. The answers to a quiz will be revealed at the start of the next part.

For this quiz, look at (but don’t load!) this code:

numberOne : Integer
numberOne = 3

numberTwo : Integer
numberTwo = numberOne + 3

numberThree : Integer
numberThree = numberOne - 2 + (numberTwo * 2)

numberFour : Integer
numberFour = "numberThree"

* is multiplication - unlike in paper maths, we can’t use x, because that could be the name of something.

  1. What are numberOne, numberTwo, and numberThree equal to?
  2. Would the typechecker like this code? Why/Why not?
  3. If the typechecker doesn’t like this code, what do you need to write to fix it? If it does like this code, what is numberFour equal to?

Appendix

There are hundreds upon hundreds of text editors available. You can use the editor that’s built into your computer (Notepad on Windows, TextEdit on MacOS, gEdit on Linux), but those editors don’t include colours, or any idris-based tools. Colours aren’t neccessary for idris, but they can make it a little easier. Here are some nice text editors:

Whichever one you choose, you will have to install a plugin for idris to work with them. Links to the plugins can be found here.