Posted on January 15, 2017 by Kwang Yul Seo
Tags: Proxy

Proxy is a mysterious type residing in Data.Proxy module. The definition of Proxy tells nothing about its nature.

-- | A concrete, poly-kinded proxy type
data Proxy t = Proxy

The documentation of Proxy says two hints. It is a (1) concrete and (2) poly-kinded proxy type.


The kind of Proxy is forall k. k -> *.

λ> :k Proxy
Proxy :: k -> *

Here k is poly-kinded so we can pass types of any kind to Proxy.

Concrete value

In Haskell, we can create a value of any type we want by annotating undefined with the type.

λ> let p = undefined :: Int

However, we can’t use this trick if the kind of the type is not *, For example, we can’t annotate undefined with type (,) because its kind is * -> * -> *.

λ> let q = undefined :: (,)

<interactive>:4:22: error:
    • Expecting two more arguments to ‘(,)’
      Expected a type, but ‘(,)’ has kind ‘* -> * -> *’
    • In an expression type signature: (,)
      In the expression: undefined :: (,)
      In an equation for ‘q’: q = undefined :: (,)

Proxy lets us to overcome this limitation. We can create a proxy value representing the type by annotating Proxy data constructor.

λ> import Data.Proxy
λ> let p = Proxy :: Proxy (,)
λ> :t p
p :: Proxy (,)

We can think of Proxy :: Proxy (,) as a reified value of the type (,).

Type Application

The read/show problem below is ill-typed because of ambiguity.

f :: String -> String
f s = show (read s)

We can fix this issue by explicitly passing the type as a value argument. As you can see the wild card pattern _, the value is not used anywhere in the definition of f. Only its type is used.

f :: forall proxy a. (Read a, Show a) => proxy a -> String -> String
f _ = (show :: a -> String) . read
λ> f (Proxy :: Proxy Int) "3"

As a side note, TypeApplications extension introduced in GHC 8 provides an alternative way to fix this.


Another application of Proxy is Typeable. Before kind polymorphism was introduced in GHC, there was a lot of code duplication in the way Typeable is implemented because t can represent only a specific kind.

class Typeable (t :: *) where
  typeOf :: t -> TypeRep

class Typeable1 (t :: * -> *) where
  typeOf1 :: t a -> TypeRep

class Typeable2 (t :: * -> * -> *) where
  typeOf2 :: t a b -> TypeRep

Proxy allows us to merge all these classes into one:

class Typeable t where
  typeOf :: Proxy t -> TypeRep

instance Typeable Int  where typeOf _ = TypeRep
instance Typeable []   where typeOf _ = TypeRep

Other use cases of Proxy

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