webbureaucrat

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

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

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.

#!/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
• [Full source for executable project)(https://gitlab.com/eleanorofs/idris-fizzbuzz-main)

I write to learn, so I welcome your constructive criticism. Report issues on GitLab.