The reflection package


Slides are in English, talk will be in Japanese. Just interrupt me when you have a question.

The problem

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?

Encoding Bools

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

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


Thank you for listening.