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-bounces@haskell.org] On Behalf Of David
| Feuer
| Sent: 11 December 2016 05:01
| To: ghc-devs mailto:ghc-devs@haskell.org>; Edward Kmett mailto:ekmett@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.orgmailto:ghc-devs@haskell.org
| https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskellhttps://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%7C488bf00986e34ac0833208d42182c4https://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%7C636170292905032831&sdata=quvhttps://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=0https://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
