Remove Proxy's

[Icelandjack]

Will the Proxy arguments be removed given visible type application in GHC 8

[phadej]

Please no. TypeApplication is very experimental extension, and even if it wasn't so; the GHC 7.8 or GHC 7.10 support is important for some of us.

[kosmikus]

I agree with @phadej. They might ultimately get removed if visible type application is stable and around for a few releases, but right now is far too early to do so. What might be possible is to additionally offer proxy-less variants of the functions that currently need proxies for GHC >= 8.

[phadej]

proxy-less variants would be good start, in best case we can "hide" proxies from user facing api, and verify that TypeApplications add value there.

I might be interested myself to experiment with that, after 0.5 is out.

EDIT I'm afraid that we just trade Proxy :: Proxy Foo to @Foo - yet that's something already.

[pavelkogan]

If Proxy were to be replaced with a type variable (i.e. servant functions took proxy a instead of Proxy a) then clients of the library could choose to use either Proxy :: Proxy Foo or id @Foo (or even (:: Foo) when type sections are implemented).

[jkarni]

@pavelkogan interesting idea

[jkarni]

What do we all think about Proxy a => proxy a?

[soenkehahn]

Can someone explain the exact advantages of proxy a, please? (Or point to a website doing so?) I feel I'm missing something here...

[phadej]

forall proxy (k -> TYPE levity). proxy a cannot be inspected, which theoretically is nice. I'm not sure though if GHC can (and if yes, then do) treat it as Proxy# a i.e. as argument has no representation (in 7.10 or 8.0).

Prelude GHC.Prim> :k Proxy# 
Proxy# :: k -> TYPE 'GHC.Types.VoidRep

The type constructor Proxy# is used to bear witness to some type variable. It's used when you want to pass around proxy values for doing things like modelling type applications. A Proxy# is not only unboxed, it also has a polymorphic kind, and has no runtime representation, being totally free.

[dredozubov]

@jkarni frankly, i don't really see the point in this change. What have you had in mind?

[kosmikus]

I'm ok with it. It's more or less a standard technique, and grants users extra flexibility. The only disadvantage I see is that to people unfamiliar with proxies, it is ever so slightly more difficult to explain.

[dredozubov]

@kosmikus Can you elaborate on flexibility a bit? Afaik this would only be useful if we can use more polymorphic proxy, but it's already kind-polymorphic in base. Am i missing some compatibility nuances or something else?

[soenkehahn]

I'm a bit worried that proxy might make type error messages worse. For example, if you mistakenly swap the arguments to serve I would assume that you will get worse error messages. I might be wrong, of course, but I think we should try this out before considering to switch.

[kosmikus]

@dredozubov The flexibility is that you can use any type constructor you like as a proxy, so if you are e.g. in a context where you have a Maybe Foo already lying around, you can simply pass that value and avoid the lengthy Proxy :: Proxy Foo construction.

[soenkehahn]

@kosmikus: When I ran into that situation, I wrote toProxy :: f a -> Proxy a. Using that is slightly shorter than Proxy :: Proxy Foo, yet I felt it more explicitly expressed, what was going on.

[kosmikus]

@soenkehahn Yes, I agree that everything is of course equally expressive, and the tradeoffs are rather minor.

[jkarni]

I guess no one feels strongly either way here, so closing.

EDIT - I meant feels strongly about proxy vs Proxy. The consensus seems to be against removing proxy altogether