Re: Magical function to support reflection

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 wrote:

On Thu, Dec 22, 2016 at 4:58 PM, Edward Kmett wrote:

...

On Mon, Dec 12, 2016 at 1:31 PM, David Feuer wrote:

...

On Dec 12, 2016 1:15 PM, "Edward Kmett" 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