Re: Magical function to support reflection

[Kiss Csongor]

The problem is in the reify function:

```
reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy
```
here, unsafeCoerce coerces `const a` to type `a`, in the concrete case, to Int.
```
*Main> unsafeCoerce (const 5) :: Int
1099511628032
```
this is indeed what seems to be the issue:
```
*Main> reify 5 reflect
1099511628032
```
which is why test1 then shows the wrong result.

Also, in the Magic newtype, there’s a `Proxy s`, which afaik doesn’t have the 
expected runtime representation
`a -> r`. (there’s a proxy in the middle, `a -> Proxy -> r`).

Changing Magic to
```
newtype Magic a r = Magic (forall (s :: *) . Reifies s a => Tagged s r)
```
now has the correct runtime rep, and the reification can be done by coercing 
the Magic in to `a -> r`, as such
```
reify' :: a -> (forall (s :: *) . Reifies s a => Tagged s r) -> r
reify' a f = unsafeCoerce (Magic f) a
```

the Proxy version is just a convenience, wrapped around the magic one:

```
reify :: forall r a. a -> (forall (s :: *) . Reifies s a => Proxy s -> r) -> r
reify a f = reify' a (unproxy f)
```

Here’s the complete file, with the changes that compile and now work:

https://gist.github.com/kcsongor/b2f829b2b60022505b7e48b1360d2679 


— Csongor

> On 20 Jan 2017, at 14:14, Matthew Pickering  
> wrote:
> 
> I modified the example on the wiki to compile but I seem to have
> missed something, could you perhaps point out what I missed?
> 
> https://gist.github.com/mpickering/da6d7852af2f6c8f59f80ce726baa864
> 
> ```
> *Main> test1 2 123 441212
> 441335
> ```
> 
> On Thu, Jan 19, 2017 at 3:58 AM, David Feuer  wrote:
>> I've updated https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport 
>> to
>> reflect both Simon's thoughts on the matter and my own reactions to them. I
>> hope you'll give it a peek.
>> 
>> David Feuer
>> ___
>> ghc-devs mailing list
>> ghc-devs@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Magical function to support reflection

[Matthew Pickering]

I modified the example on the wiki to compile but I seem to have
missed something, could you perhaps point out what I missed?

https://gist.github.com/mpickering/da6d7852af2f6c8f59f80ce726baa864

```
*Main> test1 2 123 441212
441335
```

On Thu, Jan 19, 2017 at 3:58 AM, David Feuer  wrote:
> I've updated https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport to
> reflect both Simon's thoughts on the matter and my own reactions to them. I
> hope you'll give it a peek.
>
> David Feuer
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Magical function to support reflection

[Simon Peyton Jones via ghc-devs]

I've added some comments. I like ReflectableDF a lot.

Simon

| -Original Message-
| From: David Feuer [mailto:da...@well-typed.com]
| Sent: 19 January 2017 02:59
| To: ghc-devs@haskell.org; Simon Peyton Jones <simo...@microsoft.com>
| Cc: Edward Kmett <ekm...@gmail.com>
| Subject: Re: Magical function to support reflection
| 
| I've updated
| https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport to reflect
| both Simon's thoughts on the matter and my own reactions to them. I hope
| you'll give it a peek.
| 
| David Feuer
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Magical function to support reflection

[David Feuer]

I've updated https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport to 
reflect both Simon's thoughts on the matter and my own reactions to them. I 
hope you'll give it a peek.

David Feuer
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Magical function to support reflection

[Simon Peyton Jones via ghc-devs]

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.
The approach I proposed below looks general, safe, and performant.  Or not?

To make progress it’d be good to update the wiki page, both in the light of the 
recent discussion, and with pointers to related packages, motivation, papers, 
to set the context

Simon

From: Edward Kmett [mailto:ekm...@gmail.com]
Sent: 17 January 2017 19:43
To: Simon Peyton Jones <simo...@microsoft.com>
Cc: David Feuer <david.fe...@gmail.com>; ghc-devs <ghc-devs@haskell.org>
Subject: Re: Magical function to support reflection

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<mailto:simo...@microsoft.com>> wrote:
David says that this paper is relevant
http://okmij.org/ftp/Haskell/tr-15-04.pdf<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fokmij.org%2Fftp%2FHaskell%2Ftr-15-04.pdf=02%7C01%7Csimonpj%40microsoft.com%7C5acac2bf025d4d82591408d43f10fda4%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C636202789589256322=CMLJ4RAe6DI6YQ%2FZhOP0xnV7OhZTDloBm2htr9TwhN0%3D=0>

Simon

From: David Feuer [mailto:david.fe...@gmail.com<mailto:david.fe...@gmail.com>]
Sent: 14 January 2017 00:50
To: Simon Peyton Jones <simo...@microsoft.com<mailto:simo...@microsoft.com>>
Cc: ghc-devs <ghc-devs@haskell.org<mailto:ghc-devs@haskell.org>>; Edward Kmett 
<ekm...@gmail.com<mailto: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<mailto: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) -&

Re: Magical function to support reflection

[David Feuer]

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 Reifi

Re: Magical function to support reflection

[Edward Kmett]

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 ar

RE: Magical function to support reflection

[Simon Peyton Jones via ghc-devs]

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<mailto: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 

RE: Magical function to support reflection

[David Feuer]

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

RE: Magical function to support reflection

[Simon Peyton Jones via ghc-devs]

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] On Behalf Of David

|  Feuer

|  Sent: 11 December 2016 05:01

|  To: ghc-devs <ghc-devs@haskell.org<mailto:ghc-devs@haskell.org>>; Edward 
Kmett <ekm...@gmail.com<mailto: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 specializ

Re: Magical function to support reflection

[Edward Kmett]

I wasn't referring to Tagged itself being evil. I was referring to giving
an excessively general type to reify# that can be used to generate
segfaults as being evil.

The existing reify combinator doesn't have that property, but can't be used
to build KnownNat and KnownSymbol dictionaries. (Hence why there are
specialized combinators for those in reflection.)

-Edward

On Thu, Dec 22, 2016 at 6:55 PM, David Feuer  wrote:

> On Thu, Dec 22, 2016 at 4:58 PM, Edward Kmett  wrote:
> > On Mon, Dec 12, 2016 at 1:31 PM, David Feuer 
> wrote:
> >>
> >> On Dec 12, 2016 1:15 PM, "Edward Kmett"  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

Re: Magical function to support reflection

[David Feuer]

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  wrote:
> On Thu, Dec 22, 2016 at 4:58 PM, Edward Kmett  wrote:
>> On Mon, Dec 12, 2016 at 1:31 PM, David Feuer  wrote:
>>>
>>> On Dec 12, 2016 1:15 PM, "Edward Kmett"  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

Re: Magical function to support reflection

[David Feuer]

On Thu, Dec 22, 2016 at 4:58 PM, Edward Kmett  wrote:
> On Mon, Dec 12, 2016 at 1:31 PM, David Feuer  wrote:
>>
>> On Dec 12, 2016 1:15 PM, "Edward Kmett"  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

Re: Magical function to support reflection

[Edward Kmett]

On Mon, Dec 12, 2016 at 1:31 PM, David Feuer  wrote:

> On Dec 12, 2016 1:15 PM, "Edward Kmett"  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.

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.

Tagged in the example could be replaced with explicit type application if
> backwards compatibility isn't a concern. OTOH, it is.
>
>
> Would that help Core typing?
>

It doesn't make a difference there. The only thing is it avoids needing to
make up something like Tagged.

>
>  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.

and admit both fundep and TF forms. I mean, if you're going to lie you
> might as well lie big.
>
>
> Definitely.
>


> There are a very large number of instances out there scattered across
> dozens of packages that would be broken by switching from Proxy to Tagged
> or explicit type application internally. (I realize that this is a lesser
> concern that can be resolved by a major version bump and some community
> friction, but it does mean pragmatically that migrating to something like
> this would need a plan.)
>
>
> I just want to make sure that we do what we need to get Really Good Code,
> if we're going to the trouble of adding compiler support.
>

That makes sense to me.

-Edward
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Magical function to support reflection

[David Feuer]

On Dec 12, 2016 1:15 PM, "Edward Kmett"  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?


Tagged in the example could be replaced with explicit type application if
backwards compatibility isn't a concern. OTOH, it is.


Would that help Core typing?

 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?


and admit both fundep and TF forms. I mean, if you're going to lie you
might as well lie big.


Definitely.



There are a very large number of instances out there scattered across
dozens of packages that would be broken by switching from Proxy to Tagged
or explicit type application internally. (I realize that this is a lesser
concern that can be resolved by a major version bump and some community
friction, but it does mean pragmatically that migrating to something like
this would need a plan.)


I just want to make sure that we do what we need to get Really Good Code,
if we're going to the trouble of adding compiler support.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Magical function to support reflection

[David Feuer]

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
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs