Magical function to support reflection

Simon Peyton Jones simonpj at
Sat Jan 14 00:33:46 UTC 2017

David, Edward
Here’s my take on this thread about reflection.   I’ll ignore Tagged and the ‘s’ parameter, and the proxy arguments, since they are incidental.
I can finally see a reasonable path; I think there’s a potential GHC proposal here.

First thing: PLEASE let's give a Core rendering of whatever is proposed. If it's expressible in Core that's reassuring.  If it requires an extension to Core, that's a whole different thing.

Second.  For any particular class, I think it's easy to express reify in Core.  Example (in Core):

reifyTypeable :: (Typeable a => b) -> TypeRep a -> b

reifyTypable k = k |> co
where co is a coercion that witnesses

  co :: (forall a b. Typeable a => b) ~ forall a b. (TypeRep a -> b)

Third.  This does not depend, and should not depend, on the fact that single-method classes are represented with a newtype.  E.g. if we changed Typeable to be represented with a data type thus (in Core)

data Typeable a = MkTypeable (TypeRep a)
using data rather than newtype, then we could still write reifyTypable.

reifyTypeable :: (Typeable a => b) -> TypeRep a -> b

reifyTypable = /\ab. \(f :: Typeable a => b). \(r :: TypeRep a).

               f (MkTypeable r)
The efficiency of newtype is nice, but it’s not essential.

Fourth.   As you point out, reify# is far too polymorphic. Clearly you need reify# to be a class method!  Something like this

class Reifiable a where

  type RC a :: Constraint  -- Short for Reified Constraint

  reify# :: forall r. (RC a => r) -> a -> r
Now (in Core at least) we can make instances

instance Reifiable (TypeRep a) where

  type RC (TypeRep a) = Typeable a

  reify# k = k |> co  -- For a suitable co
Now, we can’t write those instances in Haskell, but we could make the ‘deriving’ mechanism deal with it, thus:

deriving instance Reifiable (Typeable a)
You can supply a ‘where’ part if you like, but if you don’t GHC will fill in the implementation for you.  It’ll check that Typeable is a single-method class; produce a suitable implementation (in Core, as above) for reify#, and a suitable instance for RC. Pretty simple.   Now the solver can use those instances.
There are lots of details

·        I’ve used a single parameter class and a type function, because the call site of reify# will provide no information about the ‘c’ in (c => r) argument.

·        What if some other class has the same method type?  E.g. if someone wrote

class MyTR a where op :: TypeRep a

would that mess up the use of reify# for Typeable?   Well it would if they also did

deriving instance Reifiable (MyTR a)

And there really is an ambiguity: what should (reify# k (tr :: TypeRep Int)) do?  Apply k to a TypeRep or to a MyTR?  So a complaint here would be entirely legitimate.

·        I suppose that another formulation might be to abstract over the constraint, rather than the method type, and use explicit type application at calls of reify#.  So

class Reifiable c where

  type RL c :: *

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

Now all calls of reify# would have to look like

reify# @(Typeable Int) k tr

Maybe that’s acceptable.  But it doesn’t seem as nice to me.

·        One could use functional dependencies and a 2-parameter type class, but I don’t think it would change anything much.  If type functions work, they are more robust than fundeps.

·        One could abstract over the type constructor rather than the type.  I see no advantage and some disadvantages

class Reifiable t where

  type RC t :: * -> Constraint  -- Short for Reified Constraint

  reify# :: forall r. (RC t a => r) -> t a -> r

|  -----Original Message-----

|  From: ghc-devs [mailto:ghc-devs-bounces at] On Behalf Of David

|  Feuer

|  Sent: 11 December 2016 05:01

|  To: ghc-devs <ghc-devs at<mailto:ghc-devs at>>; Edward Kmett <ekmett at<mailto:ekmett at>>

|  Subject: Magical function to support reflection


|  The following proposal (with fancier formatting and some improved

|  wording) can be viewed at



|  Using the 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. I'll get right to the point of what I want, and

|  then give a bit of background about why.


|  === What I want


|  I propose the following absurdly over-general lie:


|  reify# :: (forall s . c s a => t s r) -> a -> r


|  `c` is assumed to be a single-method class with no superclasses whose

|  dictionary representation is exactly the same as the representation of `a`,

|  and `t s r` is assumed to be a newtype wrapper around `r`. In desugaring,

|  reify# f would be compiled to f at S, where S is a fresh type. I believe it's

|  necessary to use a fresh type to prevent specialization from mixing up

|  different reified values.


|  === Background


|  Let me set up a few pieces. These pieces are slightly modified from what the

|  package actually does to make things cleaner under the hood, but the

|  differences are fairly shallow.


|  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


|  So we can 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 is totally lost. 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.


|  I'd like to replace reify' with reify# to avoid this problem.


|  Thanks,

|  David Feuer

|  _______________________________________________

|  ghc-devs mailing list

|  ghc-devs at<mailto:ghc-devs at>


|  .org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-<>

|  devs&<>

|  7a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636170292905032831&sdata=quv<>

|  Cny8vD%2Fw%2BjIIypEtungW3OWbVmCQxFAK4%2FXrX%2Bb8%3D&reserved=0<>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list