Magical function to support reflection

[David Feuer]

I meant to define reify for the Tagged representation in terms of reify':

reify :: forall a r . a -> (forall (s :: *) . Reifies s a => Proxy s -> r) -> r
reify a f = reify' (unproxy f) a

Further, I figured I'd look into reifyNat, and I came up with this:

reifyNat' :: forall a r . (forall (n :: Nat) . KnownNat n => Tagged n
r) -> Integer -> r
reifyNat' f = reify# (Constrain (unTagged (f :: Tagged n r)) :: forall
(n :: Nat) . Constrain (KnownNat n) r)


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