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.