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

Albert Y. C. Lai, trebla [at] vex [dot] net

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 IntSetL.

``````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 IntSetB.

``````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”.

• emptysetL ~ emptysetB
• if xs ~ t, then isEmptyL xs = isEmptyB t
• if xs ~ t, then insertL i xs ~ insertB i t
• if xs ~ t, then lookupL i xs = lookupB 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 IntSetL or IntSetB? 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
• s0L ~ s0B
• Therefore, s1L ~ s1B
• Therefore, s2L ~ s2B
• Therefore, lookupL i s2L = lookupB i s2B

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:

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

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

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

“DomR” 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 “isEmptyL ⟨IntSet→Bool⟩ isEmptyB” 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 DomL(T) on the left and DomR(T) on the right.

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

DomL and DomR are defined by:

 DomL(Bool) = Bool DomL(Int) = Int DomL(IntSet) = [Int] DomL(T → U) = DomL(T) → DomL(U) DomR(Bool) = Bool DomR(Int) = Int DomR(IntSet) = IntBST DomR(T → U) = DomR(T) → DomR(U)

⟨T⟩ is defined by:

⟨Bool⟩ = equality for Bool
⟨Int⟩ = equality for Int
⟨IntSet⟩ = my “~”
⟨T→U⟩ = explained in the next few paragraphs

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

if xs ~ `t`, then isEmptyL xs = isEmptyB t

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

isEmptyL ⟨IntSet→Bool⟩ isEmptyB iff:
for all xs::[Int], t::IntBST :
if xs ~ t, then isEmptyL xs = isEmptyB t

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

isEmptyL ⟨IntSet→Bool⟩ isEmptyB iff:
for all xs::DomL(IntSet), t::DomR(IntSet) :
if xs ⟨IntSet⟩ t, then isEmptyL xs ⟨Bool⟩ isEmptyB t

The general form goes as:

fL ⟨T→U⟩ fR iff:
for all xL::DomL(T), xR::DomR(T) :
if xL ⟨T⟩ xR, then fL xL ⟨U⟩ fR xR

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

• emptysetL ⟨IntSet⟩ emptysetB
• isEmptyL ⟨IntSet→Bool⟩ isEmptyB
• insertL ⟨Int→IntSet→IntSet⟩ insertB
• lookupL ⟨Int→IntSet→Bool⟩ lookupB

That allows us to deduce: useL ⟨Int→Int→Bool⟩ useB. 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: DomL(A) = AL, op is implemented by opL :: DomL(U)
• right side implementation: DomR(A) = AR, op is implemented by opR :: DomR(U)
• ~ is a relation between AL and AR
• let ⟨A⟩ = “~” in the following
• opL ⟨U⟩ opR

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: DomL(A) = AL, zL::AL, sL::AL→AL
• right side: DomR(A) = AR, zR::AR, sR::AR→AR
• ~ is a relation between AL and AR
• let ⟨A⟩ = “~” in the following
• zL⟨A⟩zR and sL⟨A→A⟩sR

then:

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

Let me rewrite that to this form:

for all type AL, type AR, relation ~ between AL and AR :
let ⟨A⟩ = “~” in
for all zL::AL, zR::AR, sL::AL→AL, sR::AR→AR :
if zL⟨A⟩zR and sL⟨A→A⟩sR
then (duo under AL,zL,sL) ⟨A⟩ (duo under AR,zR,sR)

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 AL, zL, sL)” is converted to “polyduo zL sL”. Where has AL gone? It is hidden under the act of “instantiate ‘a’ to AL”. Some people explicate it with the subscript notation “polyduoAL”. I will write like that for a while, but eventually omit it. Similarly for “(duo under AR, zR, sR)”.

And the type abstraction theorem can be converted accordingly:

for all type AL, type AR, relation ~ between AL and AR :
let ⟨a⟩ = “~” in
for all zL::AL, zR::AR, sL::AL→AL, sR::AR→AR :
if zL⟨a⟩zR and sL⟨a→a⟩sR
then polyduoAL zL sL ⟨a⟩ polyduoAR zR sR

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:

for all type AL, type AR, relation ~ between AL and AR :
let ⟨a⟩ = “~” in
polyduoAL ⟨a → (a → a) → a⟩ polyduoAR

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:

e1 ⟨∀a. T⟩ e2 iff:
for all type AL, type AR, relation ~ between AL and AR :
let ⟨a⟩ = “~” in
e1AL ⟨T⟩ e2AR

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:

for all type AL, type AR, relation ~ between AL and AR :
let ⟨a⟩ = “~” in
for all zL::AL, zR::AR, sL::AL→AL, sR::AR→AR :
if zL ⟨a⟩ zR and sL ⟨a→a⟩ sR
then e zL sL ⟨a⟩ e zR sR

I will test “e 0 succ”, where succ is defined by: succ n = n+1. This amounts to specializing the left side to: AL=Integer, zL=0, sL=succ. I will leave the right side arbitrary, so as to draw general conclusions about “e zR sR”.

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

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

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

for all nL::Integer, nR::AR :
if nL ~ nR, then succ nL ~ sR nR

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

• I want a minimal relation, so that “e 0 succ ⟨a⟩ e zR sR” 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::AR, the conclusion “e 0 succ ⟨a⟩ e zR sR” 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 ~ zR
• if nL ~ nR, then succ nL ~ sR nR

It works as a partial function from the left to the right: it maps 0 to zR, 1 to sR zR, 2 to sR (sR zR), 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 = sR (sR zR), there is no other choice.

Then we get:

for all type AR :
for all zR::AR, sR::AR→AR :
e 0 succ ~ e zR sR

Suppose testing dicovers e 0 succ = 2. Then e zR sR = sR (sR zR), and this works for all AR, zR, and sR.

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 zR sR
• i≥0 because ~ doesn’t allow negative integers on the left
• f zR sR = sR (… (sR zR)…), “start with zR and apply sR 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:

for all type AL, type AR, relation ~ between AL and AR :
let ⟨a⟩ = “~” in
for all xL::AL, xR::AR :
if xL ~ xR
then trio xL ⟨[a]⟩ trio xR

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⟩:

for all type AL, type AR, function h::AL→AR :
let ⟨a⟩ be: x⟨a⟩y iff h x = y
for all xL::AL, xR::AR :
if h xL = xR
then fmap h (trio xL) = trio xR

I use the test case “trio ()”, so I’m specializing to: AL=(), xL=(), h () = xR.

for all type AR :
for all xR::AR :
fmap h (trio ()) = trio xR

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

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

### 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:

for all type AL, AR, BL, BR, h::AL→AR, k::BL→BR :
let ⟨a⟩ be: x⟨a⟩y iff h x = y
let ⟨b⟩ be: x⟨b⟩y iff k x = y
for all pL::(AL,BL), pR::(AR,BR) :
if pL ⟨(a,b)⟩ pR
then f pL ⟨a⟩ f pR

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

(x1,x2) ⟨(T,U)⟩ (y1,y2) iff: x1⟨T⟩y1 and x2⟨U⟩y2

Using that, and expanding “for all pL::(AL,BL)” to “for all x1::AL, x2::BL”, similarly for pR:

for all type AL, AR, BL, BR, h::AL→AR, k::BL→BR :
let ⟨a⟩ be: x⟨a⟩y iff h x = y
let ⟨b⟩ be: x⟨b⟩y iff k x = y
for all x1::AL, x2::BL, y1::AR, y2::BR :
if x1⟨a⟩y1 and x2⟨b⟩y2
i.e., h x1 = y1 and k x2 = y2
then f (x1,x2) ⟨a⟩ f (y1,y2)
i.e., h (f (x1,x2)) = f (y1,y2)

Simplifying:

for all type AL, AR, BL, BR, h::AL→AR, k::BL→BR :
for all x1::AL, x2::BL :
h (f (x1, x2)) = f (h x1, k x2)

I now specialize: AR=AL, BR=BL, h x = x1 (for all x::AL), k = the identity function. Idea: If f (x1, x2) returns any value at all, h maps that to x1.

for all type AL, BL :
for all x1::AL, x2::BL :
x1 = f (x1, x2)

There!

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.

I have more Haskell Notes and Examples