Hello, Idris World! and Why I'm Excited for a Total Programming Language
Tags: functional, idris
Published: 2023-04-02 13:51:11

---
title: Hello, Idris World! and Why I'm Excited for a Total Programming Language
published: true
date: 2023-04-02 00:00:00 UTC
tags: [ "functional", "idris" ]
canonical_url: https://webbureaucrat.gitlab.io/articles/hello-idris-world/
---

This article represents my first attempt to get up and running with the Idris programming language. It will document not only how to make an executable Idris package but also the basics of what Idris is and why it's not like any other programming language you're likely to have used before. From a practical perspective, it will cover some basic syntax as well as how to compile and run an Idris 2 program, including .ipkg usage.

Unlike most other Idris learning resources, I will _not_ assume you already know Haskell, not least because, frankly, I don't know Haskell very well. By the way, I also don't know Idris. I'm a beginner, and, _caveat emptor_, I definitely allow for the possibility that I could get things wrong in this article. You should allow for that possibility, too, and watch out for errors on my part.

### What's the big deal about Idris programming language?

Are you the sort of person who _really_ likes static types? Do you love being able to offload the hard work of making a program actually correct onto the compiler? If so, I recommend continuing to seek more robust type systems, and the logical conclusion of that search is Idris. Idris has two (related) innovations.

The first is called **dependent types** , which means that types can be dependent on other values that we don't normally think of as being types. For example, let's say you have a list with a length represented by an integer. (This is [called a `Vect`](https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#list-and-vect) in Idris.) If the type system is aware of the length of the list, it can prevent you from accessing an index of that list outside that range at _compile time_ instead of runtime. Again, if you're the sort of person who likes a very vocal compiler that doesn't let you do bad things, this sort of feature might be appealing to you. Of course, it doesn't begin to scratch the surface of what dependent types can do for you. But this will:

The other is called a **totality checker** , which means that Idris can check that a function or program will exit with a result (without error) in a finite amount of time for every possible input. All 'exceptions' are handled. All corner cases are accounted for. This is the ultimate [liberating constraint](https://www.youtube.com/watch?v=GqmsQeSzMdw) that frees you from worrying about whether or not your program is right and allows you to focus on your business logic.

How this all works is beyond the scope of a "Hello, world" article, but if you think you're the sort of person who would enjoy **total programming**, I would encourage you to keep reading.

And so, without further ado:

### Structuring your directory in Idris

1. After installing Idris 2 on your platform of choice, make a new directory for your Idris project.
2. Make a source directory inside your project directory called _src_.
3. Open a new file in this directory. Let's call it _Main.idr_.
4. Declare the greeting module by typing `module Main` at the top. (By convention, the module name should match the file name.)

### Learning some basic syntax in Idris

Idris uses Haskell-like syntax. That means

- The type signature sits on the line above the parameter declarations.
- Functions don't enclose parameters and arguments in parentheses or separate them with commas. Instead, parameters and arguments are separated by whitespace.
- Functions definitions come after an equals sign, and whitespace is significant thereafter.

With that in mind, let's write some Idris.

The first thing we need is `putStrLn` which takes a string and returns an`IO`. IO is a monad that allows for interacting with the world outside the Idris programming language, like writing to the console. (If you need a primer on monads, I wrote this handy article on [monads for object-oriented programmers](https://webbureaucrat.gitlab.io/articles/safer-data-parsing-with-try-monads/)

_Main.idr_

```idris
module Main

main : IO () --type signature which takes no arguments and returns IO ().
main = putStrLn "Hello, world." --call `putStrLn` with the string argument.
```

If you're not familiar with Haskell or a similar language like Elm, this is very difficult to read, but don't worry. If you're having trouble reading the type signature, think of it like this:

```typescript
const main = (): IO<void> => { 
    return putStrLn("Hello, world");
}
```

(Don't get tripped up on the empty parentheses, though: they mean different things in the two examples. In Idris, they mean that the IO takes no parameters, not the function.)

### Compiling and running Idris code

If you have Idris 2 installed, you can compile this program and run it.

#### Compiling Idris source files directly

From inside your _src_ directory, run `idris2 Greeting.idr -o greeting`. If successful, this will create a new directory called, "build". You can run your program by running `./build/exec/greeting`.

#### Compiling Idris using an Idris _ipkg_ file

Idris also has an optional package configuration file which will be much more useful in most situations. Let's back out of our _src_ directory and go to our project directory to see this work.

```
package greeting
authors = "eleanorofs"
bugtracker = "https://gitlab.com/eleanorofs/idris-kata/-/issues"
executable = "greeting"
homepage = "https://gitlab.com/eleanorofs/idris-kata"
main = Main
maintainers = "eleanorofs"
opts = "--warnpartial"
readme = "./README.md"
sourcedir = "./src"
sourceloc = "https://gitlab.com/eleanorofs/idris-kata.git"
version = 0.0.1

```

This is a good starting template for an executable package. For a library package, we would not include the `executable` or the `main` properties. As you can see, the `opts` property allows for passing additional compiler options. As an example, I'm passing one which encourages totality. Most of the rest of these properties are just metadata strings.

We can compile according to this configuration using

```bash
idris2 --build greeting.ipkg
```

Our executable will still be `./build/exec/greeting`.

### Parameters in Idris

Our program isn't very interesting, though. Let's refactor this program to make it a little more flexible, and, in the process, let's learn how to declare parameters.

_Greeting.idr_

```idris
module Main

greet : String -> String -> String
greet greeting greetable = 
  greeting ++ ", " ++ greetable ++ ". "

main : IO () --type signature which takes no arguments and returns IO ().
main = 
  putStrLn (greet "Hello" "world") --call `putStrLn` with the string arguments.
```

Now we have a more robust function that can print things like, "Howdy, Idris." or "Here's looking at you, kid." More interestingly, we have our first example of declaring parameters.`String -> String -> String` can be read as, "takes a string parameter and another string parameter and returns another string."

### Dollar sign syntax for arguments in Idris

This example is trivial, but sometimes (nested (parentheses (can (get (messy))))) in languages like this, which is why we have syntactic sugars. We can use the dollar sign (`$`) to get rid of parentheses and (maybe) make our code look a little nicer.

_Main.idr_

```idris
module Main

greet : String -> String -> String
greet greeting greetable = greeting ++ ", " ++ greetable ++ ". "

main : IO () --type signature which takes no arguments and returns IO ().
main = putStrLn $ greet "Hello" "world" --call `putStrLn` with the string arguments.
```

Much better! (Well, okay, maybe not for this example, but things like this can be useful, and the dollar sign is used liberally in the Idris 2 documentation, so I thought it was important to bring up anyway.)

### and just one more little thing... totality checking in Idris!

Let's not forget what makes Idris so special. Since we've written a function we know will succeed, let's celebrate and declare it so by placing the `total`modifier above our main function.

_Main.idr_

```idris
module Main

greet : String -> String -> String
greet greeting greetable = greeting ++ ", " ++ greetable ++ ". "

total
main : IO () --type signature which takes no arguments and returns IO ().
main = putStrLn $ greet "Hello" "world" --call `putStrLn` with the string arguments.
```

This tells the compiler we think we have a total program--a program for which all paths of its behavior are defined. If the program still compiles, we know we're right about that.

### Here's hoping Idris takes off!

This article has addressed a little of:

- basic syntax
- IO monads
- package configuration
- string concatenation
- totality checking

And you know what? I think that's plenty. Let's just take a beat and not try to cover all of theorem proving or dependent types or vim keybindings in one go.

Anyway, I hope this has been helpful. As someone who loves the idea of Idris but is worried about the lack of learning resources, I feel like we're on this journey together. My faint hope is that Idris eventually becomes mainstream enough that we can use it at work and make all of our lives much easier, and while we're nowhere near that now, I know every tutorial someone cranks out gets us a little closer to that goal.

Follow [my RSS Feed](https://webbureaucrat.gitlab.io/feed/feed.xml) or [my Dev.to](https://dev.to/webbureaucrat) if you're still reading this far! This is becoming an Idris tutorial website for the forseeable future; my drafts folder is already stacked with beginner-friendly Idris tutorials.