Re: Magical function to support reflection

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. 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. Tagged in the example could be replaced with explicit type application if

backwards compatibility isn't a concern. OTOH, it is.

Would that help Core typing?

It doesn't make a difference there. The only thing is it avoids needing to make up something like Tagged.

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. and admit both fundep and TF forms. I mean, if you're going to lie you

might as well lie big.

Definitely.

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

I just want to make sure that we do what we need to get Really Good Code, if we're going to the trouble of adding compiler support.

That makes sense to me. -Edward