Magical function to support reflection

David Feuer david.feuer at gmail.com
Tue Jan 17 19:49:38 UTC 2017 

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" <ekmett at 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 <
> simonpj at 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.feuer at gmail.com]
>> *Sent:* 14 January 2017 00:50
>> *To:* Simon Peyton Jones <simonpj at microsoft.com>
>> *Cc:* ghc-devs <ghc-devs at haskell.org>; Edward Kmett <ekmett at 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" <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%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>
>>
>>
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170117/d3a49cf0/attachment-0001.html>

More information about the ghc-devs mailing list