The reflection package
m@kotha.net
Overview
 What problem does the package solve?
 How is it implemented?
 How is it used in ad, an automatic differentiation package?
 Note:
 Slides are in English, talk will be in Japanese. Just interrupt me when you have a question.
The problem
 The package lets you parameterize a type over values.
 Example: modular arithmetic

newtype Mod n = Mod Int
Use a type class to recover a value from a type
class ReifiesInt n where
reflect :: proxy n > Int
If n is a type encoding an integer, then reflect ([]::[n]) will be that integer.
newtype Mod n = Mod Int
instance (ReifiesInt n) => Num (Mod n) where
Mod a + Mod b = Mod (a + b `mod` reflect ([]::[n]))
...
Encoding a value into a type?
 Given (i::Int), you need to create a type (n :: *) whose ReifiesInt instance gives back i.
 (i::Int) might not be known until runtime.
Encoding Bools
 s/Int/Bool/g makes the problem much easier.
class ReifiesBool b where
reflect :: proxy b > Bool
data TrueType  Represents True
data FalseType  Represents False
instance ReifiesBool TrueType where reflect = const True
instance ReifiesBool FalseType where reflect = const False
 Given these definitions, you can encode a runtime Bool value into a type:
reify :: Bool > (forall b. ReifiesBool b => Proxy b > a) > a
reify True f = f (Proxy :: Proxy TrueType)
reify False f = f (Proxy :: Proxy FalseType)
Encoding Ints as binary numbers
 Following the same pattern, natural numbers can be encoded as a list of bits.
class ReifiesInt b where
reflect :: proxy b > Int
data Zero  represents 0
data Twice n  represents (2*n)
data TwicePlus1 n  represents (2*n+1)
instance ReifiesInt Zero where reflect = const 0
instance (ReifiesInt n) => ReifiesInt (Twice n) where
reflect _ = 2 * reflect ([]::[n])
instance (ReifiesInt n) => ReifiesInt (TwicePlus1 n) where
reflect _ = 1 + 2 * reflect ([]::[n])
Encoding Ints as binary numbers (cont.)
reify :: Int > (forall n. ReifiesInt n => Proxy n > a) > a
reify n f
 n < 0 = error "cannot reify negative number"
 n == 0 = f (Proxy :: Proxy Zero)
 mod n 2 == 0 = reify (div n 2) $
\(_::Proxy m) > f (Proxy :: Proxy (Twice m))
 otherwise = reify (div n 2) $
\(_::Proxy m) > f (Proxy :: Proxy (TwicePlus1 m))
Encoding arbitrary Haskell values
The reflection package
 The package provides the Reifies class and the reify function:
class Reifies s a  s > a where
reflect :: proxy s > a
reify :: forall a r. a > (forall s. Reifies s a => Proxy s > r) > r
 It can encode arbitrary Haskell values, but the implementation is simple.
The implementation
 It uses some knowledge about how GHC represents values at runtime.
 The second argument to reify has the following type:
Reifies s a => Proxy s > r
GHC compiles this into a function that takes a dictionary containing all the methods of Reifies s a. So in runtime, the above type is equivalent to:
DICTIONARY_Reifies s a > Proxy s > r
Moreover, a dictionary for a singlemethod class is actually a newtype of that method:
(forall proxy. proxy s > a) > Proxy s > r
Using these facts, you can unsafeCoerce the function, and give an arbitrary value as a 'dictionary' to it.
Reflection in ad
 reflection is being used to implement the Reverse mode in ad.
 The reverse mode needs to build an expression graph where each node is an arithmetic operation.
 This is implemented by accumulating nodes in a shared IORef, which is hidden inside a type variable using the reflection package.
EOF
Thank you for listening.