magicDict

[Spiwack, Arnaud]

On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett <ekmett at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210426/4141e28a/attachment.html>