A friend at work posted in our Slack channel that he had some fun solving FizzBuzz using type-level programming. You can read his approach here. It sounds interesting and because I am currently reading Thinking in Types, I thought it might be a good exercise to work on the same challenge.

## Goal

Obviously we want to solve FizzBuzz, but we don't want to do it the usual way. Instead of using value-level programming (if there's such a term), we want to program the solution using type mechanism only. The final outcome will look something like this,

``````f :: IO ()
f = do
print \$ symbolVal (Proxy :: Proxy (FizzBuzz 15)) -- FizzBuzz
print \$ symbolVal (Proxy :: Proxy (FizzBuzz 5))  -- Fizz
print \$ symbolVal (Proxy :: Proxy (FizzBuzz 3))  -- Buzz
``````

or we can evaluate in REPL,

``````*FizzBuzz> :kind! FizzBuzz 15
FizzBuzz 15 :: Symbol
= "FizzBuzz"
``````

We are using `Proxy` to pass the type information to `symbolVal` so that the result can be printed to screen. The computation to get the result still happen by type-level programming.

What does it mean by type-level programming?

Let's take a look at `Proxy :: Proxy (FizzBuzz 15)` . `Proxy` has a type `Proxy (FizzBuzz 15)`.

`15` here is not a value, but a type! It is a value if it is on the LHS of `::`. So does `FizzBuzz`. In fact, `FizzBuzz` is actually a type-level function. It takes `Nat` (natural numbers at type-level) as the first argument and outputs another type that represent the answer.

You can think of the compile time expansion to be like this,

``````print \$ symbolVal (Proxy :: Proxy (FizzBuzz 15)) -- The type-level function is evaluated during compile time

print \$ symbolVal (Proxy :: Proxy "FizzBuzz") -- FizzBuzz 15 is evaluated to "FizzBuzz"
``````

The key here is during compile time. Note that the string `"FizzBuzz"` in `Proxy "FizzBuzz"` is not actually a string. It is what we call type-level string which has kind `Symbol`.

## Where to start?

First of all, we need the following language features,

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

Essentially, the solution can be broken down into two operations,

• Check a number is multiple of 3 or 5, or both by getting the remainder (we can utilize mod)
• Check if the remainder is zero

We will need to implement functions to calculate the remainder and to check if it is zero. These functions need to work on type rather than value. How are we going to do that?

## Data promotion and type-level functions

### Data promotion

`DataKinds` allows type to be promoted to kind, and value to type. All positive numbers (natural numbers) when promoted are of kind `Nat`. That's the reason why `15` (from the example above) is a type, not a value since it has been promoted. The `Bool` built-in type will also be promoted to kind `Bool` with both `'True` and `'False` promoted to type.

### Type-level functions

Type-level programming is not part of standard Haskell. To create type-level function, we can make use of `TypeFamilies` extension.

``````type family IsZero (a :: Nat) :: Bool where
IsZero 0 = 'True
IsZero _ = 'False
``````
``````*FizzBuzz> :set -XDataKinds
*FizzBuzz> :kind! IsZero 5
IsZero 5 :: Bool
= 'False
*FizzBuzz> :kind! IsZero 0
IsZero 0 :: Bool
= 'True
``````

Next, we can get the remainder by using `Mod` type-level function provided by `GHC.TypeLits` module. Here we use our `IsZero` type-level function to test the remainder for zero.

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

Now, we can write our `FizzBuzz` type-level function.

``````type family FizzBuzz (a :: Nat) where
FizzBuzz a = FB (ModRemainderIsZero a 3) (ModRemainderIsZero a 5)

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

and we can use `Proxy` from `Data.Proxy` to tie all these together.

``````f :: IO ()
f = do
print \$ symbolVal (Proxy :: Proxy (FizzBuzz 15)) -- "FizzBuzz"
print \$ symbolVal (Proxy :: Proxy (FizzBuzz 5))  -- "Fizz"
print \$ symbolVal (Proxy :: Proxy (FizzBuzz 3))  -- "Buzz"
``````

## Type-level Map

That's great but we can only do `FizzBuzz` one at a time. What if we have a list of numbers that we want to apply `FizzBuzz`. That should ring a bell for you. We want to map `FizzBuzz` to `[Nat]`.

Initially, I thought this should be easy. After all, we should be type-level programming expert by now.

``````type family TypeMap (a :: Nat -> Symbol) (xs :: [Nat]) :: [Symbol]
type instance TypeMap t '[] = '[]
type instance TypeMap t (x ': xs) = t x ': TypeMap t xs

let _ = Proxy :: Proxy (TypeMap FizzBuzz [15, 3])
``````

Trying to compile this leads to error,

``````src/FizzBuzz.hs:74:20: error:
• The type family ‘FizzBuzz’ should have 1 argument, but has been given none
• In an expression type signature: Proxy (TypeMap FizzBuzz [15, 3])
In the expression: Proxy :: Proxy (TypeMap FizzBuzz [15, 3])
In a pattern binding: _ = Proxy :: Proxy (TypeMap FizzBuzz [15, 3])
|
74 |   let _ = Proxy :: Proxy (TypeMap FizzBuzz [15, 3])
|                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
``````

Why? We are passing the correct arguments to `TypeMap`. It expects `Nat -> Symbol` as the first argument and `FizzBuzz` is exactly of kind `Nat -> Symbol`. Well, IIRC you've hit the limitation of Haskell type family. Type family needs to be fully saturated. `FizzBuzz` is not fully saturated when we pass it to `TypeMap`.

### Type-level defunctionalization

We can solve this with a technique called defunctionalization. Basically we are replacing higher-order function with specialized label.

``````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 DFizzBuzz :: Nat -> Exp Symbol
type instance Eval (DFizzBuzz n) = FB (ModRemainderIsZero n 3) (ModRemainderIsZero n 5)
``````

Now we can map `FizzBuzz` to list of numbers,

``````*FizzBuzz> :kind! Eval (MapList DFizzBuzz [15, 3])
Eval (MapList DFizzBuzz [15, 3]) :: [Symbol]
= '["FizzBuzz", "Buzz"]
``````

## Wrap up

We are almost there! That type-level map works, but the return kind is `[Symbol]` and we can't use `symbolVal` to print it as it only works for `Symbol`. We need additional functions to help concatenate `[Symbol]` to `Symbol`.

``````type family ConcatSymbols xs where
ConcatSymbols '[] = ""
ConcatSymbols (x ': xs) = AppendSymbol x (AppendSymbol ", " (ConcatSymbols xs))

print \$ symbolVal (Proxy :: Proxy (ConcatSymbols (Eval (MapList DFizzBuzz [15, 3])))) -- "FizzBuzz", "Fizz"
``````

## Limitations

Astute readers will notice that our FizzBuzz is not actually complete. We are cheating a little bit here because we didn't handle one last case - the number is neither multiple of 3 or 5, in which we should print out the number.

``````type family FB (a :: Bool) (b :: Bool) where
FB 'True 'True = "FizzBuzz"
FB _ 'True     = "Fizz"
FB 'True _     = "Buzz"
FB 'False 'False = ? -- we need to return the number here
``````

We could pass `Nat` as the first argument like so,

``````type family FB (n :: Nat) (a :: Bool) (b :: Bool) where
FB 'True 'True = "FizzBuzz"
FB _ 'True     = "Fizz"
FB 'True _     = "Buzz"
FB 'False 'False = NatToSymbol n -- convert n to Symbol
``````

Well that should work if we can make such `NatToSymbol` function. Unfortunately there isn't such function and I don't have a clue  how to create such function. My friend's solution is to create such function with manual hard coded conversion, but set of natural numbers is infinite. It will take infinite amount of memory and time to cover all of the possible cases. While it somewhat solved the problem, it is not ideal.