Simon has an idea for making it safer. I suspect it's only properly safe with the "forall s", but there may be a way to at least make it specialization-safe (if not conditionally coherence-safe) without that.
On Jan 17, 2017 2:42 PM, "Edward Kmett" <ekm...@gmail.com> wrote: > That is the paper the reflection library API is based on. > > However, doing it the way mentioned in that paper (after modifying it to > work around changes with the inliner for modern GHC) is about 3 orders of > magnitude slower. We keep it around in reflection as the 'slow' path for > portability to non-GHC compilers, and because that variant can make a form > of Typeable reflection which is needed for some Exception gimmicks folks > use. > > The current approach, and the sort of variant that David is pushing above, > is basically free, as it costs a single unsafeCoerce. To make the > reflection library work in a fully type-safe manner would take 1-3 > additional wired ins that would consist of well-typed core. The stuff David > is proposing above would be more general but less safe. > > -Edward > > On Tue, Jan 17, 2017 at 10:45 AM, Simon Peyton Jones < > simo...@microsoft.com> wrote: > >> David says that this paper is relevant >> >> http://okmij.org/ftp/Haskell/tr-15-04.pdf >> >> >> >> Simon >> >> >> >> *From:* David Feuer [mailto:david.fe...@gmail.com] >> *Sent:* 14 January 2017 00:50 >> *To:* Simon Peyton Jones <simo...@microsoft.com> >> *Cc:* ghc-devs <ghc-devs@haskell.org>; Edward Kmett <ekm...@gmail.com> >> *Subject:* RE: Magical function to support reflection >> >> >> >> I need to look through a bit more of this, but explicit type application >> certainly can be avoided using Tagged. Once we get the necessary magic, >> libraries will be able to come up with whatever interfaces they like. My >> main concern about the generality of >> >> >> >> reify# :: forall r. (RC a => r) -> a -> r >> >> >> >> (as with the primop type Edward came up with) is that it lacks the >> `forall s` safety mechanism of the reflection library. Along with its key >> role in ensuring class coherence[*], that mechanism also makes it clear >> what specialization is and is not allowed to do with reified values. Again, >> I'm not sure it can mess up the simpler/more general form you and Edward >> propose, but it makes me nervous. >> >> >> >> [*] Coherence: as long as an instance of Reifies S A exists for some >> concrete S::K, users can't incoherently write a polymorphic Reifies >> instance for s::K. >> >> >> >> On Jan 13, 2017 7:33 PM, "Simon Peyton Jones" <simo...@microsoft.com> >> wrote: >> >> David, Edward >> >> Here’s my take on this thread about reflection. I’ll ignore Tagged and >> the ‘s’ parameter, and the proxy arguments, since they are incidental. >> >> I can finally see a reasonable path; I think there’s a potential GHC >> proposal here. >> >> Simon >> >> >> >> *First thing*: PLEASE let's give a Core rendering of whatever is >> proposed. If it's expressible in Core that's reassuring. If it requires an >> extension to Core, that's a whole different thing. >> >> >> >> *Second*. For any *particular* class, I think it's easy to express >> reify in Core. Example (in Core): >> >> reifyTypeable :: (Typeable a => b) -> TypeRep a -> b >> >> reifyTypable k = k |> co >> >> where co is a coercion that witnesses >> >> co :: (forall a b. Typeable a => b) ~ forall a b. (TypeRep a -> b) >> >> >> >> *Third. *This does not depend, and should not depend, on the fact that >> single-method classes are represented with a newtype. E.g. if we changed >> Typeable to be represented with a data type thus (in Core) >> >> data Typeable a = MkTypeable (TypeRep a) >> >> using data rather than newtype, then we could still write reifyTypable. >> >> reifyTypeable :: (Typeable a => b) -> TypeRep a -> b >> >> reifyTypable = /\ab. \(f :: Typeable a => b). \(r :: TypeRep a). >> >> f (MkTypeable r) >> >> The efficiency of newtype is nice, but it’s not essential. >> >> >> >> *Fourth*. As you point out, reify# is far too polymorphic. *Clearly >> you need reify# to be a class method!* Something like this >> >> class Reifiable a where >> >> type RC a :: Constraint -- Short for Reified Constraint >> >> reify# :: forall r. (RC a => r) -> a -> r >> >> Now (in Core at least) we can make instances >> >> instance Reifiable (TypeRep a) where >> >> type RC (TypeRep a) = Typeable a >> >> reify# k = k |> co -- For a suitable co >> >> Now, we can’t write those instances in Haskell, but we could make the >> ‘deriving’ mechanism deal with it, thus: >> >> deriving instance Reifiable (Typeable a) >> >> You can supply a ‘where’ part if you like, but if you don’t GHC will fill >> in the implementation for you. It’ll check that Typeable is a >> single-method class; produce a suitable implementation (in Core, as above) >> for reify#, and a suitable instance for RC. Pretty simple. Now the solver >> can use those instances. >> >> There are lots of details >> >> · I’ve used a single parameter class and a type function, because >> the call site of reify# will provide no information about the ‘c’ in (c => >> r) argument. >> >> · What if some other class has the same method type? E.g. if >> someone wrote >> >> class MyTR a where op :: TypeRep a >> >> would that mess up the use of reify# for Typeable? Well it would if >> they also did >> >> deriving instance Reifiable (MyTR a) >> >> And there really is an ambiguity: what should (reify# k (tr :: TypeRep >> Int)) do? Apply k to a TypeRep or to a MyTR? So a complaint here would be >> entirely legitimate. >> >> · I suppose that another formulation might be to abstract over >> the constraint, rather than the method type, and use explicit type >> application at calls of reify#. So >> >> class Reifiable c where >> >> type RL c :: * >> >> reify# :: (c => r) -> RL c -> r >> >> Now all calls of reify# would have to look like >> >> reify# @(Typeable Int) k tr >> >> Maybe that’s acceptable. But it doesn’t seem as nice to me. >> >> · One could use functional dependencies and a 2-parameter type >> class, but I don’t think it would change anything much. If type functions >> work, they are more robust than fundeps. >> >> · One could abstract over the type constructor rather than the >> type. I see no advantage and some disadvantages >> >> class Reifiable t where >> >> type RC t :: * -> Constraint -- Short for Reified Constraint >> >> reify# :: forall r. (RC t a => r) -> t a -> r >> >> >> >> >> >> | -----Original Message----- >> >> | From: ghc-devs [mailto:ghc-devs-boun...@haskell.org >> <ghc-devs-boun...@haskell.org>] On Behalf Of David >> >> | Feuer >> >> | Sent: 11 December 2016 05:01 >> >> | To: ghc-devs <ghc-devs@haskell.org>; Edward Kmett <ekm...@gmail.com> >> >> | Subject: Magical function to support reflection >> >> | >> >> | The following proposal (with fancier formatting and some improved >> >> | wording) can be viewed at >> >> | https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport >> >> | >> >> | Using the Data.Reflection has some runtime costs. Notably, there can >> be no >> >> | inlining or unboxing of reified values. I think it would be nice to >> add a >> >> | GHC special to support it. I'll get right to the point of what I want, >> and >> >> | then give a bit of background about why. >> >> | >> >> | === What I want >> >> | >> >> | I propose the following absurdly over-general lie: >> >> | >> >> | reify# :: (forall s . c s a => t s r) -> a -> r >> >> | >> >> | `c` is assumed to be a single-method class with no superclasses whose >> >> | dictionary representation is exactly the same as the representation of >> `a`, >> >> | and `t s r` is assumed to be a newtype wrapper around `r`. In >> desugaring, >> >> | reify# f would be compiled to f@S, where S is a fresh type. I believe >> it's >> >> | necessary to use a fresh type to prevent specialization from mixing up >> >> | different reified values. >> >> | >> >> | === Background >> >> | >> >> | Let me set up a few pieces. These pieces are slightly modified from >> what the >> >> | package actually does to make things cleaner under the hood, but the >> >> | differences are fairly shallow. >> >> | >> >> | newtype Tagged s a = Tagged { unTagged :: a } >> >> | >> >> | unproxy :: (Proxy s -> a) -> Tagged s a >> >> | unproxy f = Tagged (f Proxy) >> >> | >> >> | class Reifies s a | s -> a where >> >> | reflect' :: Tagged s a >> >> | >> >> | -- For convenience >> >> | reflect :: forall s a proxy . Reifies s a => proxy s -> a reflect _ = >> >> | unTagged (reflect' :: Tagged s a) >> >> | >> >> | -- The key function--see below regarding implementation reify' :: >> (forall s >> >> | . Reifies s a => Tagged s r) -> a -> r >> >> | >> >> | -- For convenience >> >> | reify :: a -> (forall s . Reifies s a => Proxy s -> r) -> r reify a f = >> >> | reify' (unproxy f) a >> >> | >> >> | The key idea of reify' is that something of type >> >> | >> >> | forall s . Reifies s a => Tagged s r >> >> | >> >> | is represented in memory exactly the same as a function of type >> >> | >> >> | a -> r >> >> | >> >> | So we can currently use unsafeCoerce to interpret one as the other. >> >> | Following the general approach of the library, we can do this as such: >> >> | >> >> | newtype Magic a r = Magic (forall s . Reifies s a => Tagged s r) >> reify' :: >> >> | (forall s . Reifies s a => Tagged s r) -> a -> r reify' f = >> unsafeCoerce >> >> | (Magic f) >> >> | >> >> | This certainly works. The trouble is that any knowledge about what is >> >> | reflected is totally lost. For instance, if I write >> >> | >> >> | reify 12 $ \p -> reflect p + 3 >> >> | >> >> | then GHC will not see, at compile time, that the result is 15. If I >> write >> >> | >> >> | reify (+1) $ \p -> reflect p x >> >> | >> >> | then GHC will never inline the application of (+1). Etc. >> >> | >> >> | I'd like to replace reify' with reify# to avoid this problem. >> >> | >> >> | Thanks, >> >> | David Feuer >> >> | _______________________________________________ >> >> | ghc-devs mailing list >> >> | ghc-devs@haskell.org >> >> | https://na01.safelinks.protection.outlook.com/?url=http%3A% >> 2F%2Fmail.haskell >> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7C488bf00986e34ac0833208d42182c47a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636170292905032831&sdata=quvCny8vD%2Fw%2BjIIypEtungW3OWbVmCQxFAK4%2FXrX%2Bb8%3D&reserved=0> >> >> | .org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- >> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7C488bf00986e34ac0833208d42182c47a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636170292905032831&sdata=quvCny8vD%2Fw%2BjIIypEtungW3OWbVmCQxFAK4%2FXrX%2Bb8%3D&reserved=0> >> >> | devs&data=02%7C01%7Csimonpj%40microsoft.com%7C488bf00986e34a >> c0833208d42182c4 >> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7C488bf00986e34ac0833208d42182c47a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636170292905032831&sdata=quvCny8vD%2Fw%2BjIIypEtungW3OWbVmCQxFAK4%2FXrX%2Bb8%3D&reserved=0> >> >> | 7a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636170292905 >> 032831&sdata=quv >> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7C488bf00986e34ac0833208d42182c47a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636170292905032831&sdata=quvCny8vD%2Fw%2BjIIypEtungW3OWbVmCQxFAK4%2FXrX%2Bb8%3D&reserved=0> >> >> | Cny8vD%2Fw%2BjIIypEtungW3OWbVmCQxFAK4%2FXrX%2Bb8%3D&reserved=0 >> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7C488bf00986e34ac0833208d42182c47a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636170292905032831&sdata=quvCny8vD%2Fw%2BjIIypEtungW3OWbVmCQxFAK4%2FXrX%2Bb8%3D&reserved=0> >> >> >> > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
