Haskell: Why use Proxy?

Question

In Haskell, a Proxy is a type witness value that makes it easy to pass some types around

data Proxy a = Proxy

An example use is here in json-schema:

class JSONSchema a where
  schema :: Proxy a -> Schema

so you could do schema (Proxy :: Proxy (Int,Char)) to obtain what the JSON representation for an Int-Char-Tuple would be (probably an array).

---

Why do people use proxies? It seems to me that the same could be accomplished by

class JSONSchema a where
  schema :: Schema a

similar to how the Bounded typeclass works. I first thought it might be easier to get the schema of some given value when using proxies, but that doesn't seem to be true:

{-# LANGUAGE ScopedTypeVariables #-}

schemaOf :: JSONSchema a => a -> Schema a

schemaOf (v :: x) = schema (Proxy :: Proxy x)  -- With proxy

schemaOf (v :: x) = schema :: Schema x         -- With `:: a`
schemaOf _ = schema                            -- Even simpler with `:: a`

Also, one might worry about whether the Proxy values are actually eradicated at runtime, which is an optimisation problem that doesn't exists when using the :: a approach.

If the :: a approach as taken by Bounded achieves the same result with shorter code and less worries about optimisation, why do people use proxies? What are the benefits of proxies?

---

EDIT: Some answers and commenters rightfully pointed out that the :: a approach taints the data Schema = ... type with a "useless" type parameter - at least from the perspective of the plain data structure itself, which doesn't ever use the a (see here).

The suggestion is to use the phantom type Tagged s b instead, which allows to separate the two concerns (Tagged a Schema combines the non-parametric schema type with a type variable a), which is strictly better than the :: a approach.

So my the question should better be What are the benefits of proxies vs. the tagged approach?

Answer 1

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.)

Answer 2

Ultimately they will perform the same functionality and you see them in either style. Sometimes it's appropriate to phantom tag your values, sometimes you'd like to think of them as untyped.

The other alternative is to use Data.Tagged.

class JSONSchema a where
  schema :: Tagged a Schema

Here we have something of the best of both worlds since a Tagged Schema has phantom type information necessary to resolve the instance but we can trivially disregard that information using unTagged :: Tagged s b -> b.

I would say the driving question, couched in terms of this example, should be "Do I want to consider typed operations on Schemas?". If the answer is "no", then you will be biased toward the Proxy or Tagged approaches. If the answer is "yes", then Schema a is a great solution.

As a final note, you can use the Proxy approach (somewhat hackily) without any imports. You see this sometimes in the style

class JSONSchema a where
  schema :: proxy a -> Schema

Now that Proxy has become a suggestively named type variable only we can do something like the following

foo :: Schema
foo = schema ([] :: [X])

and never have to import Proxy at all. I personally think this is a complete hack job though which probably will end up confusing readers.