ML functions from polymorphic lists to polymorphic lists

Question

I'm learning programming in ML (OCaml), and earlier I asked about ML functions of type 'a -> 'b. Now I've been experimenting a bit with functions of type 'a list -> 'b list. There are some obvious simple examples:

let rec loop l = loop l
let return_empty l = []
let rec loop_if_not_empty = function [] -> []
                                   | l -> loop_if_not_empty l

What I can't figure out is how to make a function that does something other than return the empty list or loop (without using any library function). Can this be done? Is there a way to return non-empty lists?

Edit: Yes, if I have a function of type 'a -> 'b, then I can make another one, or a function of type 'a list -> 'b list, but what I'm wondering here is how to make the first one.

Answer 1

Well, something known as parametricity tells us that if we consider the pure subset of ML (that is, no infinite recursion, ref and all that weird stuff), there is no way to define a function with this type other than the one returning the empty list.

This all started with Wadler's paper “Theorems for free!”. This paper, basically, tells us two things:

1. If we consider programming languages that satisfy certain conditions, we can deduce some cool theorems just by looking at the type signature of a polymorphic function (this is called the Parametricity Theorem).
2. ML (without infinite recursion, ref and all that weird stuff) satisfies those conditions.

From the Parametricity Theorem we know that if we have a function f : 'a list -> 'b list, then for all 'a, 'b, 'c, 'd and for all functions g : 'a -> 'c, h : 'b -> 'd we have:

map h ∘ f = f ∘ map g

(Note, f on the left has type 'a list -> 'b list and f on the right is 'c list -> 'd list.)

We are free to choose whatever g we like, so let 'a = 'c and g = id. Now since map id = id (easy to prove by induction on the definition of map), we have:

map h ∘ f = f

Now let 'b = 'd = bool and h = not. Let's assume for some zs : bool list it happens that f zs ≠ [] : bool list. It is clear that map not ∘ f = f does not hold, because

(map not ∘ f) zs ≠ f zs

If the first element of the list on the right is true, then on the left the first element is false and vice versa!

This means, our assumption is wrong and f zs = []. Are we done? No.

We assumed that 'b is bool. We've shown that when f is invoked with type f : 'a list -> bool list for any 'a, f must always return the empty list. Can it be that when we call f as f : 'a list -> unit list it returns something different? Our intuition tells us that this is nonsense: we just can't write in pure ML a function that always returns the empty list when we want it to give us a list of booleans and might return a non-empty list otherwise! But this is not a proof.

What we want to say is that f is uniform: if it always returns the empty list for bool list, then it has to return the empty list for unit list and, in general, any 'a list. This is exactly what the second point in the bullet list in the beginning of my answer is about.

The paper tells us that in ML f must take related values to related ones. I'm not going into details about relations, it is enough to say that lists are related if and only if they have equal lengths and their elements are pair-wise related (that is, [x_1, x_2, ..., x_m] and [y_1, y_2, ..., y_n] are related if and only if m = n and x_1 is related to y_1 and x_2 is related to y_2 and so on). And the fun part is, in our case, since f is polymorphic, we can define any relation on the elements of lists!

Let's pick any 'a, 'b and look at f : 'a list -> 'b list. Now look at f : 'a list -> bool list; we've already shown that in this case f always returns the empty list. We now postulate that all the elements of 'a are related to themselves (remember, we can choose any relation we want), this implies that any zs : 'a list is related to itself. As we know, f takes related values to related ones, this means that f zs : 'b list is related to f zs : bool list, but the second list has length equal to zero, and since the first one is related to it, it is also empty.

---

For completeness, I'll mention that there is a section on impact of general recursion (possible non-termination) in the Wadler's original paper, and there is also a paper exploring free theorems in the presence of seq.

Answer 2

Let's get back to simpler objects: you cannot build an proper object of type 'a because then it would mean this object x can be used wherever 'a would fit. And that means everywhere: as an integer, an array, even a function. For example that would mean you can do things like x+2, x.(1) and (x 5). Types exist exactly to prevent this.

This the same idea that apply with a function of type 'a -> 'b, but there are some cases where this type can exists: when the function never returns an object of type 'b: when looping or raising an exception.

This also apply to functions that return a list. If your function is of type t -> 'b list and that you build an object of type t and apply it to this function, then that means that if you successfully access an element of this list then you will access to an object that have all types. So you can't access any element of the list: the list is either empty or ... there is no list.

However the type 'a list -> 'b list appears in usual exercises but that's only when you already have a function of type 'a -> 'b:

let rec map (f : 'a -> 'b) =
  function
  | [] -> []
  | x :: xs -> f x :: map f xs

But you probably know this one.

val map : ('a -> 'b) -> 'a list -> 'b list

Answer 3

Parametricity Theorem from the “Theorems for Free!” paper tells us that ML terms have a very special property: if we view a term’s type as a relation on values of this type, then this term’s value will be related to itself. Here is how to view types as relations:

• A function type 'a -> 'b corresponds to the relation defined by saying that two functions are related if they take related values to related values (assuming 'a and 'b correspond to some relations).
• A list type 'a list corresponds to the relation defined by saying that two lists are related if they have the same length and their matching elements are related (assuming 'a corresponds to some relation).
• (Now the most interesting part.) A polymorphic type corresponds to the relation defined by saying that two polymorphic values are related if we can choose any two types, any relation between the elements of these types, replace all instances of the type variable with this relation, and the resulting values will still be related.

Here is an example. Suppose we have a term foo : 'a -> 'a. The Parametricity Theorem says that foo is related to itself. What this means is that we can choose any two types, say, $A_1$ and $A_2$, choose absolutely any relation $\mathbf{A}$ between elements of this type, and if we take any $a_1 : A_1$ and $a_2 : A_2$, such that they are related according to $\mathbf{A}$, then $\operatorname{foo} a_1$ and $\operatorname{foo} a_2$ will also be related according to $\mathbf{A}$:

$$ a_1 \sim_\mathbf{A} a_2 \Rightarrow \operatorname{foo} a_1 \sim_\mathbf{A} \operatorname{foo} a_2. $$

Now if we take the relation $\mathbf{A}$ to be not an arbitrary relation, but a function $f : A_1 \to A_2$, the above becomes:

$$ f(a_1) = a_2 \Rightarrow f(\operatorname{foo} a_1) = \operatorname{foo} a_2, $$

or, in other words:

$$ f(\operatorname{foo} a_1) = \operatorname{foo} (f(a_1)), $$

which is exactly the free theorem for the id function: f . id = id . f.

---

If you perform similar steps for your function foo : 'a list -> 'b list, you’ll get that you can choose any two types $A_1$ and $A_2$, any relation $\mathbf{A}$ between their elements, any two types $B_1$ and $B_2$, any relation $\mathbf{B}$ between their elements, then take any two lists, first made of elements of $A_1$, second made of elements of $A_2$, apply your function to both lists (getting a list of $B_1$ in the first case and a list of $B_2$ in the second), and the results will be related, if the inputs were related.

Now we use this to prove that for any two types A and B the function foo returns an empty list for any input as : A list.

• Let $A_1 = A_2 = $ A and let $\mathbf{A}$ be the identity relation, thus any list of $A$ is trivially related to itself.
• Let $B_1 = $ Ø, $B_2 = $ B and $\mathbf{B}$ any relation between them (there is only one, the empty one, but it doesn’t matter).
• as is related to itself (as we chose the identity relation on A), thus foo as : Ø list is related to foo as : B list.
• We know that two lists can be related only if their lengths are equal and we also know that the first of the resulting lists must be empty, as there can be no elements of the Ø type.

Therefore, for any A, B and as : A list we have that foo as : B list has to be an empty list.