On Thu, Dec 22, 2016 at 4:58 PM, Edward Kmett <ekm...@gmail.com> wrote: > On Mon, Dec 12, 2016 at 1:31 PM, David Feuer <david.fe...@gmail.com> wrote: >> >> On Dec 12, 2016 1:15 PM, "Edward Kmett" <ekm...@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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
