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-devs@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://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
