fizzbuzz.idr

module Main

data FizzBuzz : (n: Nat) -> Type where
  Zero : FizzBuzz n
  Fizz : FizzBuzz n
  Buzz : FizzBuzz n
  Woof : FizzBuzz n
  Comb : FizzBuzz n -> FizzBuzz n -> FizzBuzz n

instance Semigroup (FizzBuzz n) where
  (<+>) a Zero = a
  (<+>) Zero b = b
  (<+>) a b    = Comb a b

instance Monoid (FizzBuzz n) where
  neutral = Zero

instance Show (FizzBuzz n) where
  show Zero = show n
  show Fizz = "fizz"
  show Buzz = "buzz"
  show Woof = "woof"
  show (Comb a b) = show a ++ show b

fizzbuzz : (n:Nat) -> FizzBuzz n
fizzbuzz n = fizz <+> buzz <+> woof where
  fizz = if mod n 3 == 0 then Fizz else neutral
  buzz = if mod n 5 == 0 then Buzz else neutral
  woof = if mod n 7 == 0 then Woof else neutral

main : IO ()
main = print $ map (\n => show $ fizzbuzz n) $ the (List _) [1..100]