#
All entries for Wednesday 30 April 2008

## April 30, 2008

### Weak Typing vs Weak Testing

I haven’t written a blog post on anything vaguely related to Computer Science in a while, so here’s an effort to change that. Bruce Eckel (BE) wrote a noted entry a while back, which seems to have been heavily discussed in what the guardian would refer to as the ‘blogosphere’, I’m thinking the kind of inflamatory and inaccurate articles that get posted on prc (not to say there aren’t good articles, but I find it increasingly difficult to sieve for something new and interesting these days).

I don’t intend to discuss BE’s terrible misconceptions that are perpetuated by this article, for example his reference to C++ as strongly typed, or blame him for not fixing the myriad of problems that the language has, after all standards bodies are mirred in backwards compatibility issues and compromise. I will blame him for the link to his blog not working, but thats another matter entirely.

What I really want to discuss is the limits of testing. Thats not to say that testing software isn’t a crucial part of the development process, and has helped me to find numerous bugs in software that I’ve written over time, but it has its limits. Now I’m not talking about expressiveness here – its plainly apparent to me that a test written in a turing complete programming language can test any property of the program that a decidably complete type checking algorithm can. Thats not really an idiomatic approach to testing unfortunately, since once one writes a test that is harder to reason about than the computer program they are trying to debug they have got a problem trying to test their test harness. I’ve numerous times found that the mistake was in a testcase, or harness that I’d coded up rather than the program itself.

A considerable number of unit tests are of a very simple form, for example testing that the sum of the numbers in the list [1,2,3,4] is 10. This is to be encourage and is all well and good. Unfortunately the problem occurs when one tries to extend these simple test cases to check complex properties. Let us imagine we are trying to write a function that sums up some numbers in a list, and we want to be confident that this function terminates. This is a trivial problem that I find it hard to think of how to test. Let us consider the following implementation, written in ML.

```
fun sum [] = 0
| sum (h :: t) = h + sum t;
```

I can be highly confident that this function terminates because I am using primitive recursion. This is a highly important approach in the development of usable theorem provers, for example the Isabelle theorem prover automatically generates proofs of termination for functions that are defined using primitive recursion. It is also easy to see how one would construct such a proof informally for this function:

1. Base Case: the list is empty so Its sum is 0. Statement holds true vacuously.

2. Inductive case: we have a list of length n. We assume that the sum of a list of length n-1 terminates and we know the addition function takes a finite amount of time to compute. Thus conclude that summing a list of length n terminates.

This is pretty much a trivial case for any primitive recursion function in ML. Our type checker helps us here – case exhaustiveness is checked for the function’s domain, in case we forget any possible cases. This may seem trivial for this function – but its incredibly useful. For example if one is writing an interpreter based on an IR composed from a union type of different datatype constructors for different IR elements.

I find it hard to convince myself that the python (chosen because of Mr. Eckel’s rampant fanboying) equivalent terminates. I have implemented the function like this:

```
def sum(l):
total = 0
for i in l:
total += i
return total
```

I don’t know where to begin in formulating a testcase to check termination. If someone does – then please comment on this blog, I’d really like to know if its possible.

A quick superficial glance would suggest that the foreach loop used here would allow me to conclude termination, but unfortunately it only return iterable items. Here’s an example:

```
def inf():
i = 0
while(True):
i = (i + 1) % 100
yield i
print sum(inf())
```

I can’t use static type checking to ensure that the parameter is a List unfortunately. I could add a decorator with explicit type checking, but unfortunately this can simply be monkey patched away. Similar problems exist if I choose to write this function in Java. For example:

```
int sum(Iterable<Integer> entries) {
int sum = 0;
for (Integer i: entries) {
sum += i;
}
return sum;
}
```

Since one could implement an iterable that always returns true. This can be resolved in Java (I think) through the following changes:

1. Write your function like:

```
int sum(ArrayList<Integer> entries) throws Exception {
if(entries.getClass() == java.util.ArrayList.class) {
int sum = 0;
for (Integer i: entries) {
sum += i;
}
return sum;
} else {
throw new Exception("Might not terminate since you are using a subclass of ArrayList");
}
}
```

2. Use a custom security manager in order to ensure that system classes have been replaced.

This has obvious disadvantages – for example if one later decides that you want to use a LinkedList or a Vector. It also assumes that no one has replaced the system classes files (e.g. rt.jar) with miscreant ones. Though obviously that could be checked using the Class Data Sharing parameters. All in all – its a massive bunch of hacks that one doesn’t want to be forced into doing just to be convinced that a damn sum function terminates!

So here’s an open challenge – can anyone convince me that they can write a simple sum function in a weakly typed language (static or dynamic) and be sure that it terminates. If you can do it via testing then its bonus points! Either way you get my respect. Note that this is my definition of weakly typed languages – anything with a type system with more loopholes/problems/lack of expressiveness in than ML is weakly typed.