<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">https://stackoverflow.com/a/5316014/34707</a><br><div><br></div><div>Let me see if I can try to explain why I think reasonable people can disagree here and why I ultimately adopted the "wrong" vocabulary from your perspective.</div><div><br></div><div>To be explicit:</div><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><br></div><div>This gets more muddled when you remove the quantifier, like here, now everything becomes the same size, nothing is being forgotten when you use "magicDict" to transform 5 :: Natural into dictionary for KnownNat (5 :: Nat) or use the single member of the dictionary to get your value back. If anything it goes the other way, because you _could_ evilly produce a dictionary from 6 :: Natural and nothing but your conscience stops you. But when used in a way that doesn't violate coherence of instance resolution, no finer fibration was introduced, reflect isn't forgetful, neither is reify, you produce singleton instances in a thin category from singleton types. In that framework, really neither term seems fully appropriate here -- or rather both do depending on your chosen perspective. This is where I believe the religious wars about which is concrete and which is abstract start up, because both uses satisfy that definition in this narrow case of isomorphism, no information is lost on either end.<br></div><div><br></div><div>It is only when you actually introduce a quantifier to ensure 's' is fresh (as it is used in the reflection library to ensure this doesn't compromise instance resolution safety in general) that there is a bias introduced and 'reflect' forgets this hallucinated structure, finally forcing a 'handedness' on the terminology to use.</div><div><br></div><div><div>I do not feel that I chose the vocabulary without due consideration of the precise meaning of the words used.<br></div><div><div><div><div></div></div><div></div></div><div></div></div><div></div></div><div><br></div><div>-Edward</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Apr 22, 2021 at 11:16 PM Spiwack, Arnaud <<a href="mailto:arnaud.spiwack@tweag.io">arnaud.spiwack@tweag.io</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><p style="margin:0px 0px 1.2em">While I do value consistency, let me pet-peeve for a minute here (sorry in advance Edward for the rant). The word “reify” comes from the latin “res”, which means object/thing. It should always mean something along the line of “making more concrete”. In normalisation by evaluation, for instance, you reify a semantic value as syntax (an object of the language of study), and you reflect values of the language into the semantic domain.</p>
<p style="margin:0px 0px 1.2em">To me, the reflection library uses the terms inconsistently. For instance you have the type <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">ReifiedMonoid</code> for the concrete type representing a monoid instance. This is, in my opinion, the right terminology. However, a <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">ReifiedMonoid</code> should be the product of reification, but in the <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">reflection</code> library it actually gets <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">reify</code>-d further. This doesn’t seem to work at the grammar level. I contend that the function should have been <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">reflect</code> all along: you reflect a concrete dictionary object into the nebulous, untouchable world of type class instances.</p>
<p style="margin:0px 0px 1.2em">It’s probably too late to fix the reflection library, hence me never complaining about it (in public :-) ). But I vote we don’t perpetuate this situation, and still call the function <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">reflectDict</code>.</p>
<div title="MDH:PGRpdj5XaGlsZSBJIGRvIHZhbHVlIGNvbnNpc3RlbmN5LCBsZXQgbWUgcGV0LXBlZXZlIGZvciBh
IG1pbnV0ZSBoZXJlIChzb3JyeSBpbiBhZHZhbmNlIEVkd2FyZCBmb3IgdGhlIHJhbnQpLiBUaGUg
d29yZCDigJxyZWlmeeKAnSBjb21lcyBmcm9tIHRoZSBsYXRpbiDigJxyZXPigJ0sIHdoaWNoIG1l
YW5zIG9iamVjdC90aGluZy4gSXQgc2hvdWxkIGFsd2F5cyBtZWFuIHNvbWV0aGluZyBhbG9uZyB0
aGUgbGluZSBvZiDigJxtYWtpbmcgbW9yZSBjb25jcmV0ZeKAnS4gSW4gbm9ybWFsaXNhdGlvbiBi
eSBldmFsdWF0aW9uLCBmb3IgaW5zdGFuY2UsIHlvdSByZWlmeSBhIHNlbWFudGljIHZhbHVlIGFz
IHN5bnRheCAoYW4gb2JqZWN0IG9mIHRoZSBsYW5ndWFnZSBvZiBzdHVkeSksIGFuZCB5b3UgcmVm
bGVjdCB2YWx1ZXMgb2YgdGhlIGxhbmd1YWdlIGludG8gdGhlIHNlbWFudGljIGRvbWFpbi48L2Rp
dj48ZGl2Pjxicj48L2Rpdj48ZGl2PlRvIG1lLCB0aGUgcmVmbGVjdGlvbiBsaWJyYXJ5IHVzZXMg
dGhlIHRlcm1zIGluY29uc2lzdGVudGx5LiBGb3IgaW5zdGFuY2UgeW91IGhhdmUgdGhlIHR5cGUg
YFJlaWZpZWRNb25vaWRgIGZvciB0aGUgY29uY3JldGUgdHlwZSByZXByZXNlbnRpbmcgYSBtb25v
aWQgaW5zdGFuY2UuIFRoaXMgaXMsIGluIG15IG9waW5pb24sIHRoZSByaWdodCB0ZXJtaW5vbG9n
eS4gSG93ZXZlciwgYSBgUmVpZmllZE1vbm9pZGAgc2hvdWxkIGJlIHRoZSBwcm9kdWN0IG9mIHJl
aWZpY2F0aW9uLCBidXQgaW4gdGhlIGByZWZsZWN0aW9uYCBsaWJyYXJ5IGl0IGFjdHVhbGx5IGdl
dHMgYHJlaWZ5YC1kIGZ1cnRoZXIuIFRoaXMgZG9lc24ndCBzZWVtIHRvIHdvcmsgYXQgdGhlIGdy
YW1tYXIgbGV2ZWwuIEkgY29udGVuZCB0aGF0IHRoZSBmdW5jdGlvbiBzaG91bGQgaGF2ZSBiZWVu
IGByZWZsZWN0YCBhbGwgYWxvbmc6IHlvdSByZWZsZWN0IGEgY29uY3JldGUgZGljdGlvbmFyeSBv
YmplY3QgaW50byB0aGUgbmVidWxvdXMsIHVudG91Y2hhYmxlIHdvcmxkIG9mIHR5cGUgY2xhc3Mg
aW5zdGFuY2VzLjwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+SXQncyBwcm9iYWJseSB0b28gbGF0
ZSB0byBmaXggdGhlIHJlZmxlY3Rpb24gbGlicmFyeSwgaGVuY2UgbWUgbmV2ZXIgY29tcGxhaW5p
bmcgYWJvdXQgaXQgKGluIHB1YmxpYyA6LSkgKS4gQnV0IEkgdm90ZSB3ZSBkb24ndCBwZXJwZXR1
YXRlIHRoaXMgc2l0dWF0aW9uLCBhbmQgc3RpbGwgY2FsbCB0aGUgZnVuY3Rpb24gYHJlZmxlY3RE
aWN0YC48YnI+PC9kaXY+" style="height:0px;width:0px;max-height:0px;max-width:0px;overflow:hidden;font-size:0em;padding:0px;margin:0px"></div></div></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>