<div dir="ltr">A few thoughts in no particular order:<br><br>Unlike this proposal, the existing 'reify' itself as core can actually be made well typed.<br><br>Tagged in the example could be replaced with explicit type application if backwards compatibility isn't a concern. OTOH, it is.<br><div><br>The form of reify' there is actually an uncomfortable middle ground between the current implementation and perhaps the more "ghc-like" implementation that uses a type family to determine 'a'. On the other hand, giving the type above with the type family in it would be rather awkward, and generalizing it further without it would make it even more brittle. On the other other hand, if you're going to be magic, you might as well go all the way to something like:</div><div><br><span style="font-size:12.8px">reify# :: (p => r) -> a -> r<br></span><br>and admit both fundep and TF forms. I mean, if you're going to lie you might as well lie big. It'd be nice to show that this can be used to reify KnownNat, Typeable, KnownSymbol, etc. and other commonly hacked dictionaries as well as Reifies.<br><br></div><div>There are a very large number of instances out there scattered across dozens of packages that would be broken by switching from Proxy to Tagged or explicit type application internally. (I realize that this is a lesser concern that can be resolved by a major version bump and some community friction, but it does mean pragmatically that migrating to something like this would need a plan.)</div><div><br></div><div>-Edward<br><br><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Dec 11, 2016 at 12:01 AM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">The following proposal (with fancier formatting and some improved<br>
wording) can be viewed at<br>
<a href="https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/<wbr>ghc/wiki/<wbr>MagicalReflectionSupport</a><br>
<br>
Using the Data.Reflection has some runtime costs. Notably, there can<br>
be no inlining or unboxing of reified values. I think it would be nice<br>
to add a GHC special to support it. I'll get right to the point of<br>
what I want, and then give a bit of background about why.<br>
<br>
=== What I want<br>
<br>
I propose the following absurdly over-general lie:<br>
<br>
reify# :: (forall s . c s a => t s r) -> a -> r<br>
<br>
`c` is assumed to be a single-method class with no superclasses whose<br>
dictionary representation is exactly the same as the representation of<br>
`a`, and `t s r` is assumed to be a newtype wrapper around `r`. In<br>
desugaring, reify# f would be compiled to f@S, where S is a fresh<br>
type. I believe it's necessary to use a fresh type to prevent<br>
specialization from mixing up different reified values.<br>
<br>
=== Background<br>
<br>
Let me set up a few pieces. These pieces are slightly modified from<br>
what the package actually does to make things cleaner under the hood,<br>
but the differences are fairly shallow.<br>
<br>
newtype Tagged s a = Tagged { unTagged :: a }<br>
<br>
unproxy :: (Proxy s -> a) -> Tagged s a<br>
unproxy f = Tagged (f Proxy)<br>
<br>
class Reifies s a | s -> a where<br>
  reflect' :: Tagged s a<br>
<br>
-- For convenience<br>
reflect :: forall s a proxy . Reifies s a => proxy s -> a<br>
reflect _ = unTagged (reflect' :: Tagged s a)<br>
<br>
-- The key function--see below regarding implementation<br>
reify' :: (forall s . Reifies s a => Tagged s r) -> a -> r<br>
<br>
-- For convenience<br>
reify :: a -> (forall s . Reifies s a => Proxy s -> r) -> r<br>
reify a f = reify' (unproxy f) a<br>
<br>
The key idea of reify' is that something of type<br>
<br>
forall s . Reifies s a => Tagged s r<br>
<br>
is represented in memory exactly the same as a function of type<br>
<br>
a -> r<br>
<br>
So we can currently use unsafeCoerce to interpret one as the other.<br>
Following the general approach of the library, we can do this as such:<br>
<br>
newtype Magic a r = Magic (forall s . Reifies s a => Tagged s r)<br>
reify' :: (forall s . Reifies s a => Tagged s r) -> a -> r<br>
reify' f = unsafeCoerce (Magic f)<br>
<br>
This certainly works. The trouble is that any knowledge about what is<br>
reflected is totally lost. For instance, if I write<br>
<br>
reify 12 $ \p -> reflect p + 3<br>
<br>
then GHC will not see, at compile time, that the result is 15. If I write<br>
<br>
reify (+1) $ \p -> reflect p x<br>
<br>
then GHC will never inline the application of (+1). Etc.<br>
<br>
I'd like to replace reify' with reify# to avoid this problem.<br>
<br>
Thanks,<br>
David Feuer<br>
</blockquote></div><br></div>