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 canstart 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 runningidris2 --init in the fizzbuzz project and fill in some sensible defaults. This is what I ended up with:

fizzbuzz.ipkg

package fizzbuzzauthors = "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 installmodules = Division, FizzBuzzopts = "--warnpartial"readme = "./README.md"sourcedir = "src"sourceloc = "https://gitlab.com/eleanorofs/idris-fizzbuzz.git"version = 0.0.1

The important thing here is thatmain andexecutable 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 methodnumberToFBNString 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 thedo syntax and theIO () monad.

idris-fizzbuzz-main/src/Main.idr

moduleMainimportFizzBuzzprintFizzBuzz :VectnNat->IO()printFizzBuzzNil=putStrLn""printFizzBuzz(x::xs)=doputStrLn$FizzBuzz.numberToFBNStringxprintFizzBuzzxs--recursive call on the rest of the list

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

idris-fizzbuzz-main/src/Main.idr

moduleMainimportData.Vect--imports fromListimportFizzBuzzprintFizzBuzz :VectnNat->IO()printFizzBuzzNil=putStrLn""printFizzBuzz(x::xs)=doputStrLn$FizzBuzz.numberToFBNStringxprintFizzBuzzxs--recursive call on the rest of the listtotalmain :IO()main=printFizzBuzz$fromList[1..1000]

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

Idris.ipkg files for executables

Now runidris2 --init again, but then change the values to an executable by including the main file and the executable name. Then, add yourfizzbuzzlibrary as a dependency usingdepends. You should end up with something like this:

idris-fizzbuzz-main/fizzbuzz-main.ipkg

package fizzbuzz-mainauthors = "eleanorofs"brief = "prints FizzBuzz from 1 to 1000."license = "MIT"maintainers = "eleanorofs"readme = "./README.md"-- homepage = -- sourceloc =-- bugtracker =-- packages to add to search pathdepends = fizzbuzz-- modules to installmodules = Main-- main file (i.e. file to load at REPL)main = Main-- name of executableexecutable = "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 withidris2 --build fizzbuzz-main.ipkg. This will produce abuild 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 idris2mkdirdependenciescddependenciesgit clone https://gitlab.com/eleanorofs/idris-fizzbuzzcdidris-fizzbuzzidris2--build fizzbuzz.ipkgidris2--install fizzbuzz.ipkgcd ../..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