| 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 <krz.gogolew...@gmail.com> | Sent: 26 April 2021 15:35 | To: Simon Peyton Jones <simo...@microsoft.com> | Cc: Spiwack, Arnaud <arnaud.spiw...@tweag.io>; Edward Kmett | <ekm...@gmail.com>; GHC developers <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 <ghc- | 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 <arnaud.spiw...@tweag.io> | > Sent: 26 April 2021 08:10 | > To: Edward Kmett <ekm...@gmail.com> | > Cc: Simon Peyton Jones <simo...@microsoft.com>; GHC developers | > <ghc-devs@haskell.org> | > Subject: Re: magicDict | > | > | > | > | > | > | > | > On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett <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%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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
