Using `Data.Reflection`

has some runtime costs. Notably, there can be no inlining or unboxing of reified values. I think it would be nice to add a GHC special to support it.

## The problem

The following is a somewhat modified version of the main idea in `Data.Reflection`

, with some relatively minor changes to clean up the very core of it.

-- Edward Kmett found these were necessary for his library, so they're likely necessary here too, for now. {-# OPTIONS_GHC -fno-cse #-} {-# OPTIONS_GHC -fno-full-laziness #-} {-# OPTIONS_GHC -fno-float-in #-} newtype Tagged s a = Tagged { unTagged :: a } unproxy :: (Proxy s -> a) -> Tagged s a unproxy f = Tagged (f Proxy) class Reifies s a | s -> a where reflect' :: Tagged s a -- For convenience reflect :: forall s a proxy . Reifies s a => proxy s -> a reflect _ = unTagged (reflect' :: Tagged s a) -- The key function--see below regarding implementation reify' :: (forall s . Reifies s a => Tagged s r) -> a -> r -- For convenience reify :: a -> (forall s . Reifies s a => Proxy s -> r) -> r reify a f = reify' (unproxy f) a

The key idea of `reify'`

is that something of type

forall s . Reifies s a => Tagged s r

is represented in memory exactly the same as a function of type `a -> r`

.

We currently use `unsafeCoerce`

to interpret one as the other. Following the general approach of the library, we can do this as such:

newtype Magic a r = Magic (forall s . Reifies s a => Tagged s r) reify' :: (forall s . Reifies s a => Tagged s r) -> a -> r reify' f = unsafeCoerce (Magic f)

This certainly works. The trouble is that any knowledge about what is reflected goes unused. For instance, if I write

reify 12 $ \p -> reflect p + 3

then GHC will not see, at compile time, that the result is 15. If I write

reify (+1) $ \p -> reflect p x

then GHC will never inline the application of `(+1)`

. Etc. It appears that the `forall s`

in `Magic`

gums up the inliner somehow.

### A larger example of the problem

mpickering asked for a more substantial example, so here's one:

newtype M s = M {getM :: Int} mkM :: Reifies s Int => Int -> M s mkM = normalize . M {-# INLINE mkM #-} instance Reifies s Int => Num (M s) where M x + M y = normalize (M (x + y)) M x - M y = normalize (M (x - y)) M x * M y = normalize (M (x * y)) abs x = x signum x = 1 fromInteger = mkM . fromIntegral {-# INLINE (+) #-} normalize :: Reifies s Int => M s -> M s normalize m@(M x) = M $ x `mod` reflect m {-# INLINE normalize #-} unInt :: Int -> Int# unInt (I# x) = x {-# INLINE unInt #-} test1 :: Int# -> Int# -> Int# -> Int# test1 m x y = unInt $ reify (I# m) $ \(_ :: Proxy s) -> getM $ (mkM (I# x) + mkM (I# y) :: M s)

Ideally, `test1`

should never have to box anything, but because nothing inlines, we get this rather unsatisfactory result:

test1 :: Int# -> Int# -> Int# -> Int# test1 = \ (m_a15J :: Int#) (x_a15K :: Int#) (y_a15L :: Int#) -> case ((\ (@ s_i1kJ) ($dReifies_i1kK :: Reifies s_i1kJ Int) -> case $dReifies_i1kK `cast` ... of _ { I# ww1_a1sH -> case ww1_a1sH of wild_a1sJ { __DEFAULT -> case modInt# x_a15K wild_a1sJ of ww2_a2ov { __DEFAULT -> case modInt# y_a15L wild_a1sJ of ww4_X2pz { __DEFAULT -> case modInt# (+# ww2_a2ov ww4_X2pz) wild_a1sJ of ww5_X2pH { __DEFAULT -> I# ww5_X2pH } } }; -1# -> test2; 0# -> case divZeroError of wild1_00 { } } }) `cast` ...) (I# m_a15J) of _ { I# x1_a15I -> x1_a15I }

## Principles

Any solution should be informed by these principles:

- It is highly desirable that the result is expressible in Core, without further extensions.

- It should work regardless of whether single-method classes are represented by a newtype or a data type. e.g. Using a data type would allow us to use call-by-value for all constraint arguments, which is quite attractive.

## Solutions

We basically want something that looks a fair bit like `reify'`

, but that translates to safe coercions in Core.

### Class/deriving-based

Simon Peyton Jones suggests making `reify#`

a class method and using the class deriving mechanism to ensure safety. This is the natural thing to do, because the implementation of `reify#`

varies by class (at least if we satisfy principle (2)), and isn't possible at all for multi-method classes. So `reify#`

is overloaded just like `(+)`

is: its implementation varies by type, and is only available at all for some types. *This is precisely what type classes are for''.
*

His first choice thus far seems to be

class Reifiable (a :: *) where type RC a :: Constraint reify# :: (RC a => r) -> a -> r

but he also mentions an alternative class design, which I'll rename for clarity:

class ReflectableTF (c :: Constraint) where type RL c :: * reify# :: (c => r) -> RL c -> r

`Reifiable`

seems to have reasonably good ergonomics, but it seems a bit odd to me for the payload type to determine the class. Furthermore, it's not at all clear to me how the class could be *named* in the `deriving`

clause. `ReflectableTF`

strikes me as rather better behaved, but it has fairly bad ergonomics (it requires explicit type application to pin down `c`

when calling `reify#`

).

One last class-based option I think might be worthy of consideration is to use `Reflectable`

with a data family:

class ReflectableDF (c :: Constraint) where data RL c :: * reify# :: (c => r) -> RL c -> r

This offers much better inference than `ReflectableTF`

, because the instance is selected by the second argument to `reify#`

. The constructor name could be chosen by the deriving mechanism to match the class name, so we'd get, e.g.,

instance ReflectableDF (Typeable a) where newtype RL (Typeable a) = Typeable (TypeRep a) reify# f = ...

**SLPJ** Oh, I like this!

**Iceland_jack** This could be levity-polymorphic (`RC :: TYPE rep -> Constraint`

, `RL :: Constraint -> TYPE rep`

)

### Non-class-based

I'm personally reluctant to commit to any particular class-based solution before it's been tried out in user-space. None of them are perfect, and we don't know for sure which will work out best in practice. My current thinking is that perhaps the best way to *start* is to add a `reify#`

function

reify# :: (c => r) -> a -> r

with a special typing rule: `reify# @ c r a`

will only be accepted by the type checker if `c`

is a single-method class whose method has the same representation as `a`

.

**SPJ**: I don't like this much

- The type of reify#, as written, is obviously too polymorphic!
- It's a new typing rule, i.e. an extension to COre
- You cannot use
`reify#`

in a polymorphic situation - It does not satisfy principle (2)