Defining Functions on Lists

Here is a function for adding a list of numbers together:

sum: list(num) -> num;
sum [ ] <= 0;
sum(x::m) <= x + sum(m);

We read this as follows: The sum of the empty list of integers is zero. To sum the list of integers whose head is x and whose tail is m, we sum the tail, m and add the head x to the result.

How is this evaluated? Suppose we ask Hope to evaluate sum[2]. Now [2] is the list whose head is 2 and whose tail is []. So [2]=2::[]. So sum[2]=sum(2::[]). This matches the second rule for sum with x=2 and m=[].

So we rewrite the right hand side of the second rule with x=2 and m=[] to give 2+sum([]);

By the first rule for sum, sum([])=0 so the result of sum[2] is 2+0 which is 2.