Improved Type-Level FizzBuzz

2018-12-28

This is a slight improvment of the code in my previous post A Preliminary Attempt at Type-Level FizzBuzz. The credit goes to my friend Shulhi Sapli. He took a look at my code and came up with a cleaner solution. This part should be straightforward if you were able to folow the code from the previous post.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind (Type)
import Data.Proxy (Proxy(..))
import GHC.TypeLits

type family IsZero (a :: Nat) :: Bool where
  IsZero 0 = 'True
  IsZero _ = 'False

type family ModRemainderIsZero (a :: Nat) (b :: Nat) where
  ModRemainderIsZero a b = IsZero (Mod a b)

type family FizzBuzz' (a :: Bool) (b :: Bool) c where
  FizzBuzz' 'True 'True _ = "FizzBuzz"
  FizzBuzz' _     'True _ = "Fizz"
  FizzBuzz' 'True _     _ = "Buzz"
  FizzBuzz' _     _     c = NatToSym c

ConcatSymbols is a type-level function to concat each Symbol with a line break in between each value. That way we can transform a list of Nat with NatToSym and ConcatSymbols into a single Symbol, turn it into a String and print it.

type family ConcatSymbols xs where
  ConcatSymbols '[] = ""
  ConcatSymbols (x ': xs) = AppendSymbol x (AppendSymbol "\n" (ConcatSymbols xs))

The nicest part is he found a solution to type-level function mapping. He got the idea from (Thinking with Types Type-Level Programming in Haskell)[http://thinkingwithtypes.com/] in chapter 10. This type-level technique is called defunctionalization, which allows for higher order type-level functions in Haskell.

type Exp a = a -> Type
type family Eval (e :: Exp a) :: a

data MapList :: (a -> Exp b) -> [a] -> Exp [b]
type instance Eval (MapList f '[]) = '[]
type instance Eval (MapList f (a ': as)) = Eval (f a) ': Eval (MapList f as)

data FizzBuzz :: Nat -> Exp Symbol
type instance Eval (FizzBuzz n) = FizzBuzz' (ModRemainderIsZero n 3) (ModRemainderIsZero n 5) n

Now we just need a list of Nats and we can map FizzBuzz and ConcatSymbols to get a Symbol. Much cleaner than the previous version.

type Nums = '[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]

type Result = ConcatSymbols (Eval (MapList FizzBuzz Nums))

main :: IO ()
main = putStr $ symbolVal (Proxy :: Proxy Result)

One thing I have not been able to do is create a working Range type-level function that takes two Nat and returns all the numbers between them in a list. The following compiles.

type family IfThenElse cond a b where
  IfThenElse 'True  a _ = a
  IfThenElse 'False _ b = b

type family Append xs y where
  Append '[] y = '[y]
  Append (x ': xs) y = x ': (Append xs y)

type family OrderToBool x where
  OrderToBool 'EQ = 'True
  OrderToBool _   = 'False

type family Range (x :: Nat) (y :: Nat) (zs :: [Nat]) :: [Nat] where
  Range x y zs =
    IfThenElse
      (OrderToBool (CmpNat x y))
      zs
      (Range (x + 1) y (Append zs x))

I want to compile and run the following, but it seems to get caught an infinite loop. The compiler suggest using the GHC flag -freduction-depth=0, but it does not seem to help. Even for small values it gets stuck.

type Result2 = ConcatSymbols (Eval (MapList FizzBuzz (Range 1 3 '[])))

main :: IO ()
main = putStr $ symbolVal (Proxy :: Proxy Result2)