Magical function to support reflection
David Feuer
david.feuer at gmail.com
Sat Jan 14 00:49:53 UTC 2017
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" <simonpj at 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-bounces at haskell.org
<ghc-devs-bounces at haskell.org>] On Behalf Of David
| Feuer
| Sent: 11 December 2016 05:01
| To: ghc-devs <ghc-devs at haskell.org>; Edward Kmett <ekmett at 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 at 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 at 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%
7C488bf00986e34ac0833208d42182c4
<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%
7C636170292905032831&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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170113/9d4944fc/attachment-0001.html>
More information about the ghc-devs
mailing list