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:
- 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).
- 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
.