Abstract Types, Parametric Polymorphism, And Dependency Injection And Mock Testing

Parametric polymorphic functions have very uniform behaviour, “works the same way for all types”; a few test cases with a few concrete types can tell you a lot about the general case. For example, the following conversation is possible:

A: I have implemented f :: a -> [a]
B: Don’t show me the code! But show me what f () happens to be.
A: It’s [(), (), ()].
B: Then I also know: f 4 is [4, 4, 4].

This comes from an important theorem that’s pretty daunting to state. Fortunately, it is closely related to a theorem about programming with abstract types. I think that the abstract type story is more relatable, so I will start with it, and then we can transition to the parametric polymorphism story.

But here is how the two are connected. Suppose there is a module ZS that exports these items:

abstract type A
z :: A
s :: A -> A

then this program that uses ZS

import ZS(A, z, s)

duo :: A
duo = s (s z)

is very much like this polymorphic function

polyduo :: a -> (a -> a) -> a
polyduo z s = s (s z)

Hopefully you are also thrilled to see:

• If you rewrite duo to polyduo, that’s dependency injection.

• If you test either by giving it a mock version of (A, z, s), that’s mock testing.

  Emphatically, you use the test result to predict what will happen under a production version of (A, z, s), which brings us back to parametric polymorphism!

Beautifully we have a nice little piece of 1980s programming language theory that explains and unifies multiple programming practices.

Programming with Abstract Types

An abstract type can have many possible implementations. A program that uses the abstract type is given one such underlying implementation, and then later someone may switch to another. So there is a correctness question to ask, and it takes one of these forms:

• Do the two implementations “behave the same”, and in what sense? How to make this precise?

• Does the program “behave the same as before” after switching? What is a strategy for answering this?

I will walk through the strategy with an example of an abstract type of sets of Ints:

abstract type IntSet
emptyset :: IntSet
isEmpty :: IntSet -> Bool
insert :: Int -> IntSet -> IntSet
lookup :: Int -> IntSet -> Bool

I have a list implementation and a binary search tree implementation. In each one, I change the names to have suffixes (in code) or subscripts (in sentences) to help me to refer them later:

• List version pseudocode:

  Suffix “_L” or subscript _L, e.g., IntSet_L or IntSet_L.

  IntSet_L = [Int]
  emptyset_L = []
  isEmpty_L = \s -> null s
  insert_L = \i s -> if lookup_L i s
                     then s
                     else i : s
  lookup_L = the usual linear search
  
  -- Note: No element occurs more than once.  This becomes a validity condition,
  -- aka data invariant.

• BST version pseudocode:

  Suffix “_B” or subscript _B, e.g., IntSet_B or IntSet_B.

  data IntBST = Empty | Node Int IntBST IntBST
  IntSet_B = IntBST
  emptyset_B = Empty
  isEmpty_B = \t -> case t of Empty -> True
                              _     -> False
  insert_B = the usual BST insert
  lookup_B = the usual BST lookup
  
  -- Note: Elements are in BST order.  This becomes a validity condition,
  -- aka data invariant.

  Notation: I write a tree in this format:

  • Non-empty tree: (left-subtree root-key right-subtree)
  • Empty tree: empty string

  Example: 2 at root, 1 on left: ((1)2)

  Example: 1 at root, 2 on right: (1(2))

  Actually you just need to know those two examples. :)

How to make precise “they behave the same” starts from this idea:

We have the insight that, e.g., [1,2] is a valid list representation, (1(2)) is a valid tree representation, and they represent the same set. Perhaps we can design a relation/correspondence, call it “~”, between lists and trees so that “xs ~ t” means that xs and t are respective valid representations of the same set.

So I define: xs ~ t iff

• valid list: elements in xs occur only once
• valid tree: elements in t are in BST order
• correspondence: both store the same elements

Examples:

• [1,2] ~ (1(2))
• [1,2] ~ ((1)2)
• [2,1] ~ (1(2))
• [2,1] ~ ((1)2)

Negative examples:

• [1,2,1] ~ (1(2)) is false, invalid list
• [1,2] ~ (2(1)) is false, invalid tree
• [1,2,3] ~ (1(2)) is false, discrepancy in elements

Then the following are true, and they are the precise meaning of “the two implementations behave the same”, or sometimes I also say “the two implementations are in correspondence”.

• emptyset_L ~ emptyset_B
• if xs ~ t, then isEmpty_L xs = isEmpty_B t
• if xs ~ t, then insert_L i xs ~ insert_B i t
• if xs ~ t, then lookup_L i xs = lookup_B i t

Generally, the correspondence uses “~” between the two representation of IntSet values (lists vs trees), “=” between Int values, “=” again between Bool values, and extends this to functions by “if inputs correspond, then outputs correspond”.

Now we can talk about programs that uses IntSet. Here is an example program:

use :: Int -> Int -> Bool
use i j = let
    s0 = emptyset
    s1 = insert i s0
    s2 = insert j s1
  in lookup i s2

Does it give the same answer whether you use IntSet_L or IntSet_B? Yes. Let me clone the code and add suffixes to help explain:

use_L :: Int -> Int -> Bool
use_L i j = let
    s0_L = emptyset_L
    s1_L = insert_L i s0_L
    s2_L = insert_L j s1_L
  in lookup_L i s2_L

use_B :: Int -> Int -> Bool
use_B i j = let
    s0_B = emptyset_B
    s1_B = insert_B i s0_B
    s2_B = insert_B j s1_B
  in lookup_B i s2_B

Step through both versions to check:

• Suppose I give both sides the same i and the same j
• s0_L ~ s0_B
• Therefore, s1_L ~ s1_B
• Therefore, s2_L ~ s2_B
• Therefore, lookup_L i s2_L = lookup_B i s2_B

This works for every program that uses IntSet. (And every program that doesn’t, for that matter.)

Zooming back out, this is what you do when you have two implementations for an abstract type. First fulfill this prerequisite:

• There are two representations; so think up a good relation between the two. (How good is good enough? You just need to make the next point work.)

• For each operation, you have two implementations; so verify that the two are “in correspondence”, under the relation you thought up.

Then you can conclude:

• For every program p: p under the 1st implementation and p under the 2nd implementation are “in correspondence”.

(Similarly if you have multiple abstract types.)

The type abstraction theorem is a general and precise way to state the above.

The Type Abstraction Theorem

The type abstraction theorem is daunting to state because it takes some setting up to make “in correspondence” precise and cover all cases. The particular challenges are: Sometimes it means “=”, some other times it means my (or your) custom “~” relation; and we ambitiously extend it to function types, e.g., IntSet → Bool.

We have two implementations of IntSet; let me call one of them “left side” and “on the left”, the other “right side” and “on the right”. Here is the ultimate purpose of the definitions. For arbitrary type expression T:

• “Dom_L(T)” means what T becomes on the left. Example: Dom_L(IntSet→Bool) = [Int]→Bool.

  “Dom_L” is short for “domain on the left”.

• “Dom_R(T)” means what T becomes on the right. Example: Dom_R(IntSet→Bool) = IntBST→Bool.

  “Dom_R” is short for “domain on the right”.

• “⟨T⟩” means the appropriate correspondence for T. Examples: ⟨Int⟩ is equality, ⟨IntSet⟩ is my “~”.

  I designed the notation to be usable infix, e.g., 4⟨Int⟩4 means 4=4 and is true, 4⟨Int⟩5 means 4=5 and is false.

  As for function types, we want “isEmpty_L ⟨IntSet→Bool⟩ isEmpty_B” to be a thing and be true, for example. This is the hard part, but I think I have primed you for it.

  It is true that ⟨T⟩ is a relation between Dom_L(T) on the left and Dom_R(T) on the right.

These can be achieved by structural recursion on type expressions. (I think you can already guess how to do Dom_L and Dom_R.)

Dom_L and Dom_R are defined by:

⟨T⟩ is defined by:

For ⟨T→U⟩, here is the motivation. Recall that, for example, isEmpty_L and isEmpty_B are in correspondence in the sense that “if inputs are in correspondence, then outputs are in correspondence”; formally:

if xs ~ t, then isEmpty_L xs = isEmpty_B t

I would very much like to make that the exact meaning of “isEmpty_L ⟨IntSet→Bool⟩ isEmpty_B”. In longer form, I want:

And observe that I can use Dom_L, Dom_R, ⟨IntSet⟩, and ⟨Bool⟩ to make it generalizable:

The general form goes as:

With that, the following are true of the two implementations:

• emptyset_L ⟨IntSet⟩ emptyset_B
• isEmpty_L ⟨IntSet→Bool⟩ isEmpty_B
• insert_L ⟨Int→IntSet→IntSet⟩ insert_B
• lookup_L ⟨Int→IntSet→Bool⟩ lookup_B

That allows us to deduce: use_L ⟨Int→Int→Bool⟩ use_B. Generally, if program p has type T, then (p under list impl) ⟨T⟩ (p under tree impl).

The same reasoning applies to other abstract types and programs. This framework is summarized as the abstraction theorem (for less clutter, I state it for just one abstract type and one operation):

If:

• A is an abstract type
• op :: U is an operation of type U
• left side implementation: Dom_L(A) = A_L, op is implemented by op_L :: Dom_L(U)
• right side implementation: Dom_R(A) = A_R, op is implemented by op_R :: Dom_R(U)
• ~ is a relation between A_L and A_R
• let ⟨A⟩ = “~” in the following
• op_L ⟨U⟩ op_R

then:

• for all type T, for all program p::T : (p under the left side) ⟨T⟩ (p under the right side)

(Similarly if you have more operations and multiple abstract types.)

The Parametricity Theorem

I now transition from programming with abstract types to parametric polymorphic functions. For less clutter, allow me to switch to a shorter toy example:

import ZS(A, z, s)
-- abstract type A
-- z :: A
-- s :: A -> A

duo :: A
duo = s (s z)

The type abstraction theorem applied to this says:

If:

• A is an abstract type
• the operations are z::A, s::A→A
• left side: Dom_L(A) = A_L, z_L::A_L, s_L::A_L→A_L
• right side: Dom_R(A) = A_R, z_R::A_R, s_R::A_R→A_R
• ~ is a relation between A_L and A_R
• let ⟨A⟩ = “~” in the following
• z_L⟨A⟩z_R and s_L⟨A→A⟩s_R

then:

• (duo under the left side) ⟨A⟩ (duo under the right side)

Let me rewrite that to this form:

If you apply some kind of dependency injection, my toy program can be converted to this parametric polymorphic function:

polyduo :: ∀a . a -> (a -> a) -> a
polyduo z s = s (s z)

Then “(duo under A_L, z_L, s_L)” is converted to “polyduo z_L s_L”. Where has A_L gone? It is hidden under the act of “instantiate ‘a’ to A_L”. Some people explicate it with the subscript notation “polyduo_AL”. I will write like that for a while, but eventually omit it. Similarly for “(duo under A_R, z_R, s_R)”.

And the type abstraction theorem can be converted accordingly:

Note that the final “if-then” part is “if inputs to polyduo correspond, then outputs to polyduo correspond”, i.e., the definition of ⟨a → (a → a) → a⟩. So we can simplify:

I want that to be the meaning of “polyduo ⟨∀a . a → (a → a) → a⟩ polyduo”, extending the definition of ⟨T⟩ to polymorphic types. This motivates the general form:

With that definition, this is true of polyduo:

polyduo ⟨∀a . a → (a → a) → a⟩ polyduo

The parametricity theorem states this in general:

For all type T in which all type variables are ∀-quantified (“T is a closed type”), for all term e::T : e⟨T⟩e.

This theorem looks very anti-climatic. But recall that there is a lot of content in how ⟨∀a. T⟩ and ⟨T→U⟩ are defined, and how ⟨a⟩ can harbour an interesting relation for a type variable (or abstract type).

This theorem is behind how we can use a few test cases on a polymorphic function to discover fairly general behaviour.

Worked Examples

Example: ∀a. a→(a→a)→a

Suppose e :: ∀a . a → (a → a) → a . The parametricity theorem expands to:

I will test “e 0 succ”, where succ is defined by: succ n = n+1. This amounts to specializing the left side to: A_L=Integer, z_L=0, s_L=succ. I will leave the right side arbitrary, so as to draw general conclusions about “e z_R s_R”.

The relation I design for ~ or ⟨a⟩ is harder, but here are my design considerations:

• I want “0 ⟨a⟩ z_R” and “succ ⟨a→a⟩ s_R” to be true, so that I can conclude that “e 0 succ ⟨a⟩ e z_R s_R” is also true.

• “succ ⟨a→a⟩ s_R” expands to:

  for all n_L::Integer, n_R::A_R :
      if n_L ~ n_R, then succ n_L ~ s_R n_R

  That really looks like what you would do in an inductive definition. And “0 ~ z_R” really looks like a base case, too.

• I want a minimal relation, so that “e 0 succ ⟨a⟩ e z_R s_R” is helpful.

  Here is an exaggerated example of how a non-minimal relation is unhelpful. If I defined x~y to be true for all x::Integer and y::A_R, the conclusion “e 0 succ ⟨a⟩ e z_R s_R” would be also trivially true without telling me anything.

  So I want x~y to be true for enough pairs of x and y, but false for others.

  This point and the previous point together really say I want an inductive definition.

So I define ~ inductively (a.k.a. “the smallest relation such that” and “if x~y then it has to come from using these clauses a finite number of times”):

• 0 ~ z_R
• if n_L ~ n_R, then succ n_L ~ s_R n_R

It works as a partial function from the left to the right: it maps 0 to z_R, 1 to s_R z_R, 2 to s_R (s_R z_R), etc.; and it doesn’t map negative integers to anything. More importantly, if later we find that 2 ~ foo for example, then we know foo = s_R (s_R z_R), there is no other choice.

Then we get:

Suppose testing dicovers e 0 succ = 2. Then e z_R s_R = s_R (s_R z_R), and this works for all A_R, z_R, and s_R.

Moreover, for every f :: ∀a . a → (a → a) → a that terminates (in more detail: f z s terminates if z and s terminate):

• f 0 succ has to terminate and give me some integer i
• i ~ f z_R s_R
• i≥0 because ~ doesn’t allow negative integers on the left
• f z_R s_R = s_R (… (s_R z_R)…), “start with z_R and apply s_R i times”

So we have basically characterized all functions of type ∀a . a → (a → a) → a under suitable assumptions about termination.

Example: ∀a. a → [a]

Suppose trio :: ∀a. a → [a] . Then the parametricity theorem expands to:

I haven’t told you what to do with ⟨[T]⟩, but here it is: Define inductively (again “smalllest relation” etc.):

• [] ⟨[T]⟩ []
• if x⟨T⟩y and xt⟨[T]⟩yt, then (x:xt)⟨[T]⟩(y:yt)

You can understand it as: the two lists have the same length, and the respective elements are related by ⟨T⟩. But I show you the inductive definition because it generalizes to all algebraic data types. (But if you generalize “have the same length” to “have the same shape”, that’s the right idea.)

It also turns out that in this and similar examples, you design the element-wise relation ⟨T⟩ to work like a function for simplicity. So suppose you have a function h, and x⟨T⟩y iff h x = y. Then xs⟨[T]⟩ys says:

• xs and ys have the same shape (length)
• for each element x in xs, the corresponding element in ys is h x
• Summary: fmap h xs = ys

This generalizes: For F an instance of Functor, xs⟨F T⟩ys iff fmap h xs = ys.

Going back to trio :: ∀a. a → [a], and using a function for ⟨a⟩:

I use the test case “trio ()”, so I’m specializing to: A_L=(), x_L=(), h () = x_R.

Suppose the test result is trio () = [(), (), ()]. Now I know:

trio x_R = fmap h (trio ()) = fmap h [(), (), ()] = [x_R, x_R, x_R]

Example: ∀a,b. (a,b) → a

The standard library function fst :: (a,b) -> a extracts the 1st field from the pair. Conversely, we find it intuitive that another function of that type has to do the same thing (or else hangs). This is justified by the parametricity theorem too.

Suppose f :: ∀a,b. (a,b) → a . You can think of that type as nesting ∀’s: ∀a. ∀b. (a,b) → a . Expanding the parametricity theorem, and using functions for relations:

I haven’t said what to do with ⟨(a,b)⟩, but it’s easily guessable:

(xl,yl) ⟨(T,U)⟩ (xr,yr) iff: xl⟨T⟩xr and yl⟨U⟩yr

Using that, and expanding “for all p_L::(A_L,B_L)” to “for all xl::A_L, yl::B_L”, similarly for p_R:

I now specialize: A_L=A_R, B_L=B_R, xl=xr, yl=yr, h x = xr (for all x), k y = yr (for all y). Idea: Force h (f (xl,yl)) = xr.

There!

Parametric vs Ad Hoc

The two names “parametric polymorphism” and “ad hoc polymorphism” were coined by Strachey for the difference in:

• Parametric: A polymorphic program behaves the same way for all types.

• Ad hoc: A polymorphic program has unrelated meanings for different types.

The parametricity theorem is the outcome of Reynolds working out a mathematical definition. It was also his idea to start with the abstract type story.

Ad hoc polymorphism allows a program of type ∀a.T to do “if ‘a’ is Int, do something special”. This breaks the parametricity theorem.

Likewise, if a user of IntSet can do “if IntSet is a list, do something special”, this doesn’t treat IntSet as an abstract type, so it breaks the type abstraction theorem.

The kind of polymorphism provided by OO languages leans on the ad hoc side, e.g., two subclasses can implement a method in arbitrarily unrelated ways, and so the knowledge that they belong to the same superclass isn’t very informative.

In a principles of languages course, I’m obliged to fearmonger you with: If a language allows this, then someone will do it, and you have a much harder time reasoning about programs.

Outside, in fairness, programmers don’t set out to troll each other. You would implement the two subclasses in conceptually related ways, even though the precise relation is difficult to formalize. In this sense, programmers stay close to the spirit of parametric polymorphism, even in a language of ad hoc polymorphism. Still, this is open to one more kind of bugs, so watch out.