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.

# Poly-kinded

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`

.

`Proxy Char`

where`k`

is`*`

.`Proxy (,)`

where`k`

is`* -> *`

`Proxy Show`

where`k`

is`* -> Constraint`

`Proxy Monad`

where`k`

is`(* -> *) -> Constraint`

# 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"
"3"
```

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

# Typeable

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

- json-schema uses
`Proxy`

to obtain the JSON representation for the given type.

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

- Edward Kmett’s reflection package shows an advanced usage of
`Proxy`

. Austin Seipp’s Reflecting values to types and back explains how to reify arbitrary terms into types that can be reflected back into terms.