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

Kiselyov and Shan (http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf) gives an evil technique to encode arbitrary Haskell values using StablePtr and unsafePerformIO.

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 single-method 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.