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.fe...@gmail.com> wrote: > 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
