<div dir="ltr">I wasn't referring to Tagged itself being evil. I was referring to giving an excessively general type to reify# that can be used to generate segfaults as being evil.<div><br></div><div>The existing reify combinator doesn't have that property, but can't be used to build KnownNat and KnownSymbol dictionaries. (Hence why there are specialized combinators for those in reflection.)<div><br></div><div>-Edward</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 22, 2016 at 6:55 PM, 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"><span class="">On Thu, Dec 22, 2016 at 4:58 PM, Edward Kmett <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br>
> On Mon, Dec 12, 2016 at 1:31 PM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br>
>><br>
>> On Dec 12, 2016 1:15 PM, "Edward Kmett" <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br>
>><br>
>> A few thoughts in no particular order:<br>
>><br>
>> Unlike this proposal, the existing 'reify' itself as core can actually be<br>
>> made well typed.<br>
>><br>
>><br>
>> Can you explain this?<br>
><br>
> I mean just that. If you look at the core generated by the existing 'reify'<br>
> combinator, nothing it does is 'evil'. We're allowing it to construct a<br>
> dictionary. That isn't unsound where core is concerned.<br>
<br>
</span>So what *is* evil about my Tagged approach? Or do you just mean that<br>
the excessive polymorphism is evil? There's no doubt that it is, but<br>
the only ways I see to avoid it are to bake in a particular Reifies<br>
class, which is a different kind of evil, or to come up with a way to<br>
express the constraint that the class has exactly one method, which is<br>
Extreme Overkill.<br>
<span class=""><br>
> Where the surface language is concerned the uniqueness of that dictionary is<br>
> preserved by the quantifier introducing a new type generatively in the local<br>
> context, so the usual problems with dictionary construction are defused.<br>
<br>
</span><span class="">>>  On the other other hand, if you're going to be magic, you might as well<br>
>> go all the way to something like:<br>
>><br>
>> reify# :: (p => r) -> a -> r<br>
>><br>
>><br>
>> How would we implement reify in terms of this variant?<br>
><br>
> That I don't have the answer to. It seems like it should work though.<br>
<br>
</span>I think it does. I've changed the reify# type a bit to avoid an<br>
ambiguity I couldn't resolve.<br>
<br>
newtype Constrain p r = Constrain (p => r)<br>
<br>
reify# :: Constrain p r -> a -> r<br>
<br>
Using my Tagged definition of Reifies, we get<br>
<br>
reify' :: forall a r . (forall s . Reifies s a => Tagged s r) -> a -> r<br>
reify' f = reify# (Constrain (unTagged (f :: Tagged s r)) :: forall s<br>
. Constrain (Reifies s a) r)<br>
<br>
reify :: forall a r . a -> (forall s . Reifies s a => Proxy s -> r) -> r<br>
reify a f = reify# (Constrain (f (Proxy :: Proxy s)) :: forall s .<br>
Constrain (Reifies s a) r) a<br>
<br>
Using your proxy version, things are trickier, but I think it's<br>
<br>
reify :: forall a r . a -> (forall s . Reifies s a => Proxy s -> r) -> r<br>
reify a f = (reify# (Constrain (f (Proxy :: Proxy s)) :: forall s .<br>
Constrain (Reifies s a) r)) (const a :: forall proxy s . proxy s -> a)<br>
<span class="HOEnZb"><font color="#888888"><br>
David<br>
</font></span></blockquote></div><br></div>