An expression composed of constructors appearing on the left-hand side of a recursion equation is called a pattern. Selecting the right recursion equation and dismantling the actual parameter to name its parts is called pattern-matching. When you write a function, you must give a recursion equation for each possible constructor defining the argument type.
Sometimes we don't need to dismantle the actual parameter, and we can use a formal parameter in the pattern that matches the whole object, irrespective of what constructors were used to define it. As an example, let's see how we could define our own function to concatenate two lists like the built-in operation <>:
infix cat : 4 ;
dec cat : list( num ) # list( num ) -> list ( num ) ;
--- ( h :: t ) cat l <= h :: ( t cat l ) ;
--- nil cat l <= l ;
The first list parameter is matched by the pattern ( h :: t ) so that its
first item (the `head') and the remaining list (the `tail') can be referred
to separately on the right-hand side. The second recursion equation covers
the case when the first list is empty. The second list parameter is matched
by the pattern l whether it's empty or not.
As well as writing enough recursion equations to satisfy all the parameter constructors, we must also be careful not to write sets of equations where more than one pattern might match the actual parameters, because that would be ambiguous.
We can write patterns to match arguments that are tuples in the same way using the tuple constructor ,. When we wrote mult ( x, y ) you probably thought the parentheses and the comma were something to do with the function application. In fact, we were constructing a tuple and the parentheses were only needed because , has a low priority. Hope treats all functions as having only one argument. This can be a tuple when you want the effect of several arguments. Without parentheses,
mult x, y
would be interpreted as:
( mult ( x ), y )
A recursion equation with the left-hand side:
--- mult ( x, y ) <= ...
is just a pattern-match on a tuple. The first item in the tuple gets named
x and the second one y.
We can also use pattern-matching on num parameters. These are defined by two constructors called succ and 0. succ defines a number in terms of the next lower one. 0 has no arguments and defines the value zero. Surely 0 is a value, not a function? Well, we're already used to thinking of function applications as another way of writing values, so it's quite consistent to think of 0 as a function application. Here's a version of mult that uses pattern-matching to identify the base case:
infix mult : 8 ;
dec mult : num # num -> num ;
--- x mult 0 <= 0 ;
--- x mult succ ( y ) <= ( x mult y ) + x ;
We can read succ ( y ) as `the successor of some number that we'll call
y'. Instead of naming the actual parameter y like we did in the original
version of mult, we're naming its predecessor.