Formally proving FizzBuzz for fun and profit, part 2.

Last time we introduced FizzBuzz and the Idris language.

The problem with our last solution (shown below) was that it combined determining what the output should be with actually creating the output strings. This time we’ll be fixing this by add Algebraic Data types and Interfaces.

fizzBuzzSimple: (x: Nat) -> String
fizzBuzzSimple x with (modNat x (the Nat 3), modNat x (the Nat 5))
  | (Z, Z) = "fizzbuzz"
  | (Z, _) = "fizz"
  | (_, Z) = "buzz"
  | _ = show x

Algebraic Data Types

Algebraic data types are types composed of other types. Think structs and enums on steroids. We want the type system to differentiate between the different possible return types (fizz, buzz, fizzbuzz and normal numbers). We acheive this in Idris with:

data FizzBuzzReturn =
   Fizz
   | Buzz
   | FizzBuzz
   | Normal Nat

This defines a new data type FizzBuzzReturn, with four cases. The Fizz, Buzz and FizzBuzz cases are just tags with no associated data. As we don’t want to have to make a case for every single non FizzBuzz number there is a Normal case which also has a single natural number associated with it. Plugging this new data type into our previous function gives:

fizzBuzzReturn: (x: Nat) -> FizzBuzzReturn
fizzBuzzReturn x with (modNat x (the Nat 3), modNat x (the Nat 5))
   | (Z, Z) = FizzBuzz
   | (Z, _) = Fizz   
   | (_, Z) = Buzz
   | _ = Normal x

By converting the different return values into different return types we’ve made the FizzBuzz logic explicit in the type system. However we’ve also created a problem, FizzBuzz expects us to print out strings, not internal data types. For that we’ll need to convert FizzBuzzReturn to strings.

Interfaces

We could just write a function to convert FizzBuzzReturns to strings, but that’s not the ludicrously over-engineered way, so we’re going to use interfaces.

Interfaces are similar to type classes in Haskell or traits in Rust. Each interface is a collection of one or more overloadable functions. Instead of specifying concrete types, functions can specify that their inputs implement a given Interface. Any type which has an implementation of that interface can then be used. Examples of interfaces are:

• Eq, which provides functions for comparing values for equality
• Ord, for a standard way of comparing values.
• Show, which is the interface we’ll be implementing.

The Show interface is the interface for converting data types to strings. It only has one function, show, defined as follows:

show : a -> String

The implementation of Show for FizzBuzzReturn is below, note the use of show for the number in normal (Show is already implemented for builtin types).

Show FizzBuzzReturn where
   show Fizz = "fizz"
   show Buzz = "buzz"
   show FizzBuzz = "fizzbuzz"
   show (Normal x) = show x

Implementing against interfaces instead of writing custom functions makes intent clear and allows easier reuse.

Putting it all together

We have successfully split the main and display logic, now to put them back together.

fizzBuzzReturnString: (x: Nat) -> String
fizzBuzzReturnString x = show(fizzBuzzReturn x)

Note how implementing the Show interface has given us a show function to use.

But does it work?

The code above (hopefully), implements FizzBuzz correctly, but we’re doing ludicrous over-engineering, “hopefully” won’t cut it. There’s nothing stopping the implementation of fizzBuzzReturn returning FizzBuzz for everything:

fizzBuzzReturn: (x: Nat) -> FizzBuzzReturn
fizzBuzzReturn x with (modNat x (the Nat 3), modNat x (the Nat 5))
  | (_, _) = FizzBuzz
 

The normal way to catch these kinds of bugs is by writing tests, but fizzBuzzReturn has literally infinite possible different inputs. We could write a handful of test and call it a day but that’s not the point of this series.

Next time we’ll look at making the Idris compiler do our testing for us, not just for a handful of inputs, but for all possible inputs.