Idris FizzBuzz Part IV: Main and .ipkg Files
Tags: functional, idris, totality
Published: 2023-05-26 12:54:51

---
series: "Idris FizzBuzz"
title: Idris FizzBuzz Part IV: Main and .ipkg Files
published: true
date: 2023-05-19 00:00:00 UTC
tags: ["functional", "idris", "totality"]
canonical_url: https://webbureaucrat.gitlab.io/articles/idris-fizzbuzz-part-iv-main-and-ipkg-files/
---

This is the fourth and final part of a walkthrough of FizzBuzz, a common interview problem, in Idris. If you haven't read the other parts, you can [start with Part I](https://webbureaucrat.gitlab.io/articles/idris-fizzbuzz-part-i-monads-comments-assert-smaller/). To show how to import and use libraries, we're going to divide this project into a library and an executable. Along the way, we will create _.ipkg_ packages for both.

### Idris .ipkg files for libraries

Start by running `idris2 --init` in the fizzbuzz project and fill in some sensible defaults. This is what I ended up with:

_fizzbuzz.ipkg_

```
package fizzbuzz

authors = "eleanorofs"
brief = "a fizzbuzz example in the Idris language."
bugtracker = "https://gitlab.com/eleanorofs/idris-fizzbuzz/-/issues"
-- packages to add to search path
-- depends =
-- name of executable
-- executable =
homepage = "https://gitlab.com/eleanorofs/idris-fizzbuzz"
license = "MIT"
-- main file (i.e. file to load at REPL)
-- main =
maintainers = "eleanorofs"
-- modules to install
modules = Division, FizzBuzz
opts = "--warnpartial"
readme = "./README.md"
sourcedir = "src"
sourceloc = "https://gitlab.com/eleanorofs/idris-fizzbuzz.git"
version = 0.0.1

```

The important thing here is that `main` and `executable` are not filled in because this is a library.

### Writing an Idris executable

Now we can create a new Idris package for the executable. As before, let's start with the source.

Let's recall that we have a method `numberToFBNString` which takes a single number and returns the string FizzBuzz equivalent of the number. Now, consider how we might do that recursively for a list of numbers. One way might be to combine the numbers into a long string and then print that string, but that would result in a slow-feeling user experience for large numbers as it would take a long time to concatenate the string. Instead, let's print the numbers one at a time, using the `do` syntax and the `IO ()` monad.

_idris-fizzbuzz-main/src/Main.idr_

```idris
module Main

import FizzBuzz

printFizzBuzz : Vect n Nat -> IO ()
printFizzBuzz Nil = putStrLn ""
printFizzBuzz (x :: xs) = 
  do putStrLn $ FizzBuzz.numberToFBNString x
     printFizzBuzz xs --recursive call on the rest of the list

```

Now we can write a main function which calls `printFizzBuzz` on a long vector, and we're done.

_idris-fizzbuzz-main/src/Main.idr_

```idris
module Main

import Data.Vect --imports fromList
import FizzBuzz

printFizzBuzz : Vect n Nat -> IO ()
printFizzBuzz Nil = putStrLn ""
printFizzBuzz (x :: xs) = 
  do putStrLn $ FizzBuzz.numberToFBNString x
     printFizzBuzz xs --recursive call on the rest of the list

total
main : IO ()
main = printFizzBuzz $ fromList [ 1 .. 1000 ]

```

Note that `main` is a total function! We have a strong guarantee that it will never error out.

### Idris _.ipkg_ files for executables

Now run `idris2 --init` again, but then change the values to an executable by including the main file and the executable name. Then, add your `fizzbuzz`library as a dependency using `depends`. You should end up with something like this:

_idris-fizzbuzz-main/fizzbuzz-main.ipkg_

```
package fizzbuzz-main
authors = "eleanorofs"
brief = "prints FizzBuzz from 1 to 1000."
license = "MIT"
maintainers = "eleanorofs"
readme = "./README.md"
-- homepage = 
-- sourceloc =
-- bugtracker =

-- packages to add to search path
depends = fizzbuzz

-- modules to install
modules = Main

-- main file (i.e. file to load at REPL)
main = Main

-- name of executable
executable = "fizzbuzz-main"
opts = "--warnpartial"
sourcedir = "src"
version = 0.0.1

```

### Compiling and running an Idris executable

With this configuration in place, we should be able to compile our executable with `idris2 --build fizzbuzz-main.ipkg`. This will produce a _build_ folder. We can run the executable, then, as `./build/exec/fizzbuzz-main`.

You should see, well, FizzBuzz.

If something isn't quite right, have a look at this Nix shell script which walks through all the steps needed to run this executable, including downloading and installing the previous FizzBuzz library.

```shell
#!/usr/bin/env nix-shell
#! nix-shell -i bash --pure
#! nix-shell -p bash cacert chez git idris2

mkdir dependencies
cd dependencies
git clone https://gitlab.com/eleanorofs/idris-fizzbuzz
cd idris-fizzbuzz
idris2 --build fizzbuzz.ipkg
idris2 --install fizzbuzz.ipkg
cd ../..
idris2 --build fizzbuzz-main.ipkg
./build/exec/fizzbuzz-main

```

(This is something I love about Nix--scripts themselves are not only perfectly reproducible but include self-documenting lists of dependencies.)

### Wrapping up FizzBuzz for Idris

I hope this has been a useful introduction to Idris and its basic usage and syntax. This was a fun little project for me, and, if you're reading this, I hope to see what fun little projects you write in Idris, too.

- [Full source for library project](https://gitlab.com/eleanorofs/idris-fizzbuzz)
- [Full source for executable project]([https://gitlab.com/eleanorofs/idris-fizzbuzz-main](https://gitlab.com/eleanorofs/idris-fizzbuzz-main))