Common patterns of recursion

map is powerful because it sums up a pattern of recursion that turns up frequently in Hope programs. We can see another common pattern in the function length used above. Here's another example of the same pattern:

     dec sum : list ( num ) -> num ;
     --- sum ( nil )    <= 0 ;
     --- sum ( n :: l ) <= n + sum ( l ) ;
The underlying pattern consists of processing each element in the list and accumulating a single value that forms the result. In sum, each element contributes its value to the final result. In length the contribution is always 1 irrespective of the type or value of the element, but the pattern is identical. Functions that display this pattern are of type:
     ( list ( alpha ) -> beta )
In the function definition, the equation for a non-empty list parameter will specify an operation whose result is a beta. This is + in the case of length and sum. One argument of the operation will be a list element and the other will be defined by a recursive call, so the type of the operation needs to be:
     ( alpha # beta -> beta )
This operation differs between applications, so it will be supplied as a parameter. Finally we need a parameter of type beta to specify the base case result. The final version of the function is usually known as reduce. In the following definition, the symbol ! introduces a comment, which finishes with another ! or with a newline:
     dec reduce :   list ( alpha ) #            ! the input list          !
                    ( alpha # beta -> beta ) #  ! the reduction operation !
                    beta                        ! the base case result    !
                ->  beta ;                      ! the result type         !
     --- reduce ( nil, f, b )    <= b ;
     --- reduce ( n :: l, f, b ) <= f ( n, reduce ( l, f, b ) ) ;
To use reduce as a replacement for sum we'll need to supply the standard function + as an actual parameter. We can do this if we prefix it with the symbol nonop to tell the compiler we don't want to use it as an infix operator:
     reduce ( [ 1,2,3 ], nonop +, 0 ) ;
     6 : num
When we use reduce as a replacement for length, we're not interested in the first argument of the reduction operation because we always add 1 whatever the list element is. This function ignores its first argument:
     dec addone : alpha # num -> num ;
     --- addone ( _ , n ) <= n + 1 ;
We use _ to represent any argument we don't want to refer to.
     reduce ( "a map they could all understand", addone, 0 ) ;
     31 : num
Like map, reduce is much more powerful than it first appears because the reduction function needn't define a scalar. Here's a candidate that inserts an object into an ordered list of the same kind of object:
     dec insert : alpha # list ( alpha ) -> list ( alpha ) ;
     --- insert ( i, nil )    <= i :: nil ;
     --- insert ( i, h :: t ) <= if i < h
                              then i :: ( h :: t )
                              else h :: insert ( i, t ) ;
Actually this isn't strictly polymorphic as its declaration suggests, because it uses the built-in function <, which is only defined over numbers and characters, but it shows the kind of thing we can do. When we use it to reduce a list of characters:
     reduce ( "All sorts and conditions of men", insert, nil ) ;
     "     Aacddefiillmnnnnoooorssstt" : list ( char )
we can see that it actually sorts them. The sorting method (insertion sort) isn't very efficient, but the example shows something of the power of higher-order functions and of reduce in particular. It's even possible to use reduce to get the effect of map, but that's left as an exercise for the reader as they say.

Of course map and reduce only work on list ( alpha ) and we'll need to provide different versions for our own structured data types. This is the preferred style of Hope programming, because it makes programs largely independent of the `shape' of the data structures they use. Here's an alternative kind of binary tree that holds data at its nodes rather than its tips, and a reduce function for it:

     data tree ( alpha ) == empty ++
                       node ( tree ( alpha ) # alpha # tree ( alpha ) ) ;
     dec redtree : tree ( alpha ) #
              ( alpha # beta -> beta ) #
              beta -> beta ;
     --- redtree ( empty, f, b )            <= b ;
     --- redtree ( node ( l, v, r ), f, b ) <=
              redtree ( l, f, f ( v, redtree ( r, f, b ) ) ) ;
We can use this kind of tree to define a more efficient sort. An ordered binary tree has the property that all the objects in its left subtree logically precede the node object and all those in its right subtree are equal to the node object or logically succeed it. We can build an ordered tree if we have a function to insert new objects into an already-ordered tree, such as:
     dec instree : alpha # tree ( alpha ) -> tree ( alpha ) ;
     --- instree ( i, empty ) <= node ( empty, i, empty ) ;
     --- instree ( i, node ( l, v, r ) ) <=
              if i < v
               then node ( instree ( i, l ), v, r )
               else node ( l, v, instree ( i, r ) ) ;
We can sort a list by converting its elements into an ordered tree using instree, then flattening the tree back into a list. This is very easy to specify using the two kinds of reduction we've defined:
     dec sort : list ( alpha ) -> list ( alpha ) ;
     --- sort ( l ) <= redtree( reduce ( l, instree, empty ), nonop ::, nil ) ;
     sort ( "Mad dogs and Englishmen" ) ;
     "   EMaadddegghilmnnnoss" : list ( char )



Roger Bailey <rb@doc.ic.ac.uk>