# 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))```

# 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.