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