Two examples, one where Proxy is necessary, and one where Proxy doesn’t fundamentally change the types, but I tend to use it anyway.
Proxy necessary
Proxy or some equivalent trick is necessary when there’s some intermediate type, not exposed in the normal type signature, that you want the consumer to be able to specify. Perhaps the intermediate type changes the semantics, such as read . show :: String -> String. With ScopedTypeVariables enabled, I’d write
f :: forall proxy a. (Read a, Show a) => proxy a -> String -> String
f _ = (show :: a -> String) . read
> f (Proxy :: Proxy Int) "3"
"3"
> f (Proxy :: Proxy Bool) "3"
"*** Exception: Prelude.read: no parse
The proxy parameter allows me to expose a as a type parameter. show . read is kind of a stupid example. A better situation may be where some algorithm uses a generic collection internally, where the collection type selected has some performance characteristics that you want to the consumer to be able to control without requiring (or permitting) them to provide or receive the intermediate value.
Something like this, using fgl types, where we don’t want to expose the internal Data type. (Perhaps someone can suggest an appropriate algorithm for this example?)
f :: Input -> Output
f = g . h
where
h :: Gr graph Data => Input -> graph Data
g :: Gr graph Data => graph Data -> Output
Exposing a proxy argument would allow the user to select between a Patricia tree or a normal tree graph implementation.
Proxy as API or implementation convenience
I sometimes use Proxy as a tool to choose a typeclass instance, especially in recursive or inductive class instances. Consider the MightBeA class I wrote in this answer about using nested Eithers:
class MightBeA t a where
isA :: proxy t -> a -> Maybe t
fromA :: t -> a
instance MightBeA t t where
isA _ = Just
fromA = id
instance MightBeA t (Either t b) where
isA _ (Left i) = Just i
isA _ _ = Nothing
fromA = Left
instance MightBeA t b => MightBeA t (Either a b) where
isA p (Right xs) = isA p xs
isA _ _ = Nothing
fromA = Right . fromA
The idea is to extract a Maybe Int from, say, Either String (Either Bool Int). The type of isA is basically a -> Maybe t. There are two reasons to use a proxy here:
First, it eliminates type signatures for the consumer. You can call isA as isA (Proxy :: Proxy Int) rather than isA :: MightBeA Int a => a -> Maybe Int.
Second, it’s easier for me to think through the inductive case by just passing the proxy through. With ScopedTypeVariables, the class can be rewritten without a proxy argument; the inductive case would be implemented as
instance MightBeA' t b => MightBeA' t (Either a b) where
-- no proxy argument
isA' (Right xs) = (isA' :: b -> Maybe t) xs
isA' _ = Nothing
fromA' = Right . fromA'
This isn’t really a big change in this case; if the type signature of isA was considerably more complex, using the proxy would be a big improvement.
When the use is exclusively for implementation convenience, I’d typically export a wrapper function so the user needn’t provide the proxy.
Proxy vs. Tagged
In all of my examples, the type parameter a doesn’t add anything useful to the output type itself. (In the first two examples, it’s unrelated to the output type; in the last example, it’s redundant of the output type.) If I returned a Tagged a x, the consumer would invariably untag it immediately. Furthermore, the user will have to write out the type of x in full, which is sometimes very inconvenient because it’s some complicated intermediate type. (Maybe someday we’ll be able to use _ in type signatures…)
(I’m interested to hear other answers on this sub-question; I’ve literally never written anything using Tagged (without rewriting it in short order using Proxy) and wonder whether I’m missing something.)