What is the purpose of `Data.Proxy`?

by

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.

Leave a Comment

tech