What is "proxy a" in printtype function?

Question

When I try to use printtype function from Type.Showtype. I find that the type signature of printtype is:

printtype :: Showtype a => proxy a -> IO ()

The confusing thing here is the type of proxy a, it seems come from Data.Proxy, but I can't find any definition of proxy, it is obvious that is different to Proxy, because first letter of proxy is lower case. And I knew the first letter of data type cannot be lower case in Haskell, so proxy a is not a type, but why does it can appear in the type signature?

Answer 1

In general a proxy for a type a is some data type Proxy a whose values carries no information. So the value is passed around to as a witness for its type (for type inference / type checking purposes). In that case proxy is isn't a specific data type, but a type variable with kind * -> *. Meaning you can use whatever you want as a proxy, but the idea remains the same.

The function is,

printtype :: Showtype a => proxy a -> IO ()

and it is supposed to "print a type", but functions are applied to values not types. So rather than passing an actual an argument of type a you pass an argument of some type proxy a, whose actual value is irrelevant (and usually will be a data type Proxy that contains no information).

Look at the instance for a simple type, e.g. pairs,

instance (Showtype a, Showtype b) => Showtype '(a,b) where
  showtype _ = showtuple' [
    showtype (Proxy :: Proxy a),
    showtype (Proxy :: Proxy b)]

First note how showtype ignores its argument,

showtype _ = ...

the value of the proxy is irrelevant, what matters is that we are printing the type (a,b). Then we have a call to showtuple', which is used to print types tuples (of any length) given a list with the printing of the types of each component. For each component we have,

showtype (Proxy :: Proxy a)
showtype (Proxy :: Proxy b)

the selected proxy here is the data type Proxy which holds no information. In one case it is of type Proxy a and in the other Proxy b. The function showtype is defined so that you could also call it with e.g.

showtype ([] :: [a])
showtype ([] :: [b])

Not that if you were passing around a rather than proxy a, here the only value you'd be able to construct (for a generic a) would be undefined. Should its evaluation ever be forced it would break your program.