Re: magicDict
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 | d...@haskell.org> 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
RE: magicDict
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 mailto:simo...@microsoft.com>> 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 mailto:krz.gogolew...@gmail.com>> | Sent: 26 April 2021 15:35 | To: Simon Peyton Jones mailto:simo...@microsoft.com>> | Cc: Spiwack, Arnaud mailto:arnaud.spiw...@tweag.io>>; Edward Kmett | mailto:ekm...@gmail.com>>; GHC developers mailto:ghc-devs@haskell.org>> | 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 mailto:d...@haskell.org>> 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 mailto:arnaud.spiw...@tweag.io>> | > Sent: 26 April 2021 08:10 | > To: Edward Kmett mailto:ekm...@gmail.com>> | > Cc: Simon Peyton Jones mailto:simo...@microsoft.com>>; GHC developers | > mailto:ghc-devs@haskell.org>> | > Subject: Re: magicDict | > | > | > | > | > | > | > | > On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett mailto:ekm...@gmail.com>> | 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<https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fkoverflow.com%2F&data=04%7C01%7Csimonpj%40microsoft.com%7Cbc489a190b534d771e8e08d908f2a2d4%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637550660487039029%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=p1oBeQtmxDH%2BRx%2FDNmIGeshz8PA0BEdiAcOk1faB0xc%3D&reserved=0>%2Fa%2F5316014%2F34707&data=04%7C01%7Csimonpj%40micro | > | soft.com<https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fsoft.com%2F&data=04%7C01%7Csimonpj%40microsoft.com%7Cbc489a190b534d771e8e08d908f2a2d4%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637550660487049021%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=N6k7M4FOB19jwAJVlx0y5WOxLwv7VUf58iihdwz2mhQ%3D&reserved=0>%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
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 | d...@haskell.org> 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 conf
RE: magicDict
| 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. |
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://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 ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
RE: magicDict
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 mailto:ekm...@gmail.com>> 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<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fstackoverflow.com%2Fa%2F5316014%2F34707&data=04%7C01%7Csimonpj%40microsoft.com%7C6460729f9ac144f3e10f08d9088265d5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637550178432988056%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=2jHuIJStnGotfXlFgA1xz7VEdM7Ps%2Buu4Ty51Q8YwAA%3D&reserved=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 http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
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
Re: magicDict
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 Let me see if I can try to explain why I think reasonable people can disagree here and why I ultimately adopted the "wrong" vocabulary from your perspective. 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*. This gets more muddled when you remove the quantifier, like here, now everything becomes the same size, nothing is being forgotten when you use "magicDict" to transform 5 :: Natural into dictionary for KnownNat (5 :: Nat) or use the single member of the dictionary to get your value back. If anything it goes the other way, because you _could_ evilly produce a dictionary from 6 :: Natural and nothing but your conscience stops you. But when used in a way that doesn't violate coherence of instance resolution, no finer fibration was introduced, reflect isn't forgetful, neither is reify, you produce singleton instances in a thin category from singleton types. In that framework, really neither term seems fully appropriate here -- or rather both do depending on your chosen perspective. This is where I believe the religious wars about which is concrete and which is abstract start up, because both uses satisfy that definition in this narrow case of isomorphism, no information is lost on either end. It is only when you actually introduce a quantifier to ensure 's' is fresh (as it is used in the reflection library to ensure this doesn't compromise instance resolution safety in general) that there is a bias introduced and 'reflect' forgets this hallucinated structure, finally forcing a 'handedness' on the terminology to use. I do not feel that I chose the vocabulary without due consideration of the precise meaning of the words used. -Edward On Thu, Apr 22, 2021 at 11:16 PM 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 > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: magicDict
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 > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: magicDict
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
RE: magicDict
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 ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: magicDict
Happy to see progress being made here. I think Ryan and others have spoken to any issues I would otherwise raise with the implementation itself. Currently I find myself reaching for unsafeCoerce over magicDict in most situations, and I'd really like to be able to stop doing that! I'm +1 on the name being something `reify`-ish, to avoid flipping the direction on the vocabulary. It is reifying a value as a dictionary. Something like `reifyValue` or `reifyAsDict` would avoid confusion as the dict isn't being reified, the value is. Both are a little clunky, but it is a very rare operation. It is also worth considering possibly mangling the name with a # or an 'unsafe' in the name to give casual users pause. -Edward On Thu, Apr 22, 2021 at 12:18 PM Krzysztof Gogolewski < krz.gogolew...@gmail.com> wrote: > 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.html#v:reify > > 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 < > ghc-devs@haskell.org> 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 > ___ > 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: magicDict
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.html#v:reify 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 ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: magicDict
Let me upvote `reflectDict`. On Thu, Apr 22, 2021 at 12:41 PM Simon Peyton Jones via ghc-devs < ghc-devs@haskell.org> 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
magicDict
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
