magicDict

[Edward Kmett]

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

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.

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

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.

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.

I do not feel that I chose the vocabulary without due consideration of the
precise meaning of the words used.

-Edward

On Thu, Apr 22, 2021 at 11:16 PM Spiwack, Arnaud <arnaud.spiwack at tweag.io>
wrote:

> 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.
>
> To me, the reflection library uses the terms inconsistently. For instance
> you have the type ReifiedMonoid for the concrete type representing a
> monoid instance. This is, in my opinion, the right terminology. However, a
> ReifiedMonoid should be the product of reification, but in the reflection
> library it actually gets reify-d further. This doesn’t seem to work at
> the grammar level. I contend that the function should have been reflect
> all along: you reflect a concrete dictionary object into the nebulous,
> untouchable world of type class instances.
>
> 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 reflectDict.
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210424/e46b8960/attachment.html>