A Preliminary Attempt at Type-Level FizzBuzz

2018-12-16
haskelltype-level

FizzBuzz is a test to assess basic programming knowledge. Having done a bit of type-level programming GHC Haskell, I thought it would be a fun exercise to write FizzBuzz at the type-level.

We will use Symbols, type-level strings that support string literals, and Nats, type-level natural numbers that support unsigned integer literals.

The Language Extensions

We need a number of language extensions enabled because type-level programming is not a part of the Haskell standard.

Kinds are the types of types, DataKinds allows types defined with data to be used at the type-level. We need this to do operations on Nat and Symbol. PolyKinds allows support for type-level functions that take more than one parameter.

Use operators like + at the type-level.

TypeFamilies allows us to define type-level functions, a function that takes a type and returns a type, and we need UndecidableInstances to call a type-level function within a type-level function.

  • Proxy passes a type as a value.
  • CmpNat compares natural numbers at the type-level, returns Ordering (EQ, LT, GT).
  • symbolVal is a function that converts a Symbol, a type-level string, into a String.

You will quickly find that there are very few basic functions available for type-level programming. There is not even an if-else control structure at the type-level. 'True is a Bool constructor promoted the type-level.

Neither is there a function to convert Nat to Symbol so we need to write them by hand. For FizzBuzz we only need 1-100. I did this quickly with seq 0 100 | awk '{printf(" NatToSym %s = \"%s\"\n", $1, $1)}'.

CmpNat returns Ordering, convert 'EQ to ‘’True’ and 'GT and 'LT to 'False.

This checks if the remainder of Mod is zero or not.

At the type-level we do not have guards or let-binding, but it should be pretty straightforward. Compare this to FizzBuzz in a value-level Haskell function.

It would be nice to be able to write a Map function and apply it to a type-level list of Nats, but a type-level function (closed type family) cannot be curried. My other idea was to apply (\x -> maybe (pure ()) (\y -> print $ symbolVal (Proxy :: Proxy (FizzBuzz y))) (someNatVal x)) on [0..100], but someNatVal converts a Integer to SomeNat, which does not allow us to extract the Nat value and convert it to a Symobl. It seems like GHC needs to know the Nat type at compile time. This led me to write out each line with seq 0 100 | awk '{printf(" printSymbolVal (Proxy :: Proxy (FizzBuzz %s))\n", $1)}'

The original goal was to solve it in a more succint way, create a range of Nats at the type-level, apply FizzBuzz to each Nat and concatenate the result into a single Symbol, but the Map part was not feasible do to the lack of currying support for closed type families.