I meant to define reify for the Tagged representation in terms of reify': reify :: forall a r . a -> (forall (s :: *) . Reifies s a => Proxy s -> r) -> r reify a f = reify' (unproxy f) a
Further, I figured I'd look into reifyNat, and I came up with this: reifyNat' :: forall a r . (forall (n :: Nat) . KnownNat n => Tagged n r) -> Integer -> r reifyNat' f = reify# (Constrain (unTagged (f :: Tagged n r)) :: forall (n :: Nat) . Constrain (KnownNat n) r) 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
