I'm a big fan of this! There aren't any covariant occurrences of Proxy in the Typeable use-case. So it really doesn't need an explicit Proxy type at all. Both the tagged and reflection packages go out of their way to make all contravariant uses agnostic about the proxy type. This rather dramatically cuts down on the amount of ScopedTypeVariable noise I need to use in my code, because I can often just pass a container holding values of the correct type directly as my "Proxy" when I have one. -Edward On Sat, Jan 26, 2013 at 3:27 AM, Roman Cheplyaka wrote:

Very nice idea! Thanks for bringing it up.

The only case I can see when this "proxyless" approach wouldn't work is if Proxy ever has to be in a covariant position (e.g. returned by a function). Then you'd need either a concrete proxy or an existential wrapper.

If there are no such functions in the new Data.Typeable (which is very plausible), then I'd prefer not to include Proxy into base, given that it's already provided by an alternative package.

Roman

* Shachaf Ben-Kiki [2013-01-25 20:07:10-0800]

...

I see that the new-typeable branch in GHC is using "typeRep :: forall a. Typeable a => Proxy a -> TypeRep" rather than "typeOf :: forall a. Typeable a => a -> TypeRep". This is clearly a big improvement over using undefined everywhere.

I'd like to suggest a small change, if it hasn't been brought up before -- "typeRep :: forall proxy a. Typeable a => proxy a -> TypeRep". This makes typeRep compatible with any other Proxy type, since it doesn't use any properties of the concrete type -- it just uses it to pass information about the "a". Things that consume a Proxy don't ever need to refer to Proxy explicitly.

This would make Typeable compatible with other Proxy libraries, like the one in "tagged". It would also make it compatible with any other type of kind * -> * -- for example, "typeRep ([] :: [Int])" would be a valid, and arguable more convenient, syntax for using typeRep. "Nothing :: Maybe Int" and so on would work too. So things that produce a "proxy" don't need to refer to Proxy explicitly either.

Possibly this would make the Proxy type entirely unnecessary. If it stays, though, I suggest that it belongs in a module other than Data.Typeable.Internal -- it's a useful type for many other things, and as long as it's in base and exposed to users, it might as well be treated as a type in its own right. It's also a monad, can provide a variant of `asTypeOf`, and so on.

Shachaf

_______________________________________________ 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

Yes, it's entirely unproblematic, and a good suggestion. Thanks, Pedro On Sat, Jan 26, 2013 at 6:36 PM, Simon Peyton-Jones wrote:

Good idea! Simple, and I see no downsides.

Pedro is putting in place a new Typeable library (using kind polymorphism) for GHC 7.8. Pedro, might you incorporate this?

Simon

| -----Original Message----- | From: libraries-bounces@haskell.org [mailto: libraries-bounces@haskell.org] On | Behalf Of Shachaf Ben-Kiki | Sent: 26 January 2013 04:07 | To: libraries@haskell.org | Subject: Proxy and new-typeable | | I see that the new-typeable branch in GHC is using "typeRep :: forall a. | Typeable a => Proxy a -> TypeRep" rather than "typeOf :: forall a. Typeable a | => a -> TypeRep". This is clearly a big improvement over using undefined | everywhere. | | I'd like to suggest a small change, if it hasn't been brought up before -- | "typeRep :: forall proxy a. Typeable a => proxy a -> TypeRep". This makes | typeRep compatible with any other Proxy type, since it doesn't use any | properties of the concrete type -- it just uses it to pass information about | the "a". Things that consume a Proxy don't ever need to refer to Proxy | explicitly. | | This would make Typeable compatible with other Proxy libraries, like the one in | "tagged". It would also make it compatible with any other type of kind * -> * | -- for example, "typeRep ([] :: [Int])" would be a valid, and arguable more | convenient, syntax for using typeRep. "Nothing :: Maybe Int" and so on would | work too. So things that produce a "proxy" don't need to refer to Proxy | explicitly either. | | Possibly this would make the Proxy type entirely unnecessary. If it stays, | though, I suggest that it belongs in a module other than Data.Typeable.Internal | -- it's a useful type for many other things, and as long as it's in base and | exposed to users, it might as well be treated as a type in its own right. It's | also a monad, can provide a variant of `asTypeOf`, and so on. | | Shachaf | | _______________________________________________ | Libraries mailing list | Libraries@haskell.org | http://www.haskell.org/mailman/listinfo/libraries

+1 for finding a resolution. The idea of another Proxy floating around fills me with unease. -Edward On Tue, Mar 19, 2013 at 7:48 PM, Ben Gamari wrote:

José Pedro Magalhães writes:

...

Yes, it's entirely unproblematic, and a good suggestion.

What happened to this proposal? As far as I can tell the new-typeable work is in (or rather, the branch has been deleted) yet Data.Typeable still seems to have its own Proxy. Given that there has been talk of a 7.8 release, this should probably be resolved quickly (although it's not clear to me from the massive thread where that discussion concluded).

Cheers,

- Ben

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

If you insist on adding Proxy to Data.Typeable, I'd like to strongly suggest that we might want to look at promoting Data.Proxy from the tagged package to base. It offers a lot of instances that I currently rely upon in production code and is already in use in a large portion of the ~42 reverse dependencies of that package: http://packdeps.haskellers.com/reverse/tagged Of course we could invert the dependencies from packages outside of base at that time. Exporting a crippled Proxy from Data.Typeable *without* those instances will basically just ensure that I need to somehow support both, fight needlessly with orphans and/or deal with qualified imports everywhere, and it will break about 3 dozen modules of mine, and impact others. All in all this makes me personally rather strongly opposed to the idea of just randomly throwing a Proxy type in the module without ensuring we don't lose existing functionality along the way. -Edward On Wed, Mar 20, 2013 at 4:04 AM, José Pedro Magalhães wrote:

Data.Typeable no longer uses Proxy, yet I think it is convenient to have a Proxy datatype defined somewhere in base, and re-export it from Data.Typeable, as you might often often want to use it.

Cheers, Pedro

On Wed, Mar 20, 2013 at 12:35 AM, Edward Kmett wrote:

...

+1 for finding a resolution. The idea of another Proxy floating around fills me with unease.

-Edward

On Tue, Mar 19, 2013 at 7:48 PM, Ben Gamari wrote:

...

José Pedro Magalhães writes:

...

Yes, it's entirely unproblematic, and a good suggestion.

What happened to this proposal? As far as I can tell the new-typeable work is in (or rather, the branch has been deleted) yet Data.Typeable still seems to have its own Proxy. Given that there has been talk of a 7.8 release, this should probably be resolved quickly (although it's not clear to me from the massive thread where that discussion concluded).

Cheers,

- Ben

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

My main concern is that many of the modules I import Proxy in already import Typeable. So if we're going to pick up the functionality of having a 'standard' Proxy, I'd rather not lose the functionality of having it trivially Applicative, Eq, Ord, even Enum and Bounded, etc. makes it much easier to work with in practice, and useful for many situations you wouldn't immediately expect. Yes, Typeable is Proxy-agnostic, but the moment you standardize on something like that the immediate second order consequence is I get 20 emails from people asking me why I'm not using the standard one. If we can agree to implement all the instances we can sanely implement for Proxy (and yes, there are a lot of non-obvious ones) then this is a non-issue. If Proxy is just something where you intend to offer a minimalist interface explicitly for the narrow use case you've currently envisioned, then I would ague that in my experience that assuming you know how something will be used is a great way to screw over users. The existing Data.Proxy has been used as the representation of Data.Tagged as a representable profunctor. It serves as a trivial Applicative, etc. If you add Proxy to Typeable, if its done by bringing the existing Data.Proxy module into base (sans a few of my more peculiar non-base instances) and then re-exporting it from Data.Typeable then my upgrade path is that I emit a new version of 'tagged' without Proxy and I add version conditional exports of all of my other instances to those modules. Existing users of Data.Proxy can then easily support versions before and after GHC 7.7 and no functionality is lost. If you add Proxy to Typeable and do not do so, then it is less than useful to me as it fragments the existing users between two different types, and gives me no story for how I straddle support for pre 7.7 and post-7.7 GHC. I am locked into a choice between two options: 1.) Continuing to support Data.Proxy, which is now completely redundant except for the fact that I have more instances for standard types. 2.) If I choose to pay the price of losing the existing functionality in order to accept a more "standard" version of the type, by having me re-export it from Data.Proxy in GHC > 7.7 then I lose existing functionality or have to orphan a ton of instances. Perhaps my explanation being so long winded has made it seem more complicated than it is, but really it just comes down to me asking that if you want Data.Proxy in Typeable, then please make sure to implement *all*the instances. =) -Edward On Wed, Mar 20, 2013 at 5:17 AM, Roman Cheplyaka wrote:

Right now Data.Typeable is proxy-agnostic. The proposal is just to export a Proxy type for convenience (alternatively, the user can define her own Proxy or use one from tagged). What exactly forces you to support both proxies in your code?

(I'm reluctant to have many proxy types scattered around mainly because of unnecessary name conflicts, but I'd like to understand your concerns too.)

Roman

* Edward Kmett [2013-03-20 04:48:49-0400]

...

If you insist on adding Proxy to Data.Typeable, I'd like to strongly suggest that we might want to look at promoting Data.Proxy from the tagged package to base.

It offers a lot of instances that I currently rely upon in production code and is already in use in a large portion of the ~42 reverse dependencies of that package:

http://packdeps.haskellers.com/reverse/tagged

Of course we could invert the dependencies from packages outside of base at that time.

Exporting a crippled Proxy from Data.Typeable *without* those instances will basically just ensure that I need to somehow support both, fight needlessly with orphans and/or deal with qualified imports everywhere, and it will break about 3 dozen modules of mine, and impact others.

All in all this makes me personally rather strongly opposed to the idea of just randomly throwing a Proxy type in the module without ensuring we don't lose existing functionality along the way.

-Edward

On Wed, Mar 20, 2013 at 4:04 AM, José Pedro Magalhães wrote:

...

Data.Typeable no longer uses Proxy, yet I think it is convenient to have a Proxy datatype defined somewhere in base, and re-export it from Data.Typeable, as you might often often want to use it.

Cheers, Pedro

On Wed, Mar 20, 2013 at 12:35 AM, Edward Kmett wrote:

...

+1 for finding a resolution. The idea of another Proxy floating around fills me with unease.

-Edward

On Tue, Mar 19, 2013 at 7:48 PM, Ben Gamari

...

José Pedro Magalhães writes:

...

Yes, it's entirely unproblematic, and a good suggestion.

What happened to this proposal? As far as I can tell the new-typeable work is in (or rather, the branch has been deleted) yet Data.Typeable still seems to have its own Proxy. Given that there has been talk of a 7.8 release, this should probably be resolved quickly (although it's not clear to me from the massive thread where that discussion concluded).

Cheers,

- Ben

_______________________________________________ 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

Ben Gamari writes:

It seems the options before us are,

a) Use Proxy strictly internally in Data.Typeable. In this case users will continue to use the Proxy types in tagged and elsewhere as they already happily do

b) Export Proxy from Data.Typeable in its current state, accepting that users relying on external Proxy types will need to either accept a loss of functionality, explicitly hide Typeable's Proxy, or rely on orphan instances

c) Find a way to bring Typeable's Proxy type to a level of functionality comparable to that currently available outside of base

Shortly after I sent this Shachaf reminded me of the (perhaps obvious in hindsight) option (d): move the Proxy type into a new module. While I'm admittedly not very familiar with the module system, I can certainly see how moving Proxy might help avoid cycles. I can try this in the morning. It may be that (c) isn't as infeasible as I had thought. Cheers, - Ben

On Fri, Mar 22, 2013 at 1:25 AM, Edward Kmett wrote:

On Fri, Mar 22, 2013 at 12:03 AM, Ben Gamari wrote:

...

Roman Cheplyaka writes:

...

Right now Data.Typeable is proxy-agnostic. The proposal is just to export a Proxy type for convenience (alternatively, the user can define her own Proxy or use one from tagged). What exactly forces you to support both proxies in your code?

(I'm reluctant to have many proxy types scattered around mainly because of unnecessary name conflicts, but I'd like to understand your concerns too.)

It seems the options before us are,

a) Use Proxy strictly internally in Data.Typeable. In this case users will continue to use the Proxy types in tagged and elsewhere as they already happily do

b) Export Proxy from Data.Typeable in its current state, accepting that users relying on external Proxy types will need to either accept a loss of functionality, explicitly hide Typeable's Proxy, or rely on orphan instances

c) Find a way to bring Typeable's Proxy type to a level of functionality comparable to that currently available outside of base

Having tried to compile a good amount of code using Data.Typeable's Proxy, it seems clear to me that (b) is the worst of the three outcomes. There are a good number of packages which rely on the instances provided by external Proxy types. Removing these will bring great deal of pain in the short turn and pose a large maintenance burden moving forward.

Tonight I tried to implement (c) but found that this might be quite tricky without establishing some very brittle cyclic imports in base. As it stands, nearly everything in base imports Typeable somehow. Requiring Typeable to in turn import Applicative, Foldable, Traversable, and others places some very unfortunate cycles in the dependency structure. Even after an hour of hacking and 200 lines of changes, I still hadn't succeeded in getting base to build with a reasonable set of Proxy instances (although, admittedly, this might just be due to my inexperience with this sort of issue).

You don't need to make it cyclic, if the edge already exists one way in the graph just follow it back and put the instance with the class.

...

In light of these points, I believe that (a) is the course of least pain. Those users that need Proxy already happily rely on packages outside of base. Meanwhile base can use its own (necessarily minimal) Proxy internally without issue. This approach requires minimal changes in base and avoids unnecessary breakage of user code, all while depriving no one of current or future functionality. Admittedly, there may be a couple more Proxy types in the namespace than would otherwise exist, but this seems like a small price to pay to avoid the breakage and pain of (b) and (c) above.

I would be happy with (a) or (c).

That said, given (c) I could make Data.Proxy in tagged re-export the Data.Typeable Proxy whenever we're on a new enough GHC and I can invert all the other dependency edges. It'll be work for me, but it means that when a user goes to mix the existing tagged Proxy with code from Data.Typeable it 'just works' and there aren't two types named Proxy floating around that'll have lots of users.

It seems to me that if Proxy is going to be exported from base, it should go in its own module -- it doesn't have much to do with Typeable. One possibility would be to call the module Data.Proxy and then conditionally not export Data.Proxy from "tagged" with a recent base. Right now tagged's Data.Proxy exports a bunch of instances (Eq, Ord, Show, Read, Typeable, Data, Enum, Ix, Bounded, Functor, Applicative, Monoid, Monad, Foldable, Traversable) and four functions (asProxyTypeOf, reproxy, proxy, unproxy). Being in a separate module, all the instances could be added pretty easily. "proxy" and "unproxy" mention Tagged, so they can reasonably be moved into Data.Tagged. The other two -- asProxyTypeOf :: a -> Proxy a -> a; reproxy :: Proxy a -> Proxy b -- look like reasonable Proxy functions that could go into base (maybe one or both of them could even be made proxy-polymorphic). Alternatively, any other module could define a Proxy type with all the relevant instances (pushing some instances out to the classes' modules as mentioned) and then tagged's Data.Proxy could re-export it and define all the helper functions. That module could be Data.Typeable but I don't think it belongs there (but it doesn't matter that much). At any rate I agree that if this moves into base, it shouldn't lose any functionality (non-orphan instances are functionality), and that a duplicate Proxy is worse than not having one in base at all. After all, base doesn't need to *use* it. Shachaf

Ben Gamari writes:

Here[1] is my attempt at moving Proxy to its own module and giving it a reasonably complete set of instances (blatantly stolen from tagged). Comments welcome, particularly if you can spot any avoidable portability issues as my experience here is pretty limited.

[1] https://github.com/bgamari/packages-base/tree/proxy

Is there any objection to this going in? From what I can tell, this is the best solution we are going to find. Cheers, - Ben

Simon Peyton-Jones writes:

I believe that Richard Eisenberg and Pedro Magalhaes are going to make a concrete proposal. Maybe it's identical to yours. Pedro, Richard?

Pedro and Richard, Any news on a proposal? I think we all agree that this should be considered a blocker for the 7.8 release. Cheers, - ben

Richard Eisenberg writes:

Hi Ben,

Oops. I had updated this page [http://hackage.haskell.org/trac/ghc/wiki/TypeLevelReasoning] with details but forgot to advertise. Pedro and I are scheduled to discuss next week, and I do hope that this get implemented/committed before April is out.

Great! Thanks for the update. Cheers, - Ben

* Shachaf Ben-Kiki [2013-04-18 23:43:41-0700]

On Thu, Apr 18, 2013 at 11:56 AM, Richard Eisenberg wrote:

...

Hi Ben,

Oops. I had updated this page [http://hackage.haskell.org/trac/ghc/wiki/TypeLevelReasoning] with details but forgot to advertise. Pedro and I are scheduled to discuss next week, and I do hope that this get implemented/committed before April is out.

Richard

There's another possible approach to the Proxy mess: Instead of using or mentioning Proxy anywhere in the Typeable API, make Maybe the "official" way to use typeRep.

The argument is something like: You want to get a TypeRep of a type, but you may or may not have a value of that type. If you do, you pass Just x. If you don't, you pass Nothing, annotated to the appropriate type. A situation where you may or may not have a value is exactly what Maybe is for, so it's not a hack. :-)

This is better than the Proxy approach because it lets typeRep have the functionality of typeOf -- typeOf x = typeRep (Just x) -- which it doesn't with plain Proxy. It's also better because Maybe is a Prelude type suited to the purpose which everybody already knows.

(Of course typeRep can keep the polymorphic type, which would make it Proxy-compatible. But we don't need to put Proxy in base, or re-export it from Data.Typeable, or even mention it in the documentation.)

I don't think it's possible. Proxy has to be kind-polymorphic, so that we can apply it to type constructors, constraints etc. But Maybe can't be kind-polymorphic, because it has a field of type 'a'. Thus, the kind of 'a' is forced to be *. Another problem with this approach is that it's not self-documenting. You have to say specifically that this argument is just a proxy and the semantics will be the same regardless of what you pass. But it was an interesting idea nevertheless. Roman

* Shachaf Ben-Kiki [2013-04-19 00:06:10-0700]

Bah, I hadn't thought of kind polymorphism. That's a problem -- though is it a problem for any use of Typeable in base?

Yes — the plan is to make Typeable itself kind-polymorphic (instead of Typeable1, Typeable2, ...). For that you need a kind-polymorphic proxy.

For the second point, at least the type of typeRep would be pretty self-documenting, because it would be polymorphic in the "proxy" type, not mention Maybe explicitly. Maybe you mean that use sites perhaps wouldn't be? The situation wouldn't really be different from how typeOf is used currently. But maybe that's not a good benchmark. Oh well.

I was referring to user-written functions which disambugate the types by taking proxies as arguments. They may take several arguments, and it may not be obvious that some of them are just proxies. So even if Maybe would be a good fit for typeOf, it's a poor substitute for Proxy in general. (But I see now that you were only concerned with base.) Roman