Magical function to support reflection

[Edward Kmett]

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.

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.)

-Edward

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20161223/24f9c74b/attachment.html>