FizzBuzz on Type Level

gistfile1.hs

-- Run on GHC 7.4.2

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Main where


-- Type Level Natural Number

data Nat = Zero | Succ Nat

type One     = Succ Zero
type Two     = Succ One
type Three   = Succ Two
type Four    = Succ Three
type Five    = Succ Four
type Ten     = Five :+: Five
type Fifteen = Ten  :+: Five

-- Comparison for Nat

type family Cmp (m :: Nat) (n :: Nat) :: Ordering
type instance Cmp Zero     Zero     = EQ
type instance Cmp Zero     (Succ n) = LT
type instance Cmp (Succ m) Zero     = GT
type instance Cmp (Succ m) (Succ n) = Cmp m n

-- Arithmetic for Nat

type family (m :: Nat) :+: (n :: Nat) :: Nat
type instance Zero   :+: n = n
type instance Succ m :+: n = Succ (m :+: n)

type m :-: n = Minus' m n (Cmp m n)
type family   Minus' (m :: Nat) (n :: Nat) (p :: Ordering) :: Nat
type instance Minus' Zero     Zero     EQ = Zero
type instance Minus' m        Zero     GT = m
type instance Minus' (Succ m) (Succ n) GT = Minus' m n GT

type m :%: n = Mod' m n (Cmp m n)
type family Mod' (m :: Nat) (n :: Nat) (p :: Ordering) :: Nat
type instance Mod' m n EQ = Zero
type instance Mod' m n LT = m
type instance Mod' m n GT = Mod' (m :-: n) n (Cmp (m :-: n) n)

-- FizzBuzz for Nat

data Result = Fizz | Buzz | FizzBuzz | Other Nat

type FizzBuzz m = FizzBuzz' m (m :%: Fifteen)
type family FizzBuzz' (m :: Nat) (r :: Nat) :: Result
type instance FizzBuzz' m Zero     = 'FizzBuzz
type instance FizzBuzz' m (Succ n) = FizzBuzz'' m (m :%: Three)
type family FizzBuzz'' (m :: Nat) (r :: Nat) :: Result
type instance FizzBuzz'' m Zero     = Fizz
type instance FizzBuzz'' m (Succ n) = FizzBuzz''' m (m :%: Five)
type family FizzBuzz''' (m :: Nat) (r :: Nat) :: Result
type instance FizzBuzz''' m Zero     = Buzz
type instance FizzBuzz''' m (Succ n) = Other m


-- Map 'type' level value to 'value' level show string

data Proxy a = Proxy

-- type to Integer value
class IntegerType n where
  toNum :: Proxy n -> Integer

-- kind Nat
instance IntegerType Zero where
  toNum = const 0

prev :: Proxy (Succ n) -> Proxy n
prev = undefined

instance IntegerType n => IntegerType (Succ n) where
  toNum = succ . toNum . prev


-- type to String value for show
class ShowType n where
  showType :: Proxy n -> String

instance ShowType n => Show (Proxy n) where
  show = showType

instance IntegerType n => ShowType n where
  showType = show . toNum

-- kind Result
instance ShowType 'Fizz     where showType _ = "Fizz"
instance ShowType 'Buzz     where showType _ = "Buzz"
instance ShowType 'FizzBuzz where showType _ = "FizzBuzz"
instance Show (Proxy n) => ShowType ('Other n) where
  showType _ = "Other " ++ show (undefined :: Proxy n)


main :: IO ()
main = do
  print (undefined :: Proxy (FizzBuzz (Five :+: One)))
  print (undefined :: Proxy (FizzBuzz Ten))
  print (undefined :: Proxy (FizzBuzz Fifteen))
  print (undefined :: Proxy (FizzBuzz (Fifteen :+: One)))

  
-- ghci> main
-- Fizz
-- Buzz
-- FizzBuzz
-- Other 16