magicDict

[Simon Peyton Jones]

Can we just agree a name, then?   Please correct me if I'm wrong, but

  *   I think Ed prefers 'reifyDict',
  *   That is compatible with the existing reflection library
  *   Arnaud disagrees but isn't going to die in the trenches for this one
  *   Virtually anything is better than 'magicDict'.


So: reifyDict it is?

Simon

From: Spiwack, Arnaud <arnaud.spiwack at tweag.io>
Sent: 26 April 2021 08:10
To: Edward Kmett <ekmett at gmail.com>
Cc: Simon Peyton Jones <simonpj at microsoft.com>; GHC developers <ghc-devs at haskell.org>
Subject: Re: magicDict



On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett <ekmett at gmail.com<mailto: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<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fstackoverflow.com%2Fa%2F5316014%2F34707&data=04%7C01%7Csimonpj%40microsoft.com%7C6460729f9ac144f3e10f08d9088265d5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637550178432988056%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=2jHuIJStnGotfXlFgA1xz7VEdM7Ps%2Buu4Ty51Q8YwAA%3D&reserved=0>

:-)

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/6920f0d4/attachment.html>