Magical function to support reflection

[Edward Kmett]

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.

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