Spiwack, Arnaud arnaud.spiwack at
Mon Apr 26 07:10:02 UTC 2021

On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett <ekmett at> 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.


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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list