Suppose we have a list of integers and we want to write a function to add up all its elements. The declaration will look like this:
dec sumlist : list ( num ) -> num ;
We need to refer to the individual elements of the actual parameter in the
equations defining sumlist. We do this using an equation whose left-hand
side looks like this:
--- sumlist ( x :: y ) ...
This is an expression involving list constructors and corresponds to an
actual parameter that's a list. x and y are formal parameters, but they
now name individual parts of the actual parameter value. In an application
of sumlist like:
sumlist ( [ 1, 2, 3 ] )
the actual parameter will be `dismantled' so that x names the value 1 and
y names the value [ 2, 3 ]. The complete equation will be:
--- sumlist ( x :: y ) <= x + sumlist ( y ) ;
Notice there's no base case test. As we might expect, it's the empty list,
but we can't test for it directly in the equation because there's no formal
parameter that refers to the whole list. In fact, if we write the
application:
sumlist ( nil )
we'll get an error message because we can't dismantle nil to find the
values of x and y. We must cover this case separately using a second
recursion equation:
--- sumlist ( nil ) <= 0 ;
The two equations can be given in either order. When sumlist is applied,
the actual parameter is examined to see which constructor function was used
to define it. If the actual parameter is a non-empty list, the first
equation is used, because non-empty lists are defined using the ::
constructor. The first number in the list gets named x and the remaining
list y. If the actual parameter is the empty list, the second equation is
be used because empty lists are defined using the constructor nil.