<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>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.<br></div><div><br></div><a href="https://stackoverflow.com/a/5316014/34707" target="_blank">https://stackoverflow.com/a/5316014/34707</a></div></blockquote><div><br></div><div>:-)</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>I do not feel that I chose the vocabulary without due consideration of the precise meaning of the words used.</div></blockquote><div><br></div><div>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.</div><div><br></div><div>Though it still seems to me that the name `ReifiedMonoid` uses the word for a different thing than the `reifyMonoid` function does.<br></div><div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">To be explicit:<div><br></div><div>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 <font face="monospace">s `Reifies` a</font> now concretely names exactly one inhabitant of 'a'.</div><div><br></div><div>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.</div><div><br></div><div><div></div></div><div>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, <i>where a quantifier is being injected to track the particular member</i>.</div></div></blockquote><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Best,</div><div>Arnaud<br></div></div></div>