Reflection

import Data.Reflection (Given (given), give)

The reflection library is used to solve the configuration problem, which is when we have some value (usually, configuration information) that must be shared between many parts of a program. Let's consider modular arithmetic as an example:

newtype Modulus = Modulus { unModulus :: Integer }

addMod :: Modulus -> Integer -> Integer -> Integer
addMod (Modulus m) a b = (a + b) `mod` m

eqMod :: Modulus -> Integer -> Integer -> Bool
eqMod (Modulus m) a b = (a `mod` m) == (b `mod` m)

Here we have implemented ordinary modular addition and equality in a simple way. We can compute elementary facts such as:

• eqMod (Modulus 3) 1 4 == True
• addMod (Modulus 3) 2 2 == 1
• ... and so on.

There are two things about this approach that are not nice:

1. We have to specify the Modulus at every function call.
2. This interface permits rather strange expressions, such as eqMod (Modulus 3) 1 (addMod (Modulus 5) 2 2). Is such an expression even well-formed? It's hard to say.

Because Haskell isn't dependently typed, values are not types, but reflection allows us to reflect values in types. Then, type class instance resolution can solve our two awkward problems by:

1. Inferring the correct value at each call site, so that we do not have to specify it every time.
2. Because we do not specify the Modulus at every call site, the risk of using different values is significantly diminished.

We alter our definitions of addMod and eqMod slightly:

addMod :: Given Modulus => Integer -> Integer -> Integer
addMod a b = (a + b) `mod` m
  where Modulus m = given @Modulus

eqMod :: Given Modulus => Integer -> Integer -> Bool
eqMod a b = (a `mod` m) == (b `mod` m)
  where Modulus m = given @Modulus

To use the modified functions, we insert a call to give above any modular arithmetic expression. For example,

• give (Modulus 3) (eqMod 1 4) == True
• give (Modulus 3) (addMod 2 2) == 1

(The parentheses around eqMod and addMod are actually optional.) We can still construct our ill-conceived expression: (give (Modulus 3) eqMod) 1 ((give (Modulus 5) addMod) 2 2) but we are unlikely to do so accidentally because we are not specifying the Modulus at every call site.

We can go further, and actually rule out the problematic expression, by introducing a phantom type parameter to Modulus and a newtype wrapper around Integer. However, this goes beyond merely demonstrating the use of Given, so we leave it as an exercise for the reader.