A friend at work posted in our Slack channel that he had some fun solving FizzBuzz using typelevel 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 valuelevel 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 typelevel programming.
What does it mean by typelevel 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 typelevel function. It takes Nat
(natural numbers at typelevel) 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 typelevel 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 typelevel 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 typelevel 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
builtin type will also be promoted to kind Bool
with both 'True
and 'False
promoted to type.
Typelevel functions
Typelevel programming is not part of standard Haskell. To create typelevel 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
typelevel function provided by GHC.TypeLits
module. Here we use our IsZero
typelevel 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
typelevel 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"
Typelevel 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 typelevel 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
.
Typelevel defunctionalization
We can solve this with a technique called defunctionalization. Basically we are replacing higherorder 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 typelevel 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.