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