What is the purpose of `Data.Proxy`?

Question

Proxy from Data.Proxy seems to be nothing more than a mere

data Proxy s

When do I need such an uninhabited type or rather, what does it enable I couldn't do otherwise, when does it simplify things compared to other approaches, and how is it used in practice?

Answer 1

I frequently use Proxy with its partner in crime Data.Tagged, as the documentation indicates, to avoid unsafely passing dummy arguments.

For example,

data Q  class Modulus a where   value :: Tagged a Int  instance Modulus Q where   value = Tagged 5  f x y = (x+y) `mod` (proxy value (Proxy::Proxy Q)) 

An alternative way to write that without Tagged is

data Q  class Modulus a where   value :: Proxy a -> Int  instance Modulus Q where   value _ = 5  f x y = (x+y) `mod` (value (Proxy::Proxy Q)) 

In both examples, we could also remove the Proxy type and just use an undefined :: Q to pass in the phantom type. However, using undefined is generally frowned upon because of the problems that can ensue if that value is ever evaluated. Consider the following:

data P = Three        | Default  instance Modulus P where   value Three = 3   value _ = 5  f x y = (x+y) `mod` (value (undefined :: P)) 

which is a valid way to write the instance if I use the Default constructor, the program would crash since I'm trying to evaluate undefined. Thus the Proxy type gives type safety for phantom types.

EDIT

As Carl pointed out, another benefit of Proxy is the ability to have a phantom type of kind other than *. For example, I'm messing around with type lists:

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators,      MultiParamTypeClasses, PolyKinds, FlexibleContexts,      ScopedTypeVariables #-}  import Data.Tagged import Data.Proxy  class Foo (a::[*]) b where   foo:: Tagged a [b]  instance Foo '[] Int where   foo = Tagged []  instance (Foo xs Int) => Foo (x ': xs) Int where   foo = Tagged $ 1 : (proxy foo (Proxy :: Proxy xs)) -- xs has kind [*]  toUnary :: [Int] toUnary = proxy foo (Proxy :: Proxy '[Int, Bool, String, Double, Float]) 

However, since undefined is a value, its type must have kind * or #. If I tried to use undefined in my example, I'd need something like undefined :: '[Int, Bool, String, Double, Float], which results in the compile error:

Kind mis-match     Expected kind `OpenKind',     but '[Int, Bool, String, Double, Float] has kind `[*]' 

For more on kinds, check this out. Given the error message, I expected to be able to write undefined :: Int#, but I still got the error Couldn't match kind # against *, so apparently this is a case of a poor GHC error message, or a simple mistake on my part.