Dependently typed fizzbuzz with Idris

fizzbuzz.idr

%default total

-- Proofs that a value is divisible my 3 and 5 respectively
IsFizz : (k : Nat) -> Type
IsFizz k = (modNatNZ k 3 SIsNotZ = 0)

IsBuzz : Nat -> Type
IsBuzz k = (modNatNZ k 5 SIsNotZ = 0)

-- The type Fizzbuzz, one can only construct an instance of Fizz if one can provide
-- the proof that it is fizz and one that it cannot be buzz. etc.
data Fizzbuzz : (k: Nat) -> Type where
  Fizz : (k: Nat) -> IsFizz k -> Not (IsBuzz k) -> Fizzbuzz k
  Buzz : (k: Nat) -> Not (IsFizz k) -> IsBuzz k -> Fizzbuzz k
  FizzBuzz : (k: Nat) -> IsFizz k -> IsBuzz k -> Fizzbuzz k
  Normal : (k: Nat) -> Not (IsFizz k) -> Not (IsBuzz k) -> Fizzbuzz k

-- construct an instance of Fizzbuzz given a number
fizzbuzz : (k: Nat) -> Fizzbuzz k
fizzbuzz k = let isFizz = decEq (modNatNZ k 3 SIsNotZ) 0 
                 isBuzz = decEq (modNatNZ k 5 SIsNotZ) 0 in 
                 case (isFizz, isBuzz) of
                       (Yes isfizz, No notbuzz) => Fizz k isfizz notbuzz
                       (No notfizz, Yes isbuzz) => Buzz k notfizz isbuzz
                       (Yes isfizz, Yes isbuzz) => FizzBuzz k isfizz isbuzz
                       (No notfizz, No notbuzz) => Normal k notfizz notbuzz

showFizzBuzz : Nat -> String
showFizzBuzz k = case fizzbuzz k of
                  Fizz k _ _     => "fizz"
                  Buzz k _ _     => "buzz"
                  FizzBuzz k _ _ => "fizzbuzz"
                  Normal k _ _   => show k

Result of pairing session with Tom Oram https://github.com/tomphp