If we wanted to write a Pascal program to print the first n natural numbers in descending order we'd probably write a loop that printed one value out on each iteration, such as:
for i := n downto 1 do write ( i ) ;
In Hope we write one expression that defines all the values at once, rather
like we did for mult:
dec nats : num -> list ( num ) ;
--- nats ( n ) <= if n = 0 then nil else n :: nats ( n-1 ) ;
nil is useful for writing the base case of a recursive function that
defines a list. If we try the function at the terminal by typing:
nats ( 10 ) ;
[ 10,9,8,7,6,5,4,3,2,1 ] : list ( num )
we can see that the numbers are in descending order because that's the way we
arranged them in the list, and not because they were defined in that order.
The values in the expression defining the list are treated as though they
were all generated at the same time. On the ALICE machine they actually are
generated at the same time.
To get the results of a Hope program in the right order, we must put them in the right place in the final data structure. If we want the list of the numbers n through 1 in the opposite order we can't write the definition as:
... else nats ( n-1 ) :: n ;
because the argument types for :: are the wrong way round. We need to use
a another built-in operation <> (read as `append') that concatenates two
lists. The definition will then look like this:
--- nats ( n ) <= if n = 0 then nil else nats ( n-1 ) <> [ n ] ;
We put n in brackets to make it into a (single-item) list because <>
expects both its arguments to be lists.
We could also have written ( n :: nil ) instead of [ n ].