How about 'reifyDict'? The reflection library uses 'reify' to create a dictionary and 'reflect' to extract a value out of it. https://hackage.haskell.org/package/reflection-2.1.6/docs/Data-Reflection.ht... On Thu, Apr 22, 2021 at 3:27 PM Spiwack, Arnaud wrote:

Let me upvote `reflectDict`.

On Thu, Apr 22, 2021 at 12:41 PM Simon Peyton Jones via ghc-devs wrote:

...

Ed, and other ghc-devs

We are busy tidying up magicDict, and making it much more type-safe: see

https://gitlab.haskell.org/ghc/ghc/-/issues/16646 https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5573

As part of that change we’re think of changing its currently-rather-obscure name. I rather favour “reflectDict”. Any other views?

Simon

_______________________________________________ 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

Ah, yes... I can never remember which is reify and which is reflect. I'm fine either way. Maybe reifyDict is better. S | -----Original Message----- | From: Krzysztof Gogolewski | Sent: 22 April 2021 20:18 | To: Spiwack, Arnaud | Cc: Simon Peyton Jones ; GHC developers | Subject: Re: magicDict | | How about 'reifyDict'? The reflection library uses 'reify' to create a | dictionary and 'reflect' to extract a value out of it. | | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fhack | age.haskell.org%2Fpackage%2Freflection-2.1.6%2Fdocs%2FData- | Reflection.html%23v%3Areify&data=04%7C01%7Csimonpj%40microsoft.com | %7C4c3a0fe8f1b2459d746308d905c34ed0%7C72f988bf86f141af91ab2d7cd011db47 | %7C1%7C0%7C637547159883839881%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAw | MDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=bQ | RNfsZPQQ%2FxqVcJvVpRJSkBIEZojqmKyqhpv7gr9XU%3D&reserved=0 | | On Thu, Apr 22, 2021 at 3:27 PM Spiwack, Arnaud | wrote: | > | > Let me upvote `reflectDict`. | > | > On Thu, Apr 22, 2021 at 12:41 PM Simon Peyton Jones via ghc-devs | wrote: | >> | >> Ed, and other ghc-devs | >> | >> We are busy tidying up magicDict, and making it much more type- | safe: | >> see | >> | >> | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgit | >> lab.haskell.org%2Fghc%2Fghc%2F- | %2Fissues%2F16646&data=04%7C01%7Cs | >> | imonpj%40microsoft.com%7C4c3a0fe8f1b2459d746308d905c34ed0%7C72f988bf8 | >> | 6f141af91ab2d7cd011db47%7C1%7C0%7C637547159883839881%7CUnknown%7CTWFp | >> | bGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6M | >> | n0%3D%7C3000&sdata=6OX7dPWC2sVUeMKNaqZVGwH%2FJ9mGSWQRUEWuvUWq8uE% | >> 3D&reserved=0 | >> | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgit | >> lab.haskell.org%2Fghc%2Fghc%2F- | %2Fmerge_requests%2F5573&data=04%7 | >> | C01%7Csimonpj%40microsoft.com%7C4c3a0fe8f1b2459d746308d905c34ed0%7C72 | >> | f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637547159883839881%7CUnknown | >> | %7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLC | >> | JXVCI6Mn0%3D%7C3000&sdata=D2Q3wq74Y4RVnaAOjXQX6R9EuxuDplwmJ0zdk%2 | >> BAhN64%3D&reserved=0 | >> | >> As part of that change we're think of changing its currently- | rather-obscure name. I rather favour "reflectDict". Any other views? | >> | >> Simon | >> | >> _______________________________________________ | >> ghc-devs mailing list | >> ghc-devs@haskell.org | >> | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail | >> .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=04%7C | >> | 01%7Csimonpj%40microsoft.com%7C4c3a0fe8f1b2459d746308d905c34ed0%7C72f | >> | 988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637547159883839881%7CUnknown% | >> | 7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJ | >> | XVCI6Mn0%3D%7C3000&sdata=%2BQHuwK50UdRQR0AQOuNGstDM%2BtDEv%2F75fs | >> Ia3mfqvIw%3D&reserved=0 | > | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail. | > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=04%7C01 | > | %7Csimonpj%40microsoft.com%7C4c3a0fe8f1b2459d746308d905c34ed0%7C72f988 | > | bf86f141af91ab2d7cd011db47%7C1%7C0%7C637547159883839881%7CUnknown%7CTW | > | FpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6 | > | Mn0%3D%7C3000&sdata=%2BQHuwK50UdRQR0AQOuNGstDM%2BtDEv%2F75fsIa3mfq | > vIw%3D&reserved=0

This makes sense to me, and provides a good explanation for why I mix up the terms. So usual parlance is reify brings stuff back down/ reflect bounces it up? On Fri, Apr 23, 2021 at 2:16 AM Spiwack, Arnaud wrote:

While I do value consistency, let me pet-peeve for a minute here (sorry in advance Edward for the rant). The word “reify” comes from the latin “res”, which means object/thing. It should always mean something along the line of “making more concrete”. In normalisation by evaluation, for instance, you reify a semantic value as syntax (an object of the language of study), and you reflect values of the language into the semantic domain.

To me, the reflection library uses the terms inconsistently. For instance you have the type ReifiedMonoid for the concrete type representing a monoid instance. This is, in my opinion, the right terminology. However, a ReifiedMonoid should be the product of reification, but in the reflection library it actually gets reify-d further. This doesn’t seem to work at the grammar level. I contend that the function should have been reflect all along: you reflect a concrete dictionary object into the nebulous, untouchable world of type class instances.

It’s probably too late to fix the reflection library, hence me never complaining about it (in public :-) ). But I vote we don’t perpetuate this situation, and still call the function reflectDict. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett wrote:

I speak to much this same point in this old stack overflow response, though to exactly the opposite conclusion, and to exactly the opposite pet peeve.

https://stackoverflow.com/a/5316014/34707

:-) I do not feel that I chose the vocabulary without due consideration of the

precise meaning of the words used.

I didn't mean to imply that you did. Sorry if I did so: written communication is hard. For what it's worth, I didn't really think that I would change your mind, either. Though it still seems to me that the name `ReifiedMonoid` uses the word for a different thing than the `reifyMonoid` function does. To be explicit:

Viewing a type as a space, 'reify' in the reflection library takes some space 'a' and splits it into individual fibers for each term in 'a', finding the appropriate one and handing it back to you as a fresh type 's' that captures just that singular value. The result is significantly less abstract, as we gained detail on the type, now every point in the original space 'a' is a new space. At the type level the fresh 's' in s `Reifies` a now concretely names exactly one inhabitant of 'a'.

On the flip side, 'reflect' in the reflection library forgets this finer fibration / structure on space, losing the information about which fiber the answer came from, being forgetful is precisely the justification of it being the 'reflect' half of the reify -| reflect pairing.

I confess I don't necessarily anticipate this changing your mind but it was not chosen blindly, reflect is the forgetful mapping here, reification is free and left adjoint to it, at least in the context of reflection-the-library, *where a quantifier is being injected to track the particular member*.

I've got to admit that I have the hardest time seeing the `s` as representing an inhabitant of `a`. I'm probably missing something here. I also don't think that a free object construction embodies a reify/reflect pair completely. It's probably fair to see `reify` as being the natural mapping from the free object of X to X (the counit of the adjunction). But reification will not be the unit of the adjunction, because it's trivial. So there is still a piece missing in this story. Anyway… I've made my point, and I am not too willing to spend too much time proving Wadler's law correct. So I think I'll stop here, fascinating a conversation though it is. Best, Arnaud

I would like to propose one more option: withDict :: dt -> (ct => a) -> a 1. This is less symmetric than '(ct => a) -> dt -> a' but in existing applications magicDict gets the arguments in the reverse order. 2. Easier to chain 'withDict d1 (withDict d2 ...)'. 3. The name is similar to 'withTypeable' or 'withFile', and avoids arguing which is reify or reflect. On Mon, Apr 26, 2021 at 9:41 AM Simon Peyton Jones via ghc-devs wrote:

Can we just agree a name, then? Please correct me if I’m wrong, but

I think Ed prefers ‘reifyDict’, That is compatible with the existing reflection library Arnaud disagrees but isn’t going to die in the trenches for this one Virtually anything is better than ‘magicDict’.

So: reifyDict it is?

Simon

From: Spiwack, Arnaud Sent: 26 April 2021 08:10 To: Edward Kmett Cc: Simon Peyton Jones ; GHC developers Subject: Re: magicDict

On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett wrote:

I speak to much this same point in this old stack overflow response, though to exactly the opposite conclusion, and to exactly the opposite pet peeve.

https://stackoverflow.com/a/5316014/34707

:-)

I do not feel that I chose the vocabulary without due consideration of the precise meaning of the words used.

I didn't mean to imply that you did. Sorry if I did so: written communication is hard. For what it's worth, I didn't really think that I would change your mind, either.

Though it still seems to me that the name `ReifiedMonoid` uses the word for a different thing than the `reifyMonoid` function does.

To be explicit:

Viewing a type as a space, 'reify' in the reflection library takes some space 'a' and splits it into individual fibers for each term in 'a', finding the appropriate one and handing it back to you as a fresh type 's' that captures just that singular value. The result is significantly less abstract, as we gained detail on the type, now every point in the original space 'a' is a new space. At the type level the fresh 's' in s `Reifies` a now concretely names exactly one inhabitant of 'a'.

On the flip side, 'reflect' in the reflection library forgets this finer fibration / structure on space, losing the information about which fiber the answer came from, being forgetful is precisely the justification of it being the 'reflect' half of the reify -| reflect pairing.

I confess I don't necessarily anticipate this changing your mind but it was not chosen blindly, reflect is the forgetful mapping here, reification is free and left adjoint to it, at least in the context of reflection-the-library, where a quantifier is being injected to track the particular member.

I've got to admit that I have the hardest time seeing the `s` as representing an inhabitant of `a`. I'm probably missing something here.

I also don't think that a free object construction embodies a reify/reflect pair completely. It's probably fair to see `reify` as being the natural mapping from the free object of X to X (the counit of the adjunction). But reification will not be the unit of the adjunction, because it's trivial. So there is still a piece missing in this story.

Anyway… I've made my point, and I am not too willing to spend too much time proving Wadler's law correct. So I think I'll stop here, fascinating a conversation though it is.

Best,

Arnaud

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

I like withDict a lot. It is direct, easy to chain/use, avoids fighting about direction completely, and even matches the argument order used by reify in the reflection library. +1 from me. On Mon, Apr 26, 2021 at 7:49 AM Simon Peyton Jones wrote:

| I would like to propose one more option: | | withDict :: dt -> (ct => a) -> a

Ah, you mean simply: swap the argument order. I can see your logic about chaining etc. I'd be fine with this.

Simon

| -----Original Message----- | From: Krzysztof Gogolewski | Sent: 26 April 2021 15:35 | To: Simon Peyton Jones | Cc: Spiwack, Arnaud ; Edward Kmett | ; GHC developers | Subject: Re: magicDict | | I would like to propose one more option: | | withDict :: dt -> (ct => a) -> a | | 1. This is less symmetric than '(ct => a) -> dt -> a' | but in existing applications magicDict gets the arguments | in the reverse order. | 2. Easier to chain 'withDict d1 (withDict d2 ...)'. | 3. The name is similar to 'withTypeable' or 'withFile', | and avoids arguing which is reify or reflect. | | On Mon, Apr 26, 2021 at 9:41 AM Simon Peyton Jones via ghc-devs wrote: | > | > Can we just agree a name, then? Please correct me if I'm wrong, | but | > | > I think Ed prefers 'reifyDict', | > That is compatible with the existing reflection library Arnaud | > disagrees but isn't going to die in the trenches for this one | > Virtually anything is better than 'magicDict'. | > | > | > | > | > | > So: reifyDict it is? | > | > | > | > Simon | > | > | > | > From: Spiwack, Arnaud | > Sent: 26 April 2021 08:10 | > To: Edward Kmett | > Cc: Simon Peyton Jones ; GHC developers | > | > Subject: Re: magicDict | > | > | > | > | > | > | > | > On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett | wrote: | > | > I speak to much this same point in this old stack overflow response, | though to exactly the opposite conclusion, and to exactly the opposite | pet peeve. | > | > | > | > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fstac | > | koverflow.com%2Fa%2F5316014%2F34707&data=04%7C01%7Csimonpj%40micro | > | soft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988bf86f141af91ab2d7c | > | d011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTWFpbGZsb3d8eyJWIjoi | > | MC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000& | > | sdata=VlRrIEROGj%2BE6%2FuLXBEdfa%2BPWVlHh50dahgjIrw4tQU%3D&reserve | > d=0 | > | > | > | > :-) | > | > | > | > I do not feel that I chose the vocabulary without due consideration | of the precise meaning of the words used. | > | > | > | > I didn't mean to imply that you did. Sorry if I did so: written | communication is hard. For what it's worth, I didn't really think that | I would change your mind, either. | > | > | > | > Though it still seems to me that the name `ReifiedMonoid` uses the | word for a different thing than the `reifyMonoid` function does. | > | > | > | > To be explicit: | > | > | > | > Viewing a type as a space, 'reify' in the reflection library takes | some space 'a' and splits it into individual fibers for each term in | 'a', finding the appropriate one and handing it back to you as a fresh | type 's' that captures just that singular value. The result is | significantly less abstract, as we gained detail on the type, now | every point in the original space 'a' is a new space. At the type | level the fresh 's' in s `Reifies` a now concretely names exactly one | inhabitant of 'a'. | > | > | > | > On the flip side, 'reflect' in the reflection library forgets this | finer fibration / structure on space, losing the information about | which fiber the answer came from, being forgetful is precisely the | justification of it being the 'reflect' half of the reify -| reflect | pairing. | > | > | > | > I confess I don't necessarily anticipate this changing your mind but | it was not chosen blindly, reflect is the forgetful mapping here, | reification is free and left adjoint to it, at least in the context of | reflection-the-library, where a quantifier is being injected to track | the particular member. | > | > | > | > I've got to admit that I have the hardest time seeing the `s` as | representing an inhabitant of `a`. I'm probably missing something | here. | > | > | > | > I also don't think that a free object construction embodies a | reify/reflect pair completely. It's probably fair to see `reify` as | being the natural mapping from the free object of X to X (the counit | of the adjunction). But reification will not be the unit of the | adjunction, because it's trivial. So there is still a piece missing in | this story. | > | > | > | > Anyway... I've made my point, and I am not too willing to spend too | much time proving Wadler's law correct. So I think I'll stop here, | fascinating a conversation though it is. | > | > | > | > Best, | > | > Arnaud | > | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail. | > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=04%7C01 | > | %7Csimonpj%40microsoft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988 | > | bf86f141af91ab2d7cd011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTW | > | FpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6 | > | Mn0%3D%7C1000&sdata=4JfXyRNMjQKTSLqme2VJU9Dy0s6N4Y8t%2BINHYp38xJk% | > 3D&reserved=0

Indeed. Sent from my iPhone

On Apr 26, 2021, at 2:22 PM, Simon Peyton Jones wrote:

 You mean you like ‘withDict’ with that name, as well as the argument order K suggests? i.e. not reifyDict?

Simon

From: Edward Kmett Sent: 26 April 2021 21:34 To: Simon Peyton Jones Cc: Krzysztof Gogolewski ; Spiwack, Arnaud ; GHC developers ; Ryan Scott Subject: Re: magicDict

I like withDict a lot. It is direct, easy to chain/use, avoids fighting about direction completely, and even matches the argument order used by reify in the reflection library.

+1 from me.

On Mon, Apr 26, 2021 at 7:49 AM Simon Peyton Jones wrote:

| I would like to propose one more option: | | withDict :: dt -> (ct => a) -> a

Ah, you mean simply: swap the argument order. I can see your logic about chaining etc. I'd be fine with this.

Simon

| -----Original Message----- | From: Krzysztof Gogolewski | Sent: 26 April 2021 15:35 | To: Simon Peyton Jones | Cc: Spiwack, Arnaud ; Edward Kmett | ; GHC developers | Subject: Re: magicDict | | I would like to propose one more option: | | withDict :: dt -> (ct => a) -> a | | 1. This is less symmetric than '(ct => a) -> dt -> a' | but in existing applications magicDict gets the arguments | in the reverse order. | 2. Easier to chain 'withDict d1 (withDict d2 ...)'. | 3. The name is similar to 'withTypeable' or 'withFile', | and avoids arguing which is reify or reflect. | | On Mon, Apr 26, 2021 at 9:41 AM Simon Peyton Jones via ghc-devs wrote: | > | > Can we just agree a name, then? Please correct me if I'm wrong, | but | > | > I think Ed prefers 'reifyDict', | > That is compatible with the existing reflection library Arnaud | > disagrees but isn't going to die in the trenches for this one | > Virtually anything is better than 'magicDict'. | > | > | > | > | > | > So: reifyDict it is? | > | > | > | > Simon | > | > | > | > From: Spiwack, Arnaud | > Sent: 26 April 2021 08:10 | > To: Edward Kmett | > Cc: Simon Peyton Jones ; GHC developers | > | > Subject: Re: magicDict | > | > | > | > | > | > | > | > On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett | wrote: | > | > I speak to much this same point in this old stack overflow response, | though to exactly the opposite conclusion, and to exactly the opposite | pet peeve. | > | > | > | > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fstac | > | koverflow.com%2Fa%2F5316014%2F34707&data=04%7C01%7Csimonpj%40micro | > | soft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988bf86f141af91ab2d7c | > | d011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTWFpbGZsb3d8eyJWIjoi | > | MC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000& | > | sdata=VlRrIEROGj%2BE6%2FuLXBEdfa%2BPWVlHh50dahgjIrw4tQU%3D&reserve | > d=0 | > | > | > | > :-) | > | > | > | > I do not feel that I chose the vocabulary without due consideration | of the precise meaning of the words used. | > | > | > | > I didn't mean to imply that you did. Sorry if I did so: written | communication is hard. For what it's worth, I didn't really think that | I would change your mind, either. | > | > | > | > Though it still seems to me that the name `ReifiedMonoid` uses the | word for a different thing than the `reifyMonoid` function does. | > | > | > | > To be explicit: | > | > | > | > Viewing a type as a space, 'reify' in the reflection library takes | some space 'a' and splits it into individual fibers for each term in | 'a', finding the appropriate one and handing it back to you as a fresh | type 's' that captures just that singular value. The result is | significantly less abstract, as we gained detail on the type, now | every point in the original space 'a' is a new space. At the type | level the fresh 's' in s `Reifies` a now concretely names exactly one | inhabitant of 'a'. | > | > | > | > On the flip side, 'reflect' in the reflection library forgets this | finer fibration / structure on space, losing the information about | which fiber the answer came from, being forgetful is precisely the | justification of it being the 'reflect' half of the reify -| reflect | pairing. | > | > | > | > I confess I don't necessarily anticipate this changing your mind but | it was not chosen blindly, reflect is the forgetful mapping here, | reification is free and left adjoint to it, at least in the context of | reflection-the-library, where a quantifier is being injected to track | the particular member. | > | > | > | > I've got to admit that I have the hardest time seeing the `s` as | representing an inhabitant of `a`. I'm probably missing something | here. | > | > | > | > I also don't think that a free object construction embodies a | reify/reflect pair completely. It's probably fair to see `reify` as | being the natural mapping from the free object of X to X (the counit | of the adjunction). But reification will not be the unit of the | adjunction, because it's trivial. So there is still a piece missing in | this story. | > | > | > | > Anyway... I've made my point, and I am not too willing to spend too | much time proving Wadler's law correct. So I think I'll stop here, | fascinating a conversation though it is. | > | > | > | > Best, | > | > Arnaud | > | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail. | > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=04%7C01 | > | %7Csimonpj%40microsoft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988 | > | bf86f141af91ab2d7cd011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTW | > | FpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6 | > | Mn0%3D%7C1000&sdata=4JfXyRNMjQKTSLqme2VJU9Dy0s6N4Y8t%2BINHYp38xJk% | > 3D&reserved=0