Dependently typed FizzBuzz, about 5 years late to the party

FizzBuzz.idr

module FizzBuzz

-- Dependently-typed FizzBuzz, about 5 years late to the party.

-- A specification of the problem.  Each constructor tells the conditions
-- under which it can be applied, and the "auto" keyword means that proof
-- search will be used in the context where they are applied to fill them
-- out. For instance, applying `N` to some Nat fails unless there's a proof in
-- scope that the argument meets the criteria.
data FB : Nat -> Type where
  N        : (n : Nat) -> {auto not3 : Not (n `mod` 3 = 0)} -> {auto not5 : Not (n `mod` 5 = 0)} -> FB n
  Fizz     : (n : Nat) -> {auto div3 : n `mod` 3 = 0}       -> {auto not5 : Not (n `mod` 5 = 0)} -> FB n
  Buzz     : (n : Nat) -> {auto not3 : Not (n `mod` 3 = 0)} -> {auto div5 : n `mod` 5 = 0}       -> FB n
  FizzBuzz : (n : Nat) -> {auto div3 : n `mod` 3 = 0}       -> {auto div5 : n `mod` 5 = 0}       -> FB n

-- A function to calculate what to output for a given number. decEq leaves
-- proofs in scope (the arguments to `Yes` and `No`) that will be found by
-- proof search when applying the constructors.
fb : (n : Nat) -> FB n
fb n with (decEq (n `mod` 3) 0)
  fb n | (Yes prf)   with (decEq (n `mod` 5) 0)
    fb n | (Yes prf)   | (Yes x)     = FizzBuzz n
    fb n | (Yes prf)   | (No contra) = Fizz n
  fb n | (No contra) with (decEq (n `mod` 5) 0)
    fb n | (No contra) | (Yes prf) = Buzz n
    fb n | (No contra) | (No f)    = N n


-- An infinite stream of the natural numbers, starting at 0 and going up. Z is
-- 0, S is one plus its argument. `iterate` starts a stream with its second
-- argument, then generates each new element by applying its first argument to
-- the previous element.
nats : Stream Nat
nats = iterate S Z

--- A stream of pairs of Nats and their corresponding output. Use `tail`
--- because the problem says to start at 1.
fizzBuzz : Stream (n : Nat ** FB n)
fizzBuzz = map (\n => (n ** (fb n))) (tail nats)

-- Generate output for the screen. The type system can't help us here!
instance Show (n : Nat ** FB n) where
  show (x ** N x)        = show x
  show (x ** Fizz x)     = "Fizz"
  show (x ** Buzz x)     = "Buzz"
  show (x ** FizzBuzz x) = "FizzBuzz"

-- Take the first 100 numbers' FizzBuzzes, then print them to the screen.
namespace Main
  main : IO ()
  main = sequence_ . map (putStrLn . show) . take 100 $ fizzBuzz

Could also write [1..] to get a Stream of Nats.