Theorems in PHP for minimal cost

January 29, 2015

Note: This is mostly a port of Parametricity in JavaScript via TypeScript using PHP and Hack.

Thought experiment

Consider the following PHP function:

function foo($x) {
  // implementation hidden
}

What can we infer about this function? The short answer is: almost nothing.

We don't know what type the argument, $x, is expected to be. It could be an integer, a string, an instance of a class, or anything in between.

There's no way to know what sort of data structure this function returns, or whether it returns anything at all.

Essentially, we have no way of knowing anything about what this function does, or how we can use it.

Enter types

Using Hack, let's tweak this function's declaration and see what happens:

function foo<T>(T $x): T {
  // implementation hidden
}

We've made three small changes:

  1. Declare T as a type variable
  2. Declare T as the type of the function's input argument
  3. Declare T as the type of the function's output value

Now let's see what we can infer about this function.

The function takes exactly one argument of any type we like. That type is represented by the type variable T.

The function returns a value, also of type T. Since the function's input and output types share the same type variable T, its return value has the same type as whatever argument was passed in.

If we call foo(42) with the number 42, then T means int, and the function will return an integer.

If we call foo("forty two") with the string forty two, then T means string, and the function will return a string.

The developer writing the implementation can't know anything about what T will be in practice. Is $x a number? Maybe it's a string. Perhaps it's an instance of some class. It can be any of these, and no matter which it is, the function has to return a value of the same type.

The implementation

It turns out that there's only one possible implementation for a function with this type: identity.

If we ignore silly cases like return null; and return $undefined;, the only way to guarantee that we return a value with the same type as the argument is to simply return the argument itself.

function foo<T>(T $x): T {
  return $x;
}

This is a property of parametrically polymorphic functions known as parametricity, and is quite useful for API design, library consumption, and generally reasoning about code.

Parametricity also applies to more complicated (and more interesting) functions, and allows us to derive useful theorems about them using only their type signatures.

Affordable theorems

Say that r is a function of type:

r : ∀X. X* → X*

In Hack, this can be written as:

function r<T>(ImmVector<T> $xs): ImmVector<T> {

Say also that a is a total function of type:

a : A → A'

In Hack, this can be written for A of int and A' of string as:

function a(int $x): string {

From what we learned in Theorems for free!, we know that:

a* ∘ rA = rA' ∘ a*

We can demonstrate this in Hack:

$f = compose(map($x ==> a($x)), $xs ==> r($xs));
$g = compose($xs ==> r($xs), map($x ==> a($x)));

$xs = randVector();
echo '$f($xs) == $g($xs): ' . show(equal($f($xs), $g($xs))) . "\n"; // true