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

- Given
*a*, prove that*a*is true - Given
*a*, prove that*b*is true - 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.