Re: magicDict

[Edward Kmett]

Indeed.

Sent from my iPhone

> On Apr 26, 2021, at 2:22 PM, Simon Peyton Jones  wrote:
> 
> 
> You mean you like ‘withDict’ with that name,  as well as the argument order K 
> suggests?   i.e. not reifyDict?
>  
> Simon
>  
> From: Edward Kmett  
> Sent: 26 April 2021 21:34
> To: Simon Peyton Jones 
> Cc: Krzysztof Gogolewski ; Spiwack, Arnaud 
> ; GHC developers ; Ryan Scott 
> 
> Subject: Re: magicDict
>  
> I like withDict a lot. It is direct, easy to chain/use, avoids fighting about 
> direction completely, and even matches the argument order used by reify in 
> the reflection library.
> 
>  
> 
> +1 from me.
> 
>  
> 
> On Mon, Apr 26, 2021 at 7:49 AM Simon Peyton Jones  
> wrote:
> 
> |  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  |  d...@haskell.org> 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%2F34707data=04%7C01%7Csimonpj%40micro
> |  >
> |  soft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988bf86f141af91ab2d7c
> |  >
> |  d011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTWFpbGZsb3d8eyJWIjoi
> |  >
> |  MC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000
> |  >
> |  sdata=VlRrIEROGj%2BE6%2FuLXBEdfa%2BPWVlHh50dahgjIrw4tQU%3Dreserve
> |  > 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 

RE: magicDict

[Simon Peyton Jones via ghc-devs]

You mean you like 'withDict' with that name,  as well as the argument order K 
suggests?   i.e. not reifyDict?

Simon

From: Edward Kmett 
Sent: 26 April 2021 21:34
To: Simon Peyton Jones 
Cc: Krzysztof Gogolewski ; Spiwack, Arnaud 
; GHC developers ; Ryan Scott 

Subject: Re: magicDict

I like withDict a lot. It is direct, easy to chain/use, avoids fighting about 
direction completely, and even matches the argument order used by reify in the 
reflection library.

+1 from me.

On Mon, Apr 26, 2021 at 7:49 AM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
|  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 
mailto:krz.gogolew...@gmail.com>>
|  Sent: 26 April 2021 15:35
|  To: Simon Peyton Jones mailto:simo...@microsoft.com>>
|  Cc: Spiwack, Arnaud 
mailto:arnaud.spiw...@tweag.io>>; Edward Kmett
|  mailto:ekm...@gmail.com>>; GHC developers 
mailto:ghc-devs@haskell.org>>
|  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 mailto:d...@haskell.org>> 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 
mailto:arnaud.spiw...@tweag.io>>
|  > Sent: 26 April 2021 08:10
|  > To: Edward Kmett mailto:ekm...@gmail.com>>
|  > Cc: Simon Peyton Jones 
mailto:simo...@microsoft.com>>; GHC developers
|  > mailto:ghc-devs@haskell.org>>
|  > Subject: Re: magicDict
|  >
|  >
|  >
|  >
|  >
|  >
|  >
|  > On Sun, Apr 25, 2021 at 2:20 AM Edward Kmett 
mailto:ekm...@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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fstac
|  >
|  
koverflow.com%2Fa%2F5316014%2F34707data=04%7C01%7Csimonpj%40micro
|  >
|  
soft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988bf86f141af91ab2d7c
|  >
|  d011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTWFpbGZsb3d8eyJWIjoi
|  >
|  MC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000
|  >
|  sdata=VlRrIEROGj%2BE6%2FuLXBEdfa%2BPWVlHh50dahgjIrw4tQU%3Dreserve
|  > 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 / 

Re: magicDict

[Edward Kmett]

I like withDict a lot. It is direct, easy to chain/use, avoids fighting
about direction completely, and even matches the argument order used by
reify in the reflection library.

+1 from me.

On Mon, Apr 26, 2021 at 7:49 AM Simon Peyton Jones 
wrote:

> |  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  |  d...@haskell.org> 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%2F34707data=04%7C01%7Csimonpj%40micro
> |  >
> |  soft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988bf86f141af91ab2d7c
> |  >
> |  d011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTWFpbGZsb3d8eyJWIjoi
> |  >
> |  MC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000
> |  >
> |  sdata=VlRrIEROGj%2BE6%2FuLXBEdfa%2BPWVlHh50dahgjIrw4tQU%3Dreserve
> |  > 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 

RE: magicDict

[Simon Peyton Jones via ghc-devs]

|  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%2F34707data=04%7C01%7Csimonpj%40micro
|  >
|  soft.com%7C87da21fdcc8e4ed6bef508d908c071fb%7C72f988bf86f141af91ab2d7c
|  >
|  d011db47%7C1%7C0%7C637550444930791696%7CUnknown%7CTWFpbGZsb3d8eyJWIjoi
|  >
|  MC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000
|  >
|  sdata=VlRrIEROGj%2BE6%2FuLXBEdfa%2BPWVlHh50dahgjIrw4tQU%3Dreserve
|  > 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-
|  devsdata=04%7C01
|  >
|  

Re: magicDict

[Krzysztof Gogolewski]

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://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
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: magicDict

[Simon Peyton Jones via ghc-devs]

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 
mailto:ekm...@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
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: magicDict

[Spiwack, Arnaud]

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://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
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs