wiki:MagicalReflectionSupport

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:

  1. It is highly desirable that the result is expressible in Core, without further extensions.
  1. 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)
Last modified 10 months ago Last modified on Jan 20, 2017 2:52:25 PM