“Implications” of Parametric Polymorphism

Round 1

-- What does this function do?
foo :: a -> a
// in pseudo C#/Java
A foo(A x);

foo is a function that takes an a and returns an a, but a can be any type. So what does foo do? There’s no way foo can know what concrete type a is — a could be an integer, a string, a list, etc. foo doesn’t know how to make a new a, and foo also doesn’t know how to manipulate an a. This leaves only one possibility: foo returns the a that it’s given. This is called the ‘unit’ function.

Round 2

-- What does this function do
bar :: a -> b
// in pseudo C#/Java
B bar(A x);

What does bar do? Nothing. We can’t even implement bar because we don’t know how to create a b. We can write functions that take integers and return strings, but we can’t write a function that returns a generic b without knowing how to create a b or an example of a b.

Round 3

-- What does this function do?
bar :: (a -> b) -> a -> b
// in pseudo C#/Java
B bar(Function<A,B> f, A x);

Now what does bar do? Bar takes a function from a to b and an a; it returns a b. bar doesn’t know anything about a or b, but it does have a new tool: a function from a to b. The only way to implement this function?bar must apply the it’s first argument with it’s second argument. Here’s what that looks like:

bar :: (a -> b) -> a -> b
bar f a = f a
// in pseudo C#/Java
B bar(Function<A,B> f, A x) {
return f(x);
}

The Twist

Now answer these questions:

  1. Given a, prove that a is true
  2. Given a, prove that b is true
  3. Given that a implies b and a, prove that b true

These three questions aren’t any different from the previous three. If you want to prove these statements, you need to look at what truths are given/what parameters are provided. After looking at the given truths, follow the implications. If you show that the implications link to what you want to prove, then you’ve proved it. It’s the same thing in programming, just swap “prove” with “implement” and “given truths” with “parameters.”

Given all a function’s parameters, what implementations can this function have? Follow the types. Any path from the parameters to the return type is both an implementation and a proof that the function can be implemented.