Last time we made a function for determining which FizzBuzz variant is needed for a single number. Now we need calculate FizzBuzz for all the numbers between 1 and 100, then print them out.
Note, Idris uses monads to perform IO such as printing to stdout. If you don’t know what monads are, good luck. This will not be a monad tutorial, there are already too many bad ones out there, no need to add another. For our purposes all you need to know is that functions which return IO can do IO such as printing to the stdout and the do notation lets us sequence IO actions. For everything else monad, here is a good place to start
Who needs loops?
Idris doesn’t have for loops so we’re going to use recursion.
We’ll keep calling our fizzbuzz function with increasing numbers, starting from 1, until we get to 100.
fizzbuzz_loop: (n: Nat) -> (end: Nat) -> IO ()
fizzbuzz_loop n end = case n == end of
True => pure ()
False => do
putStrLn $ show $ fizzbuzz n
fizzbuzz_loop (S n) end
main: IO ()
main = fizzbuzz_loop 1 101The pure function creates an empty IO action.
The end, no really
We now have a formally proven implementation of FizzBuzz. Hopefully if you’ve stuck with me to then you’ve learnt a few things about Idris and formal methods along the way. Strong, expressive type systems are the future.
The full source code can be found on github here. If you do attempt to make this version of FizzBuzz in an interview, comment below on how it went.