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, if f :: a -> [a] and a test case yields f () = [(), (), ()], then we can deduce f 4 = [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 IS that exports this interface:

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

then this program that uses IS

import IS

use :: Bool
use = let
    s0 = emptyset
    s1 = insert 4 s0
    s2 = insert 5 s1
  in lookup 4 s2

is very much like this polymorphic function

polyUse :: a
        -> (Int -> a -> a)
        -> (Int -> a -> Bool)
        -> Bool
polyUse emp ins lkp = let
    s0 = emp
    s1 = ins 4 s0
    s2 = ins 5 s1
  in lkp 4 s2

Hopefully you are also thrilled to see:

• If you rewrite use to polyUse, that’s dependency injection.

• If you test either by giving it a mock version of IS, that’s mock testing.

  Emphatically, you use the test result to predict what will happen under a production version of IS, 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
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 = []
  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
  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 i = j and xs ~ t, then insert_L i xs ~ insert_B j t
• if i = j and xs ~ t, then lookup_L i xs = lookup_B j t

(It looks redundant to assume “i = j” instead of just having i, but I am setting up for a generalization later.)

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 :: Bool
use = let
    s0 = emptyset
    s1 = insert 4 s0
    s2 = insert 5 s1
  in lookup 4 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 :: Bool
use_L = let
    s0_L = emptyset_L
    s1_L = insert_L 4 s0_L
    s2_L = insert_L 5 s1_L
  in lookup_L 4 s2_L

use_B :: Bool
use_B = let
    s0_B = emptyset_B
    s1_B = insert_B 4 s0_B
    s2_B = insert_B 5 s1_B
  in lookup_B 4 s2_B

Step through both versions to check:

• s0_L ~ s0_B
• Therefore, s1_L ~ s1_B
• Therefore, s2_L ~ s2_B
• Therefore, lookup_L 4 s2_L = lookup_B 4 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 relation for T between Dom_L(T) and Dom_R(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 “lookup_L ⟨Int→IntSet→Bool⟩ lookup_B” to be a thing and be true, for example. This is the hard part, but I think I have primed you for it.

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⟩, the motivation is “if inputs correspond, then outputs correspond” as hinted earlier. So we define formally:

For example, “lookup_L ⟨Int→IntSet→Bool⟩ lookup_B” expands to:

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

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

That allows us to deduce: use_L ⟨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
• left side implementation: Dom_L(A) = A_L, op_L :: Dom_L(U)
• right side implementation: Dom_R(A) = A_R, op_R :: Dom_R(U)
• (~) is a relation between A_L and A_R
• under ⟨A⟩ = (~), we have 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.

The type abstraction theorem can be rearranged as (giving explicit “for all” to A_L, A_R, (~), op_L, op_R):

Applied to the IntSet example:

If you perform dependency injection, you get this parametric polymorphic function:

polyUse :: a
        -> (Int -> a -> a)
        -> (Int -> a -> Bool)
        -> Bool
polyUse emp ins lkp = let
    s0 = emp
    s1 = ins 4 s0
    s2 = ins 5 s1
  in lkp 4 s2

Then use_L is converted to “polyUse emptyset_L insert_L lookup_L”. (A_L is implicit, hidden under the act of instantiating a to A_L; some people make it explicit with “polyUse_AL”.) Similarly for use_R.

And the type abstraction theorem can be converted accordingly:

Note that it has a drastic (cheesy?) simplification by the definition of ⟨T→U⟩:

That motivates extending the definition of ⟨⟩ to polymorphic types:

With that definition, this is true of polyUse:

polyUse ⟨∀a. a→(Int→a→a)→(Int→a→Bool)→Bool⟩ polyUse

The parametricity theorem says that it’s true 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 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 . I expand the parametricity theorem step by step:

0. The parametricity theorem says:

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

1. Expand ⟨∀a. …⟩

   for all type A_L, type A_R, relation (~) between A_L and A_R :
       let Dom_L(a) = A_L, Dom_R(a) = A_R, ⟨a⟩ = (~) in
       e ⟨a → (a → a) → a⟩ e

2. Expand ⟨a → (a → a) → a⟩

   for all type A_L, type A_R, relation (~) between A_L and A_R :
       let Dom_L(a) = A_L, Dom_R(a) = A_R, ⟨a⟩ = (~) in
       for all z_L::Dom_L(a), z_R::Dom_R(a), s_L::Dom_L(a→a), s_R::Dom_R(a→a) :
           if z_L ⟨a⟩ z_R and s_L ⟨a → a⟩ s_R
           then e z_L s_L ⟨a⟩ e z_R s_R

3. Expand s_L ⟨a → a⟩ s_R

   for all type A_L, type A_R, relation (~) between A_L and A_R :
       let Dom_L(a) = A_L, Dom_R(a) = A_R, ⟨a⟩ = (~) in
       for all z_L::Dom_L(a), z_R::Dom~R(a), s_L::Dom_L(a→a), s_R::Dom_R(a→a) :
           if z_L ⟨a⟩ z_R and (for all x::Dom_L(a), y::Dom_R(a): if x ⟨a⟩ y then s_L x ⟨a⟩ s_R y)
           then e z_L s_L ⟨a⟩ e z_R s_R

4. Expand Dom_L, Dom_R, ⟨a⟩

   for all type A_L, type A_R, relation (~) between A_L and A_R :
       for all z_L::A_L, z_R::A_R, s_L::A_L→A_L, s_R::A_R→A_R :
           if z_L ~ z_R and (for all x::A_L, y::A_R: if x ~ y then s_L x ~ s_R y)
           then e z_L s_L ~ e z_R s_R

(In future examples, I will jump straight to the final expansion.)

I will show that e is determined by e 0 succ, where succ = (λn → n+1). This and the proof below are inspired by how the assumption looks like induction over the natural numbers.

Choose A_L = ℕ, z_L = 0, s_L = succ. Choose (~) to be this functional relation: x~y iff f z_R s_R x = y, where f is defined recursively:

This shows two common tricks:

• Choose (~) in terms of some inputs (z_R and s_R in this example). This is legal by re-ordering the for-all variables.

• Usually choosing (~) to be a function makes things simpler.

  In later examples, I will write in this short form: “choose (~) to be the function f z_R s_R”.

After that choosing, we get

Then there are two assumptions to verify (left as an exercise):

• f z_R s_R 0 = z_R
• for all x::ℕ, y::A_R: if f z_R s_R x = y then f z_R s_R (succ x) = s_R y

With that, we get

It means: e hides a secret natural number n, and all it does is to start with z_R and apply s_R n times. The secret n can be exposed by e 0 succ. (Advanced students go on to say that the type (∀a . a → (a → a) → a) encodes ℕ.)

For example, if e 0 succ = 2, then e z_R s_R = s_R (s_R z_R).

Example: ∀a. a → [a]

Suppose e :: ∀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:

• [] ⟨[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.)

Usually the element-wise relation ⟨T⟩ is a function h; then ⟨[T]⟩ simplifies to the function map h, i.e., xs⟨[T]⟩ys iff map h xs = ys.

Going back to e :: ∀a. a → [a]. I prove that one special test, e (), tells you what e does in general. Choose A_L=(), x_L=(), (~) to be the function const x_R.

(The () type is called “the unit type”. It has only one value, also written as (). You can think of the type definition data Unit = TheOneAndOnly apart from notation. You can also think of a singleton set.)

Then we get:

The assumption (const x_R () = x_R) is easily verified. Conclusion:

So for example, if e () = [(), (), ()], then e x_R = map (const x_R) [(), (), ()] = [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 any 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:

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:

Choose A_L=(), B_L=(), xl=(), yl=(), (~) to be the function const xr, (#) to be the function const yr. Then:

The assumptions are easily verified. Conclusion:

i.e., xr = f (xr,yr).

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.

I have more Haskell Notes and Examples