| I would like to propose one more option:
|
| withDict :: dt -> (ct => a) -> a
Ah, you mean simply: swap the argument order. I can see your logic about chaining etc. I'd be fine with this.
Simon
| -----Original Message-----
| From: Krzysztof Gogolewski
| Sent: 26 April 2021 15:35
| To: Simon Peyton Jones
| Cc: Spiwack, Arnaud ; Edward Kmett
| ; GHC developers
| Subject: Re: magicDict
|
| I would like to propose one more option:
|
| withDict :: dt -> (ct => a) -> a
|
| 1. This is less symmetric than '(ct => a) -> dt -> a'
| but in existing applications magicDict gets the arguments
| in the reverse order.
| 2. Easier to chain 'withDict d1 (withDict d2 ...)'.
| 3. The name is similar to 'withTypeable' or 'withFile',
| and avoids arguing which is reify or reflect.
|
| On Mon, Apr 26, 2021 at 9:41 AM Simon Peyton Jones via ghc-devs wrote:
| >
| > 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
| > Sent: 26 April 2021 08:10
| > To: Edward Kmett
| > Cc: Simon Peyton Jones ; GHC developers
| >
| > Subject: Re: magicDict
| >
| >
| >
| >
| >
| >
| >
| > On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett
| 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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fstac
| >
| koverflow.com%2Fa%2F5316014%2F34707&data=04%7C01%7Csimonpj%40micro
| >
| soft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988bf86f141af91ab2d7c
| >
| d011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTWFpbGZsb3d8eyJWIjoi
| >
| MC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&
| >
| sdata=VlRrIEROGj%2BE6%2FuLXBEdfa%2BPWVlHh50dahgjIrw4tQU%3D&reserve
| > d=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
| >
| > _______________________________________________
| > ghc-devs mailing list
| > ghc-devs@haskell.org
| >
| https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.
| > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
| devs&data=04%7C01
| >
| %7Csimonpj%40microsoft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988
| >
| bf86f141af91ab2d7cd011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTW
| >
| FpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6
| >
| Mn0%3D%7C1000&sdata=4JfXyRNMjQKTSLqme2VJU9Dy0s6N4Y8t%2BINHYp38xJk%
| > 3D&reserved=0
