Thanks for bringing this up again. This was started in my data-proxy branch of base https://github.com/ghc/packages-base/tree/data-proxy, but never really finished. We definitely want to have this in 7.8, and I think there's only some minor finishing work to do (check if we have all the instances we want, document, etc.). Perhaps you can look through what's there already, and what you think is missing? I'm more than happy to accept contributing patches too :-) Thanks, Pedro On Sun, Jul 21, 2013 at 3:09 AM, Shachaf Ben-Kiki wrote:

On Mon, Mar 4, 2013 at 11:12 AM, José Pedro Magalhães wrote:

...

Hi,

On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg wrote:

...

Unless I'm missing something, this all looks very straightforward. The implementation is there, already, in the guise of (gcast Refl). We would just shuffle the definitions around a bit. Am I indeed missing

something?

I think that is the case indeed. Though I agree that it would be a nice addition to Data.Typeable.

This thread is a few months old now, but it looks like people were generally in favor of adding (gcast Refl) to Data.Typeable. I've used it in real code in at least one place since then (where I just defined it locally). It doesn't look like it's actually been added, though -- is it planned to go into HEAD eventually?

Shachaf

There seems to be a small tangle. The proposal includes deprecating gcast1 and gcast2 in favor of the poly-kinded gcast. But, there is a small discrepancy between these. Here are the type signatures:

gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b) gcast1 :: forall c t t' a. (Typeable (t :: * -> *), Typeable t') => c (t a) -> Maybe (c (t' a))

The difference is that gcast1 does *not* require the variable `a` to be Typeable, whereas defining gcast1 = gcast does require this. Not requiring `a` to be Typeable seems correct to me, as the type signature of gcast1 requires both uses of `a` to be the same. But, gcast isn't smart enough to know that. Here are some ideas of how to proceed: - Keep gcast1 and gcast2 undeprecated. - Require clients to add more Typeable constraints (for example, in Data.Data) to get their code to compile with gcast. - Come up with some other workaround, but none is striking me at the moment. Thoughts? Richard On 2013-07-22 09:44, Richard Eisenberg wrote:

I was waiting to respond to Shachaf's email saying "pushed", but instead, I have to say "currently validating".

Expect this by the end of the day. Sorry it's taken so long!

Richard

On 2013-07-22 09:23, José Pedro Magalhães wrote:

...

Thanks for bringing this up again. This was started in my data-proxy branch of base [1], but never really finished. We definitely want to have this in 7.8, and I think there's only some minor finishing work to do (check if we have all the instances we want, document, etc.). Perhaps you can look through what's there already, and what you think is missing? I'm more than happy to accept contributing patches too :-)

Thanks, Pedro

On Sun, Jul 21, 2013 at 3:09 AM, Shachaf Ben-Kiki wrote:

...

On Mon, Mar 4, 2013 at 11:12 AM, José Pedro Magalhães wrote:

...

Hi,

On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg wrote:

...

Unless I'm missing something, this all looks very

straightforward. The

...

implementation is there, already, in the guise of (gcast Refl). We would just shuffle the definitions around a bit. Am I indeed missing something?

I think that is the case indeed. Though I agree that it would be a nice addition to Data.Typeable.

This thread is a few months old now, but it looks like people were generally in favor of adding (gcast Refl) to Data.Typeable. I've used it in real code in at least one place since then (where I just defined it locally). It doesn't look like it's actually been added, though -- is it planned to go into HEAD eventually?

    Shachaf

Links: ------ [1] https://github.com/ghc/packages-base/tree/data-proxy

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

I favor keeping them undeprecated as I currently have code that needs the lack of a Typeable constraint there in cases where the argument plays a similar role to the region parameter for ST s, where it *can't* be made Typeable! On the plus side, you may be able to eliminate the requirement that the arguments be of kind * though, rather dramatically increasing the utility of gcast1 and gcast2. -Edward On Jul 22, 2013, at 5:38 AM, José Pedro Magalhães wrote:

Hi,

On Mon, Jul 22, 2013 at 10:19 AM, Richard Eisenberg wrote:

...

There seems to be a small tangle. The proposal includes deprecating gcast1 and gcast2 in favor of the poly-kinded gcast. But, there is a small discrepancy between these. Here are the type signatures:

...

gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b) gcast1 :: forall c t t' a. (Typeable (t :: * -> *), Typeable t') => c (t a) -> Maybe (c (t' a))

The difference is that gcast1 does *not* require the variable `a` to be Typeable, whereas defining gcast1 = gcast does require this. Not requiring `a` to be Typeable seems correct to me, as the type signature of gcast1 requires both uses of `a` to be the same. But, gcast isn't smart enough to know that. Here are some ideas of how to proceed:

- Keep gcast1 and gcast2 undeprecated.

I'd say we should go for this first option, because the second one is pretty bad.

Cheers, Pedro

...

- Require clients to add more Typeable constraints (for example, in Data.Data) to get their code to compile with gcast. - Come up with some other workaround, but none is striking me at the moment.

Thoughts?

Richard

On 2013-07-22 09:44, Richard Eisenberg wrote:

...

I was waiting to respond to Shachaf's email saying "pushed", but instead, I have to say "currently validating".

Expect this by the end of the day. Sorry it's taken so long!

Richard

On 2013-07-22 09:23, José Pedro Magalhães wrote:

...

Thanks for bringing this up again. This was started in my data-proxy branch of base [1], but never really finished. We definitely want to have this in 7.8, and I think there's only some minor finishing work to do (check if we have all the instances we want, document, etc.). Perhaps you can look through what's there already, and what you think is missing? I'm more than happy to accept contributing patches too :-)

Thanks, Pedro

On Sun, Jul 21, 2013 at 3:09 AM, Shachaf Ben-Kiki wrote:

...

On Mon, Mar 4, 2013 at 11:12 AM, José Pedro Magalhães wrote:

...

Hi,

On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg wrote: > > Unless I'm missing something, this all looks very straightforward. The > implementation is there, already, in the guise of (gcast Refl). We would > just shuffle the definitions around a bit. Am I indeed missing something?

I think that is the case indeed. Though I agree that it would be a nice addition to Data.Typeable.

This thread is a few months old now, but it looks like people were generally in favor of adding (gcast Refl) to Data.Typeable. I've used it in real code in at least one place since then (where I just defined it locally). It doesn't look like it's actually been added, though -- is it planned to go into HEAD eventually?

Shachaf

Links: ------ [1] https://github.com/ghc/packages-base/tree/data-proxy

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

If we have gcast1 then can't the others just be applications of that under various wrappers? In practice we should be able to implement gcast2 by working on a single argument with a product kind, and so on and so forth, but we need at least gcast1 as a base case. In theory this is the more fundamental operation, and gcast is defineable in terms of gcast1 with a wrapper with a unit-kinded argument, but I wouldn't want to invert the relationship. This is based on the same trick that Conor uses to show that a single (poly-kinded) type argument is enough for all of the indexed monad machinery, no matter how complicated it gets. *tl;dr* We only need gcast1, the others are window-dressing. -Edward On Mon, Jul 22, 2013 at 9:31 PM, Simon Peyton-Jones wrote:

Harump. There is *still* an infinite family going on here, isn't there?

gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)

but what about this

gcast_2 :: forall a b c d e. (Typeable a, Typeable b, Typeable d, Typeable e) => c a b -> c d e

Then, as you point out, we have gcast1 and 2 (etc). And there are more. What about

gcast1' :: forall c t a a'. (Typeable a, Typeable a') => c (t a) -> Maybe (c (t a'))

One could imagine all sorts of combinations of bits that stay the same (and hence do not need to be Typeable) and bits that change (and hence do need to be Typable).

As Edward says, all these functions can be polykinded, which makes them more useful, but there still seem too many of them.

I wonder if we could instead make a combinatory library that lets us build these functions easily. It think we are going to offer a function that computes an equality witness:

mkEqWit :: (Typable a, Typeable b) => Maybe (EQ a b)

Now we need to be able to compose witnesses:

appEqWit :: Eq a b -> Eq c d -> Eq (a c) (b d) reflEqWit :: Eq a a

Now, I think you can make all those other casts.

Would that do the job better?

Simon

| -----Original Message----- | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | Sent: 22 July 2013 10:20 | To: José Pedro Magalhães | Cc: Dimitrios Vytiniotis; Simon Peyton-Jones; Stephanie Weirich; | josepedromagalhaes@gmail.com; libraries@haskell.org; Conor McBride | Subject: Re: new-typeable, new cast? | | There seems to be a small tangle. The proposal includes deprecating | gcast1 and gcast2 in favor of the poly-kinded gcast. But, there is a | small discrepancy between these. Here are the type signatures: | | > gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b) | > gcast1 :: forall c t t' a. (Typeable (t :: * -> *), Typeable t') | > => c (t a) -> Maybe (c (t' a)) | | The difference is that gcast1 does *not* require the variable `a` to be | Typeable, whereas defining gcast1 = gcast does require this. Not | requiring `a` to be Typeable seems correct to me, as the type signature | of gcast1 requires both uses of `a` to be the same. But, gcast isn't | smart enough to know that. Here are some ideas of how to proceed: | | - Keep gcast1 and gcast2 undeprecated. | - Require clients to add more Typeable constraints (for example, in | Data.Data) to get their code to compile with gcast. | - Come up with some other workaround, but none is striking me at the | moment. | | Thoughts? | | Richard | | On 2013-07-22 09:44, Richard Eisenberg wrote: | > I was waiting to respond to Shachaf's email saying "pushed", but | > instead, I have to say "currently validating". | > | > Expect this by the end of the day. Sorry it's taken so long! | > | > Richard | > | > On 2013-07-22 09:23, José Pedro Magalhães wrote: | >> Thanks for bringing this up again. This was started in my data-proxy | >> branch of base [1], | >> but never really finished. We definitely want to have this in 7.8, and | >> I think there's | >> only some minor finishing work to do (check if we have all the | >> instances we want, | >> document, etc.). Perhaps you can look through what's there already, | >> and what you | >> think is missing? I'm more than happy to accept contributing patches | >> too :-) | >> | >> Thanks, | >> Pedro | >> | >> On Sun, Jul 21, 2013 at 3:09 AM, Shachaf Ben-Kiki

...

| >> wrote: | >> | >>> On Mon, Mar 4, 2013 at 11:12 AM, José Pedro Magalhães | >>> wrote: | >>>> Hi, | >>>> | >>>> On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg | >>> wrote: | >>>>> | >>>>> Unless I'm missing something, this all looks very | >>> straightforward. The | >>>>> implementation is there, already, in the guise of (gcast Refl). | >>> We would | >>>>> just shuffle the definitions around a bit. Am I indeed missing | >>> something? | >>>> | >>>> | >>>> I think that is the case indeed. Though I agree that it would be | >>> a nice | >>>> addition to Data.Typeable. | >>>> | >>>> | >>> | >>> This thread is a few months old now, but it looks like people were | >>> generally in favor of adding (gcast Refl) to Data.Typeable. I've | >>> used | >>> it in real code in at least one place since then (where I just | >>> defined | >>> it locally). It doesn't look like it's actually been added, though | >>> -- | >>> is it planned to go into HEAD eventually? | >>> | >>> Shachaf | >> | >> | >> | >> Links: | >> ------ | >> [1] https://github.com/ghc/packages-base/tree/data-proxy | > | > _______________________________________________ | > Libraries mailing list | > Libraries@haskell.org | > http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

Well, there was another surprise. Haddock can't deal with Proxy for some reason. (It dies with the error "synifyKind". I looked but couldn't figure out what was going on there.) I've posted a bug report on the haddock Trac (http://trac.haskell.org/haddock/ticket/242), but validation currently fails on the branch (data-proxy) with this work in it. So, I can't merge with master. At this point, I'm going to wait until the haddock folks fix that bug, then assuming all is well, I will merge. Richard On 2013-07-23 09:59, Richard Eisenberg wrote:

I think that we really only need (eqT :: (Typeable a, Typeable b) => Maybe (a :=: b)). All of the gcasts can be defined in terms of that function.

However, I concretely propose (and plan to do) this: Leave gcast1 and gcast2 in and undeprecated. Simon is right that there is an infinite family of gcasts, and there may be no great reason to have gcast1 and gcast2 and none of the others, but there also doesn't seem to be a compelling reason to remove them (or deprecate them) and break code. In any case, this debate doesn't seem to be a good reason to hold up wrapping the rest of these details up, because we can always revisit and add or remove functions in the coming weeks. I'm not trying to ramrod my ideas through here, just trying to favor action over inaction -- anyone can feel free to come back and make edits after I push.

Barring another surprise, I believe I'll push before lunch (in the UK).

Richard

On 2013-07-23 03:04, Edward Kmett wrote:

...

If we have gcast1 then can't the others just be applications of that under various wrappers?

In practice we should be able to implement gcast2 by working on a single argument with a product kind, and so on and so forth, but we need at least gcast1 as a base case.

In theory this is the more fundamental operation, and gcast is defineable in terms of gcast1 with a wrapper with a unit-kinded argument, but I wouldn't want to invert the relationship.

This is based on the same trick that Conor uses to show that a single (poly-kinded) type argument is enough for all of the indexed monad machinery, no matter how complicated it gets.

TL;DR We only need gcast1, the others are window-dressing.

-Edward

On Mon, Jul 22, 2013 at 9:31 PM, Simon Peyton-Jones wrote:

...

Harump.  There is *still* an infinite family going on here, isn't there?

gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)

but what about this

gcast_2 :: forall a b c d e. (Typeable a, Typeable b, Typeable d, Typeable e)              => c a b -> c d e

Then, as you point out, we have gcast1 and 2 (etc).  And there are more.  What about

gcast1' :: forall c t a a'. (Typeable a, Typeable a')        => c (t a) -> Maybe (c (t a'))

One could imagine all sorts of combinations of bits that stay the same (and hence do not need to be Typeable) and bits that change (and hence do need to be Typable).

As Edward says, all these functions can be polykinded, which makes them more useful, but there still seem too many of them.

I wonder if we could instead make a combinatory library that lets us build these functions easily.  It think we are going to offer a function that computes an equality witness:

mkEqWit :: (Typable a, Typeable b) => Maybe (EQ a b)

Now we need to be able to compose witnesses:

appEqWit :: Eq a b -> Eq c d -> Eq (a c) (b d) reflEqWit :: Eq a a

Now, I think you can make all those other casts.

Would that do the job better?

Simon

|  -----Original Message----- |  From: Richard Eisenberg [mailto:eir@cis.upenn.edu] |  Sent: 22 July 2013 10:20 |  To: José Pedro Magalhães |  Cc: Dimitrios Vytiniotis; Simon Peyton-Jones; Stephanie Weirich; |  josepedromagalhaes@gmail.com; libraries@haskell.org; Conor McBride |  Subject: Re: new-typeable, new cast? |

|  There seems to be a small tangle. The proposal includes deprecating |  gcast1 and gcast2 in favor of the poly-kinded gcast. But, there is a |  small discrepancy between these. Here are the type signatures: | |  > gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b) |  > gcast1 :: forall c t t' a. (Typeable (t :: * -> *), Typeable t') |  >        => c (t a) -> Maybe (c (t' a)) | |  The difference is that gcast1 does *not* require the variable `a` to be |  Typeable, whereas defining gcast1 = gcast does require this. Not |  requiring `a` to be Typeable seems correct to me, as the type signature |  of gcast1 requires both uses of `a` to be the same. But, gcast isn't |  smart enough to know that. Here are some ideas of how to proceed: | |  - Keep gcast1 and gcast2 undeprecated. |  - Require clients to add more Typeable constraints (for example, in |  Data.Data) to get their code to compile with gcast. |  - Come up with some other workaround, but none is striking me at the |  moment. | |  Thoughts? | |  Richard | |  On 2013-07-22 09:44, Richard Eisenberg wrote: |  > I was waiting to respond to Shachaf's email saying "pushed", but |  > instead, I have to say "currently validating". |  > |  > Expect this by the end of the day. Sorry it's taken so long! |  > |  > Richard |  > |  > On 2013-07-22 09:23, José Pedro Magalhães wrote: |  >> Thanks for bringing this up again. This was started in my data-proxy |  >> branch of base [1], |  >> but never really finished. We definitely want to have this in 7.8, and |  >> I think there's |  >>  only some minor finishing work to do (check if we have all the |  >> instances we want, |  >> document, etc.). Perhaps you can look through what's there already, |  >> and what you |  >> think is missing? I'm more than happy to accept contributing patches |  >> too :-) |  >> |  >> Thanks, |  >> Pedro |  >> |  >> On Sun, Jul 21, 2013 at 3:09 AM, Shachaf Ben-Kiki |  >> wrote: |  >> |  >>> On Mon, Mar 4, 2013 at 11:12 AM, José Pedro Magalhães |  >>> wrote: |  >>>> Hi, |  >>>> |  >>>> On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg |  >>> wrote: |  >>>>> |  >>>>> Unless I'm missing something, this all looks very |  >>> straightforward. The |  >>>>> implementation is there, already, in the guise of (gcast Refl). |  >>> We would |  >>>>> just shuffle the definitions around a bit. Am I indeed missing |  >>> something? |  >>>> |  >>>> |  >>>> I think that is the case indeed. Though I agree that it would be |  >>> a nice |  >>>> addition to Data.Typeable. |  >>>> |  >>>> |  >>> |  >>> This thread is a few months old now, but it looks like people were |  >>> generally in favor of adding (gcast Refl) to Data.Typeable. I've |  >>> used |  >>> it in real code in at least one place since then (where I just |  >>> defined |  >>> it locally). It doesn't look like it's actually been added, though |  >>> -- |  >>> is it planned to go into HEAD eventually? |  >>> |  >>>     Shachaf |  >> |  >> |  >> |  >> Links: |  >> ------ |  >> [1] https://github.com/ghc/packages-base/tree/data-proxy [1] |  > |  > _______________________________________________ |  > Libraries mailing list |  > Libraries@haskell.org |  > http://www.haskell.org/mailman/listinfo/libraries [2]

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries [2]

Links: ------ [1] https://github.com/ghc/packages-base/tree/data-proxy [2] http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

I would really want to keep asProxyTypeOf around as it is commonly used and has no other plausible home within tagged. reproxy is quite negotiable. Ever since its signature was generalized a version or two ago in tagged, it has started to feel quite silly. If I move coerce :: (Functor f, Contravariant f) => f a -> f b coerce = contramap absurd . fmap absurd -- using absurd from 'void' -- or equivalently: coerce = contramap (const ()) . fmap (const ()) from lens up into the contravariant package, then the role that function plays can be replaced entirely with that more general purpose combinator in "user land" without needing any funny looking functions in base. Proxy is both Contravariant and a normal covariant Functor as it doesn't use its argument, just like Const m. reproxy originally witnessed this fact just for Proxy, but that fact in its broader generality has since been exploited to make getters and folds in lens, so reproxy is basically just residue of an old approach. -Edward On Tue, Jul 30, 2013 at 6:44 PM, Shachaf Ben-Kiki wrote:

On Mon, Jul 22, 2013 at 1:23 AM, José Pedro Magalhães wrote:

...

Thanks for bringing this up again. This was started in my data-proxy branch of base, but never really finished. We definitely want to have this in 7.8, and I think there's only some minor finishing work to do (check if we have all the instances we want, document, etc.). Perhaps you can look through what's there already, and what you think is missing? I'm more than happy to accept contributing patches too :-)

I'm looking at the current state of Data.Proxy in base (it looks like Richard merged data-proxy into master) and it looks pretty good instance-wise. Issues I'm aware of:

* It looks like there's a SafeHaskell issue -- should this be marked Trustworthy? See https://github.com/ekmett/tagged/pull/13 * tagged's Data.Proxy defines some useful functions that aren't present in base. Two of them can move into tagged's Data.Tagged, but the other two should probably go in base's Data.Proxy. In particular

asProxyTypeOf :: a -> proxy a -> a asProxyTypeOf = const

reproxy :: proxy s -> Proxy t reproxy _ = Proxy

When these are fixed, tagged can probably shuffle a couple of functions around and then use base's Data.Proxy rather than exporting its own module (for GHC ≥ 7.7).

(By the way: Some instances are slightly different from what GHC would derive -- e.g. «_ == _ = True» is different from «Proxy == Proxy = True», which is ()'s Eq behavior. I think this is OK but I wanted to mention it.)

Thanks, Shachaf

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

On Wed, Jul 31, 2013 at 09:38:06AM +0100, Richard Eisenberg wrote:

As for the instances' behavior being different from GHC's generated versions, I think the lazier ones (as implemented) are probably more useful.

My instinct is to disagree. It's like how case with a single pattern is still strict -- I expect (==) to do some work even if in principle it doesn't have to. And indeed if () behaves that way I would expect Proxy to do the same. I'm not critically affected by the decision one way or the other though, so don't disrupt anything on my account.

If I don't hear otherwise by the end of the day, I'll push these changes.

Richard

On 2013-07-31 00:35, Edward Kmett wrote:

...

I would really want to keep asProxyTypeOf around as it is commonly used and has no other plausible home within tagged. 

reproxy is quite negotiable.

Ever since its signature was generalized a version or two ago in tagged, it has started to feel quite silly.

If I move

coerce :: (Functor f, Contravariant f) => f a -> f b coerce = contramap absurd . fmap absurd -- using absurd from 'void' -- or equivalently:  coerce = contramap (const ()) . fmap (const ())

from lens up into the contravariant package, then the role that function plays can be replaced entirely with that more general purpose combinator in "user land" without needing any funny looking functions in base.

Proxy is both Contravariant and a normal covariant Functor as it doesn't use its argument, just like Const m. reproxy originally witnessed this fact just for Proxy, but that fact in its broader generality has since been exploited to make getters and folds in lens, so reproxy is basically just residue of an old approach.

-Edward

On Tue, Jul 30, 2013 at 6:44 PM, Shachaf Ben-Kiki wrote:

...

...

Thanks for bringing this up again. This was started in my data-proxy branch of base, but never really finished. We definitely want to have this in 7.8, and I think there's only some minor finishing work to do (check if we have all the instances we want, document, etc.). Perhaps you can look through what's there already, and what you think is missing? I'm more than happy to accept contributing

On Mon, Jul 22, 2013 at 1:23 AM, José Pedro Magalhães wrote: patches too :-)

...

I'm looking at the current state of Data.Proxy in base (it looks like Richard merged data-proxy into master) and it looks pretty good instance-wise. Issues I'm aware of:

* It looks like there's a SafeHaskell issue -- should this be marked Trustworthy? See https://github.com/ekmett/tagged/pull/13 [1] * tagged's Data.Proxy defines some useful functions that aren't present in base. Two of them can move into tagged's Data.Tagged, but the other two should probably go in base's Data.Proxy. In particular

asProxyTypeOf :: a -> proxy a -> a asProxyTypeOf = const

reproxy :: proxy s -> Proxy t reproxy _ = Proxy

When these are fixed, tagged can probably shuffle a couple of functions around and then use base's Data.Proxy rather than exporting its own module (for GHC ≥ 7.7).

(By the way: Some instances are slightly different from what GHC would derive -- e.g. «_ == _ = True» is different from «Proxy == Proxy = True», which is ()'s Eq behavior. I think this is OK but I wanted to mention it.)

Thanks,

    Shachaf

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries [2]

Links: ------ [1] https://github.com/ekmett/tagged/pull/13 [2] http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

Hello, Could we perhaps have a better (shorter) name for asProxyTypeOf? I ended up with [1] in one of my libraries (hintType2, hintType1Of2, hintType2Of2 could also be useful). I would like to suggest adding proxy values for standard types (aUnit, aChar, etc in the link) as well, should I make a separate proposal (one could imagine a special syntax for proxy values, e.g. expr `hintTypeArg` ''Type built in the compiler, but that would take years to land...)? [1] http://hackage.haskell.org/packages/archive/data-textual/0.1/doc/html/Data-T... On 07/31/2013 03:35 AM, Edward Kmett wrote:

I would really want to keep asProxyTypeOf around as it is commonly used and has no other plausible home within tagged.

reproxy is quite negotiable.

Ever since its signature was generalized a version or two ago in tagged, it has started to feel quite silly.

If I move

coerce :: (Functor f, Contravariant f) => f a -> f b coerce = contramap absurd . fmap absurd -- using absurd from 'void' -- or equivalently: coerce = contramap (const ()) . fmap (const ())

from lens up into the contravariant package, then the role that function plays can be replaced entirely with that more general purpose combinator in "user land" without needing any funny looking functions in base.

Proxy is both Contravariant and a normal covariant Functor as it doesn't use its argument, just like Const m. reproxy originally witnessed this fact just for Proxy, but that fact in its broader generality has since been exploited to make getters and folds in lens, so reproxy is basically just residue of an old approach.

-Edward

On Tue, Jul 30, 2013 at 6:44 PM, Shachaf Ben-Kiki mailto:shachaf@gmail.com> wrote:

On Mon, Jul 22, 2013 at 1:23 AM, José Pedro Magalhães mailto:jpm@cs.uu.nl> wrote: > Thanks for bringing this up again. This was started in my data-proxy branch > of base, > but never really finished. We definitely want to have this in 7.8, and I > think there's > only some minor finishing work to do (check if we have all the instances we > want, > document, etc.). Perhaps you can look through what's there already, and what > you > think is missing? I'm more than happy to accept contributing patches too :-) > >

I'm looking at the current state of Data.Proxy in base (it looks like Richard merged data-proxy into master) and it looks pretty good instance-wise. Issues I'm aware of:

* It looks like there's a SafeHaskell issue -- should this be marked Trustworthy? See https://github.com/ekmett/tagged/pull/13 * tagged's Data.Proxy defines some useful functions that aren't present in base. Two of them can move into tagged's Data.Tagged, but the other two should probably go in base's Data.Proxy. In particular

asProxyTypeOf :: a -> proxy a -> a asProxyTypeOf = const

reproxy :: proxy s -> Proxy t reproxy _ = Proxy

When these are fixed, tagged can probably shuffle a couple of functions around and then use base's Data.Proxy rather than exporting its own module (for GHC ≥ 7.7).

(By the way: Some instances are slightly different from what GHC would derive -- e.g. «_ == _ = True» is different from «Proxy == Proxy = True», which is ()'s Eq behavior. I think this is OK but I wanted to mention it.)

Thanks, Shachaf

_______________________________________________ Libraries mailing list Libraries@haskell.org mailto:Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries