What’s a Proxy?

Have you seen something like this in Haskell or PureScript code?

f (Proxy :: Proxy Int)

Have you wondered what the heck is a Proxy and what’s it doing there?

Type inference

In Haskell we can have overloaded functions — i.e. functions whose implementation depends on the types of their arguments or result. The mechanism for achieving the overloading is type classes. Take, for example, the Show type class and its method show:

class Show a where 
    show :: a -> String

There are multiple implementations of it for different a. If I call show True, the compiler knows to reach out for the Show Bool instance and take its implementation, but if I call show 42, the compiler will take the Show Integer implementation, and so on.

Lack of type inference

But sometimes there is no way to tell what the type should be. Take this tricky function for example:

validate s = show (read s)

The purpose of it should be obvious: convert the string to a value, then back to string, thus ensuring that the input string has the right format, while at the same time canonicalizing the representation. So, for example, if the input string was “00042”, the output would be just “42”, removing the insignificant zeroes.

But here’s the problem: which implementations of show and read do we use? There is no way to tell! The compiler could pick Show Bool, or Show Int, or Show String, or anything else - and the program would still typecheck, but the behavior would be unpredictable. So instead of trying to guess, the compiler would just issue an error, saying that type a0 is ambiguous or some such.

Forcing type inference

Ok, so in order to force the compiler to infer the type unambiguously, we need to give it something from which to infer. Since the “something” could really be only parameters or result type, and the result type is already taken, let’s just add an extra parameter that wouldn’t be used in the function body, but would only serve the type inference:

validate :: (Read a, Show a) => a -> String -> String 
validate dummy s = showA dummy (read s) 
    where 
        showA :: x -> x -> String 
        showA _ = show

Now the compiler can look at the signature of showA and see that both its parameters are required to have the same type. Then it can look at the actual first parameter dummy and see that it's of type a, and therefore the second actual parameter read s must also be of type a. From this, the compiler has enough information to select the appropriate implementation of read, and then of show.

Now I can call this function like this:

validate 0 "00042" == "42" 
validate True "False" == "False"   // a bit confusing, isn't it?

Forcing type inference slightly better

But in real life, it’s not always feasible to provide a dummy value. Some values may be too expensive to create, some may be even impossible (when the type in question has a higher kind), it’s not uniform for all types, and finally, sometimes we just don’t know the concrete type at the point where we need this trick.

So how else can we let the compiler know what the type is? Remember that the compiler doesn’t need to have an actual value of the type itself to infer it. It can be some other type that contains the type to be inferred. For example, the compiler can infer the result type of head from the argument type. "If the argument is [Int] - thinks the compiler - then the result must be Int"

Let’s use that:

data Dummy a = Dummy
validate :: (Read a, Show a) => Dummy a -> String -> String 
validate dummy s = showA dummy (read s) 
    where 
        showA :: Dummy x -> x -> String 
        showA _ = show

Notice that Dummy's type parameter isn't actually used in its constructor. All constructors are exactly the same value - it's like unit, but with a type attached to it.

The body of the function almost hasn’t changed, except for an extra Dummy in two places. The type inference still works exactly the same way: infer the type of showA's second parameter from the first, use that to choose the read and show implementations.

Calling such function would require some boilerplate though:

validate (Dummy :: Dummy Int) "00042" == "42" 
validate (Dummy :: Dummy Bool) "False" == "False"

This trick has become a commonplace in Haskell at some point, and thus has been inducted into the standard library, but as Proxy. I'm guessing Dummy had some bad connotations or something…

‘Dummy’ tomato. Photo by Tiago Fioreze.

Language support

In modern Haskell there is better support for doing this sort of thing — the TypeApplications extension. When it is enabled, we can just specify the types straight up with the @ syntax, without any dancing around with dummy values:

validate :: forall a. (Read a, Show a) => String -> String 
validate s = show @a (read s)
validate @Int "00042" == "42" 
validate @Bool "False" == "False"

Side note: the forall a. syntax in the function definition is enabled by the ScopedTypeVariables extension and is required in order to use @a in the body of the function. Without it, the a in the signature and the a in the body would be two different type variables, and the ambiguity will return.

Sadly, this doesn’t apply to PureScript. In PureScript we still have to use the good old Proxy.