%OP%BON
%OP%JUY
%OP%DFT
%OP%GRN
%OP%TM3
%OP%HM4
%OP%FM4
%OP%BM3
%OP%LM2
%OP%FO/Hope Tutorial//Page @P@/
%OP%AMM
%CO:A,5,78%
%C%%H2%A HOPE TUTORIAL%H2%

%C%%H2%Roger Bailey, Imperial College%H2%








%C%%H2%Functions In Conventional Languages:%H2%

%JR%In a language like Pascal, a function is a piece of 'packaged' program for 
%JL%performing standard operations like finding square roots.  To obtain the 
square root of a positive number stored in a variable x, we write:


at the point in the program where we want the value, such as:




%JR%this is called an %H4%application%H4% of the function.  The value represented by "x" 
%JL%is called the %H4%argument%H4% or %H4%actual parameter%H4%.  In this context, the canned 
%JR%program computes the square root of "x", "1.0" is added to it and the result 
is then printed.


%JR%We can also define our own functions specifying how the result is computed 
%JL%using ordinary Pascal statements.  Here's a function that returns the greater 
of its two argument values:










%JR%The identifiers "x" and "y" are called %H4%formal parameters%H4%.  They're used 
%JL%inside the definition to name the two values that will be supplied as 
%JR%arguments when the function is applied.  We can use "max" anywhere we need a 
%JL%value, just like "sqrt".  Here's how we might use "max" to filter out 
negative values on output:



%P0%
%JR%A more interesting case is when the actual parameter is a function 
%JL%application itself or involves one.  We can use "max" to find the largest of 
%H4%three%H4% numbers by writing:





%JR%Combining functions together like this is called %H4%composition%H4%.  The expression 
%JL%is evaluated 'inside-out' because the outer application of "max" can't be 
%JR%evaluated until the value of its second argument is known.  The %H4%inner%H4% 
%JL%application of "max" is therefore evaluated first using the values of "b" and 
"c" and the result is used as the actual parameter of the outer application.


%JR%Another way of combining functions together is to define more powerful ones 
%JL%using simpler ones as 'building blocks'.  If we often need to find the 
largest of three numbers we might define:








and apply it by writing:









%C%%H2%Programming with functions%H2%

%JR%Pascal is called an %H4%imperative%H4% language because programs written in it are 
%JL%recipes for 'doing something'.  If our programs consist only of functions, we 
%JR%can concentrate on %H4%what%H4% the results are and ignore %H4%how%H4% they're computed. 
%JL%Forget that "sqrt" is a piece of code and think of "sqrt ( x )" as a way of 
%JR%writing a %H4%value%H4% in your program, and you'll get the idea.  You can think of 
%JL%"MaxOf3" like this as well if you ignore the way it works inside.  By 
%JR%defining a 'toolkit' of useful functions and combining them together like 
%JL%this, we can build powerful programs that are quite short and easy to 
understand.
%P0%
%JR%In Pascal, functions can only return 'simple' data objects such as numbers or 
%JL%characters, but real programs use big data structures and can't easily be 
%JR%written using these functions.  In Hope, functions can return %H4%any%H4% type of 
%JL%value, including data structures equivalent to Pascal's %H2%array%H2%s and %H2%record%H2%s 
%JR%and much more.  Programming in Hope has the flavour of simply 'writing down 
%JL%the answer' by writing an expression that defines it.  This will contain one 
%JR%or more function applications to define smaller parts of the answer.  These 
%JL%functions won't usually be built in like "sqrt", so we'll have to define them 
%JR%ourselves, but we'll still think of them as %H4%definitions%H4% of data objects, and 
not as %H4%algorithms%H4% for computing them.






%C%%H2%A simple Hope example -- conditionals%H2%

%JR%Let's see how we can define "max" in Hope.  Like Pascal, it's a 
%JL%%H4%strongly%H4%-%H4%typed%H4% language, which means we must tell the compiler about the 
%JR%types of all objects in our programs so it can check that they're used 
%JL%consistently.  The function definition comes in two parts.  First we declare 
the argument and result types:





%JR%"%H2%dec%H2%" is in bold face because it's a reserved word and you can't use it as a 
%JL%name.  Type it in lower case when entering programs.  "max" is the name of 
%JR%the function being defined.  Names consist of upper and lower case letters 
%JL%(which are distinct) and digits, and must start with a letter.  The current 
%JR%fashion is to use lower case.  The layout isn't significant and you can 
%JL%separate symbols with any number of blanks, tabs and newlines for clarity, as 
%JR%in this example.  Symbols need only be separated when they might otherwise be 
confused as one, such as "%H2%dec%H2%" and "max".


%JR%The next part of the declaration gives the types of the arguments (read the 
%JL%symbol ":" as 'takes a').  Non-negative integers are of the predefined type 
%JR%"num" (in lower case).  "#" is read as 'and a'; (or you can use the reserved 
%JL%word "%H2%X%H2%").  "->" is read as 'yields'.  The semicolon marks the end of the 
%JR%declaration, which tells the compiler that "max" takes two numbers as 
arguments and returns a single number as its result.


%JR%The result of a function is defined by one or more %H4%recursion equations%H4%.  
"max" needs only one equation to define it:



%P0%
%JR%Read the symbol "---" as 'the value of'.  The expression "max ( x, y )" is 
%JL%called the %H4%left%H4%-%H4%hand side%H4% of the equation.  It defines "x" and "y" as formal 
%JR%parameters, or local names for the values that will be supplied when the 
%JL%function is applied.  Parameter names are local to the equation, so "x" and 
%JR%"y" won't be confused with any other "x" or "y" in the program.  The symbol 
"<=" is read as 'is defined as'.


%JR%The rest of the equation (called the %H4%right%H4%-%H4%hand side%H4%) defines the result. 
%JL%It's a conditional expression.  The symbols "%H2%if%H2%", "%H2%then%H2%" and "%H2%else%H2%" are 
%JR%reserved words.  Pascal's conditional statement chooses between alternative 
%JL%%H4%actions%H4%, but Hope's conditional expression chooses between alternative 
%JR%%H4%values%H4%, in line with our view that function applications are ways of writing 
%JL%values rather than recipes for computing them.  If the value of the 
%JR%expression "x > y" is "true", the value of the whole conditional expression 
%JL%is the value of "x", otherwise it's the value of "y".  The alternative values 
can be defined by any Hope expressions.


%JR%When the value of a function is defined by more than one expression like 
%JL%this, they are evaluated in an unspecified order.  On a suitable computer, 
%JR%such as the Imperial College ALICE machine, it's even possible to evaluate 
%JL%both expressions and the test in parallel and throw away one of the values 
according to the result of the test.






%C%%H2%Using functions that we've defined%H2%

%JR%A Hope program is just a a single expression containing one or more function 
%JL%applications composed together.  It's evaluated immediately and the result 
%JR%and its type are printed on the screen.  Here's a simple program that uses 
"max", with its output (which is shown in italics):






%JR%The rules for evaluating the expression are the same as those of Pascal: 
%JL%function arguments are evaluated first, the functions are applied, and 
finally other operations are performed in the usual order of priority. 
%P0%
%JR%We can also use existing functions to define new ones.  Here's the Hope 
version of "MaxOf3":










%C%%H2%A more interesting example - repetition%H2%

%JR%Just as Pascal's conditional statement is replaced by Hope's conditional 
%JL%value, so the repetitive statement is replaced by the %H4%repetitive value%H4%. 
Here's a Pascal function that multiplies two numbers using repeated addition:
















%JR%It's hard to be sure this function does enough additions (it took me three 
%JL%tries to get it right) and this seems to be a general problem with loops in 
%JR%programs.  A common way of checking imperative programs is to simulate their 
%JL%execution.  If we do this for input values of 2 and 3, we'll find that "prod" 
%JR%starts with the value 0 and gets values of 2, 4 and 6 on successive loop 
iterations, which suggests the definition is correct.
%P0%
%JR%Hope doesn't have any loops, so we must write all the additions that the 
%JL%Pascal program performed in a single expression.  It's much easier to see 
that this has the right number of additions:






%JR%or would be if we knew how many times to write "+ x".  The hand simulation 
%JL%suggests we need to write it "y" times, which is tricky when we don't know 
%JR%the value of "y".  What we do know is that for a given value of "y", the 
expressions:





%JR%will have the same number of "+ x" terms if written out in full.  The second 
%JL%one always has two terms, whatever the value of "y", so we'll use it as the 
definition of "mult":





%JR%On the face of it we've written something ridiculous, because it means we 
%JL%must apply "mult" to find the value of "mult".  Remember however that this is 
%JR%really shorthand for "0" followed by "y" occurrences of "+ x".  When "y" is 
%JL%zero, the result of "mult" is also zero because there are %H4%no%H4% "+ x" terms.  In 
%JR%this case "mult" isn't defined in terms of itself, so if we add a special 
test for it, the definition terminates.  A usable definition of "mult" is:





%JR%Functions that are defined using themselves like this are called %H4%recursive%H4%.  
%JL%Every Pascal program using a loop can be expressed as a recursive function in 
%JR%Hope.  All recursive definitions need one case (called the %H4%base case%H4%) where 
%JL%the function isn't defined in terms of itself, just as Pascal loops need a 
terminating condition.
%P0%
%C%%H2%Another way of using functions%H2%

%JR%Hope allows us to use a function with two arguments like "mult" as an infix 
%JL%operator.  We must assign it a priority and use it as an operator everywhere 
%JR%including the equations that definine it.  The definition of "mult" when used 
as an infix operator looks like this:






 
%JR%A bigger number in the %H2%infix%H2% declaration means a higher priority.  The second 
%JL%argument of "mult" is parenthesised because its priority of 8 is greater than 
%JR%the built-in subtraction operation.  Most of Hope's standard functions are 
supplied as infix operators.






%C%%H2%Other kinds of data%H2%


%JR%Hope provides two other primitive data types.  A "truval" (truth value) is 
%JL%equivalent to a Pascal Boolean and has values "true" and "false".  We've 
%JR%already seen the expression "x > y" defining a truth value.  ">" is a 
%JL%standard function whose type is "num # num -> truval".  We can use truth 
%JR%values in conditional expressions and combine them together with the standard 
functions "and", "or" and "not".


%JR%Single characters are of type "char", with values "'a'", "'b'" and so on.  
%JL%Characters are most useful as components of data structures such as 
character-strings.
%P0%
%C%%H2%Data structures%H2%

%JR%Practical programs need data structures and Hope has two standard kinds 
%JL%already built in.  The simplest kind corresponds to a Pascal record. We can 
%JR%bind a fixed number of objects of any type together into a structure called a 
%H4%tuple%H4%, for example:





%JR%are tuples of type "num # num" and "char%H2%%H2% # truval" respectively.  We use 
%JL%tuples when we want a function to define more than one value.  Here's one 
that defines the time of day given the number of seconds since midnight:








%JR%"div" is the built-in integer division function and "mod" gives the remainder 
%JL%after integer division.  If we type an application of "time24" at the 
%JR%terminal, the result tuple and its type will be printed on the screen in the 
usual way:




%P0%
%JR%The second standard data type, called a %H4%list%H4%, corresponds roughly to a 
%JL%one-dimensional array in Pascal.  It can contain any number of objects 
%JR%(including none at all) but they must all be the same type.  We can write 
expressions in our programs that represent lists, such as:





%JR%which is of type "list ( num )".  There are two standard functions for 
%JL%defining lists.  The infix operator "::" (read as 'cons') defines a list in 
terms of a single object and list containing the same type of object, so





defines the list:





%JR%Don't think of "::" as adding "10" to the front of "[ 20, 30, 40 ]".  It 
%JL%really definines a %H4%new%H4% list "[ 10, 20, 30, 40 ]" in terms of two other 
%JR%objects without changing their meaning, rather in the same way that "1 + 3" 
defines a new value of "4" without changing the meaning of "1" or "3".


%JR%The other standard list function is "nil", which defines a list with no 
%JL%elements in it.  We can represent every list by an expression consisting of 
applications of "::" and "nil".  When we write an expression like:





it's considered to be a shorthand way of writing:





%JR%There's also a shorthand way of writing lists of characters.  The following 
three expressions are all equivalent:



%P0%
%JR%When the result of a Hope program is a list, it's always printed out in the 
%JL%concise bracketed notation; if it's a list of characters, it's printed in 
quotes.


%JR%Every data type in Hope is defined by a set of primitive functions like "::" 
%JL%and "nil".  They're called %H4%constructor%H4% functions, and aren't defined by 
%JR%recursion equations.  When we defined a tuple, we were actually using a 
%JL%standard constructor called "," (read as 'comma').  Later on we'll see how 
constructors are defined for other types of data.





%C%%H2%Functions that define lists%H2%


%JR%If we wanted to write a Pascal program to print the first %H4%n%H4% natural numbers 
%JL%in descending order we'd probably write a loop that printed one value out on 
each iteration, such as:





%JR%In Hope we write one expression that defines all the values at once, rather 
like we did for "mult":






%JR%"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:






%JR%we can see that the numbers are in descending order because that's the way we 
%JL%arranged them in the list, and %H4%not%H4% because they were defined in that order.  
%JR%The values in the expression defining the list are treated as though they 
%JL%were all generated at the same time.  On the ALICE machine they actually %H4%are%H4% 
generated at the same time.
%P0%
%JR%To get the results of a Hope program in the right order, we must put them in 
%JL%the right place in the final data structure.  If we want the list of the 
%JR%numbers "n" through "1" in the opposite order we can't write the definition 
as:





%JR%because the argument types for "::" are the wrong way round.  We need to use 
%JL%a another built-in operation "<>" (read as 'append') that concatenates two 
lists.  The definition will then look like this:





%JR%We put "n" in brackets to make it into a (single-item) list because "<>" 
%JL%expects both its arguments to be lists.  We could also have written "( n :: 
nil )" instead of "[ n ]".






%C%%H2%Data structures as parameters%H2%


%JR%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:





%JR%We need to refer to the individual elements of the actual parameter in the 
%JL%equations defining "sumlist".  We do this using an equation whose left-hand 
side looks like this:



%P0%
%JR%This is an expression involving list constructors and corresponds to an 
%JL%actual parameter that's a list.  "x" and "y" are formal parameters, but they 
%JR%now name %H4%individual parts%H4% of the actual parameter value.  In an application 
of "sumlist" like:





%JR%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:





%JR%Notice there's no base case test.  As we might expect, it's the empty list, 
%JL%but we can't test for it directly in the equation because there's no formal 
%JR%parameter that refers to the whole list.  In fact, if we write the 
application:
 




%JR%we'll get an error message because we can't dismantle "nil" to find the 
%JL%values of "x" and "y".  We must cover this case separately using a second 
recursion equation:





%JR%The two equations can be given in either order.  When "sumlist" is applied, 
%JL%the actual parameter is examined to see which constructor function was used 
%JR%to define it.  If the actual parameter is a non-empty list, the first 
%JL%equation is used, because non-empty lists are defined using the "::" 
%JR%constructor.  The first number in the list gets named "x" and the remaining 
%JL%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".
%P0%
%C%%H2%Pattern-matching%H2%

%JR%An expression composed of constructors appearing on the left-hand side of a 
%JL%recursion equation is called a %H4%pattern%H4%.  Selecting the right recursion 
%JR%equation and dismantling the actual parameter to name its parts is called 
%JL%%H4%pattern%H4%-%H4%matching%H4%.  When you write a function, you must give a recursion 
equation for each possible constructor defining the argument type. 


%JR%Sometimes we don't need to dismantle the actual parameter, and we can use a 
%JL%formal parameter in the pattern that matches the whole object, irrespective 
%JR%of what constructors were used to define it.  As an example, let's see how we 
%JL%could define our own function to concatenate two lists like the built-in 
operation "<>":








%JR%The first list parameter is matched by the pattern "( h :: t )" so that its 
%JL%first item (the 'head") and the remaining list (the 'tail') can be referred 
%JR%to separately on the right-hand side.  The second recursion equation covers 
%JL%the case when the first list is empty.  The second list parameter is matched 
by the pattern "l" whether it's empty or not.


%JR%As well as writing enough recursion equations to satisfy all the parameter 
%JL%constructors, we must also be careful not to write sets of equations where 
%JR%more than one pattern might match the actual parameters, because that would 
be ambiguous.


%JR%We can write patterns to match arguments that are tuples in the same way 
%JL%using the tuple constructor ",".  When we wrote "mult ( x, y )" you probably 
%JR%thought the parentheses and the comma were something to do with the function 
%JL%application.  In fact, we were constructing a tuple and the parentheses were 
%JR%only needed because "," has a low priority.  Hope treats all functions as 
%JL%having only one argument.  This can be a tuple when you want the effect of 
several arguments.  Without parentheses,





would be interpreted as:



%P0%
A recursion equation with the left-hand side:





%JR%is just a pattern-match on a tuple.  The first item in the tuple gets named 
"x" and the second one "y".


%JR%We can also use pattern-matching on "num" parameters.  These are defined by 
%JL%two constructors called "succ" and "0".  "succ" defines a number in terms of 
%JR%the next lower one.  "0" has no arguments and defines the value zero.  Surely 
%JL%"0" is a %H4%value%H4%, not a function? Well, we're already used to thinking of 
%JR%function applications as another way of writing values, so it's quite 
%JL%consistent to think of "0" as a function application.  Here's a version of 
"mult" that uses pattern-matching to identify the base case:








%JR%We can read "succ ( y )" as 'the successor of some number that we'll call 
%JL%"y"'.  Instead of naming the actual parameter "y" like we did in the original 
version of "mult", we're naming its predecessor.
%P0%
%C%%H2%Simplifying expressions%H2%

%JR%In Pascal programs we can simplify complex expressions by removing common 
sub-expressions and evaluating them separately.  Instead of:





we would probably write:





%JR%which is clearer and more efficient.  Hope programs consist only of 
%JL%expressions and it's even more important to simplify them.  We do this by 
using a %H4%qualified expression%H4%:





%JR%This looks like an assignment, but it isn't.  "==" is read as 'is defined as' 
%JL%and "z" is local to the expression following the "%H2%in%H2%".  If we write something 
like:





%JR%we're actually introducing a new variable "z" to use in the sub-expression "z 
* z".  It hides the original one in the sub-expression "z + 1".


%JR%There's a second form of qualified expression for people who like to use 
variables first and define their meanings later.  It looks like this:





%JR%The result of the qualified expression is the same whether we define it using 
%JL%%H2%let%H2% or %H2%where%H2%.  "x + y" is evaluated first, and its value is used in the main 
expression.
%P0%
%JR%The qualifying expression will often be a function application that defines a 
%JL%data structure.  If we want to name part of the structure we can use a 
pattern on the left-hand side of the "==" symbol:







%JR%We'll use this construction most often when we write recursive functions that 
%JL%define tuples.  Here's a typical example.  Suppose we want to form a string 
%JR%of words from a sentence.  For simplicity a word is taken to be any sequence 
%JL%of characters, and words are separated in the sentence by any number of 
%JR%blanks.  The sentence and a single word will be of type "list ( char )" and 
the final sequence of words a "list ( list ( char ) )".


%JR%It's fairly straightforward to obtain the first word.  Here's a function that 
does it:









%JR%One of the nice features of Hope is that we can type in and print out any 
%JL%kind of value, so it's easy to check out the individual functions of our 
program separately.  If we test "firsttry" we'll see:






%JR%But there's a problem here because we're going to need the rest of the 
%JL%sentence if we're to find the remaining words.  We must arrange that that the 
%JR%function returns the remaining list as well as the first word.  This is where 
tuples come in:








%P0%
%JR%The qualified expression is parenthesised so it only applies to the 
%JL%expression after the %H2%else%H2%, otherwise we'll evaluate "firstword" recursivly as 
%JR%long as the sentence is non-empty, even if it starts with a blank.  This 
version of the function produces:






%JR%We can use this to define a function to split the sentence into a list of its 
individual words:










which we can test by typing an application at the terminal:










%C%%H2%Review%H2%

%JR%So far we've concentrated on features of Hope that have something in common 
%JL%with traditional languages such as Pascal, but without many of their 
%JR%limitations, such as fixed-size data structures.  We've also been introduced 
%JL%to the functional style of programming where programs are no longer recipes 
for action, but just definitions of data objects.


%JR%Now we'll introduce features of Hope that lift it onto a much higher level of 
%JL%expressive power, and let us write programs that are not only extremely 
%JR%powerful and concise, but that can be checked for correctness at compile-time 
and mechanically transformed into more efficient versions.
%P0%
%C%%H2%Making functions more powerful%H2%

%JR%The Hope compiler can spot many common kinds of error by checking the types 
%JL%of all objects in expressions.  This is harder than checking at run-time, but 
%JR%more efficient and saves the embarrassment of discovering an error at 
%JL%run-time in a rarely-executed branch of the air traffic control system we 
just wrote.


%JR%However, strict type-checking can be a nuisance if we want to perform some 
%JL%operation that doesn't depend on the type of the data.  Try writing a Pascal 
%JR%procedure to reverse an array of %H4%either%H4% 10 integers %H4%or%H4% 10 characters and 
you'll see what I mean.


%JR%Hope avoids this kind of restriction by allowing a function to operate on 
%JL%more than one type of object.  We've already used the standard constructors 
%JR%"::" and "nil" to define a "list ( num )", a "list ( char )" and a "list ( 
%JL%list ( char ) )".  The standard equality function "=" will compare any two 
%JR%objects of the same type.  Functions with this property are called 
%JL%%H4%polymorphic%H4%.  Pascal's built-in functions "abs" and "sqr" and operations like 
">" and "=" are polymorphic in a primitive kind of way.


%JR%We can define our own polymorphic functions in Hope.  The function "cat" we 
%JL%defined above will concatenate lists of numbers, but we can use it for lists 
%JR%containing any type of object.  To do this we first declare a kind of 
%JL%'universal type' called a %H4%type variable%H4%.  We use this in the declaration of 
"cat" where it stands for any actual type:







%JR%This says that "cat" has two parameters that are lists and defines a list, 
%JL%but it doesn't say what kind of object is in the list.  However, "alpha" 
%JR%always stands for the same type throughout a given declaration, so all the 
lists must contain the %H4%same%H4% type of object.  The expressions:





%JR%are correctly-typed applications of "cat" and define a "list ( num )" and a 
"list ( char )" respectively, while the expression:



%P0%
%JR%isn't because "alpha" can't be interpreted as two %H4%different%H4% types.  The 
%JL%interpretation of a type variable is local to a declaration so it can have 
different interpretations in other declarations without confusion.


%JR%Of course it only makes sense for a function to be polymorphic as long as the 
%JL%equations defining it don't make any assumptions about types.  In the case of 
%JR%"cat" the definition uses only "::" and "nil", which are polymorphic 
%JL%themselves.  However, a function like "sumlist" uses "+" and can only be used 
with lists of numbers as parameters.






%C%%H2%Defining your own data types%H2%

%JR%Tuples and lists are quite powerful, but for more sophisticated applications, 
%JL%we'll need to define our own types.  User-defined types make programs clearer 
%JR%and help the type-checker to help the programmer.  We introduce a new data 
type in a %H4%data declaration%H4%:





%JR%"%H2%data%H2%" is a reserved word and "vague" is the name of the new type.  "==" is 
%JL%read as 'is defined as' and "++" is read as 'or'.  "yes", "no" and "maybe" 
%JR%are the names for the constructor functions of the new type.  We can now 
write function definitions that use these constructors in patterns:







%JR%The constructors can be parameterised with any type of object, including the 
%JL%type that's being defined.  We can define types like lists, whose objects are 
%JR%of unlimited size using this kind of recursive definition.  As an example, 
here's a user-defined binary tree that can contain numbers as its leaves:



%P0%
%JR%There are three constructors.  "empty" has no parameters and defines a tree 
%JL%with nothing in it.  "tip" defines a tree in terms of a single num, and 
"node" defines a tree in terms of two other trees.  Here's a typical tree:


%L%%H2%                                      .
%H2%                                     / \
%H2%                                    /   \
%H2%                                ___/     \___
%H2%                       ________/             \________
%H2%                      /       /               \       \
%H2%                     /       /\               /\       \
%H2%                    1       /  \             /  \       \
%H2%                           /    \           /    \       5
%H2%                          2      3         .      4   
                                 

%JR%Here's an example of a function that manipulates trees.  It returns the sum 
of all the numbers contained in one:








%JR%Unfortunately there's no shorthand for writing tree constants like there is 
%JL%for list constants, so we've got to write them out the long way using 
%JR%constructors.  If we want to use "sumtree" to add up all the numbers in the 
example tree above, we must type in the expression:










%JR%This isn't really a drawback, because programs that manipulate complex data 
%JL%structures like trees will generally define them using other functions. 
%JR%However, it's very useful to be able to type any kind of constant data 
%JL%structure at the terminal when we're checking out an individual function like 
%JR%"sumtree".  When we want to test a Pascal program piecemeal, we usually have 
to write elaborate test harnesses or stubs to generate test data.
%P0%
%C%%H2%Making data more abstract%H2%

%JR%The identifier "list" isn't really a Hope data type.  It's called a %H4%type 
%JL%constructor%H4% and must be parameterised with an actual type before it 
%JR%represents one.  We did this every time we declared a "list ( num )" or a 
%JL%"list ( char )".  The parameter can also be a user-defined type, as with a 
%JR%"list ( tree )" or even a type variable as in "list ( alpha )", which defines 
%JL%a %H4%polymorphic data type%H4%.  Constructing new data types like this is a 
%JR%compile-time operation by the way, and you shouldn't confuse it with 
constructing new data %H4%values%H4%, which is a run-time operation.


%JR%You can define your own polymorphic data types.  Here's a version of the 
binary tree we defined earlier that can have any type of value in its leaves:







%JR%Once again, "alpha" is taken to be the same type throughout one instance of a 
%JL%tree.  If it's a number, then all references to "tree ( alpha )" are taken as 
references to "tree ( num )".


%JR%We can define polymorphic functions that operate on trees containing any type 
%JL%of object, because tree constructors are now polymorphic.  Here's a function 
to 'flatten' a binary tree into a list of the same type of object:






%P0%
We can demonstrate it on various kinds of tree:



















%JR%Notice how the type-checker may need to go through several levels of data 
types to deduce the type of the result.
%P0%
%C%%H2%Even more concise programs%H2%

%JR%The importance of polymorphic types and functions is that they let us write 
%JL%shorter, clearer programs.  It's similar to the way Pascal procedures let us 
%JR%use the same code to operate on different data values, but much more 
%JL%powerful.  We can write a single Hope function to reverse a list of numbers 
%JR%or characters, where we'd need to write two identical Pascal subroutines to 
reverse an array of integers and an array of characters.

%JR%We can use polymorphic functions whenever we're concerned only with the 
%JL%arrangement of the objects in a data structure and not with their values.  
%JR%Sometimes, we'll want to apply some function to the primitive data items in 
%JL%the structure.  Here's a function that uses a second function "square" to 
define a "list (num)" whose elements are the squares of another "list (num)":











%JR%Every time we write a function to process every element of a list, we'll 
%JL%write something almost identical to "squarelist".  Here's a function to 
define a list of factorials:












%JR%"factlist" has exactly the same 'shape' as "squarelist", it just applies 
%JL%"fact" instead of "square" and then applies itself recursively.  Values that 
%JR%differ between applications are usually supplied as actual parameters. Hope 
%JL%treats functions as data objects, so we can do this in a perfectly natural 
%JR%way.  A function that can take another function as an actual parameter is 
%JL%called a %H4%higher%H4%-%H4%order function%H4%.  When we declare it we must give the type of 
%JR%formal parameter standing for the function in the usual way.  The declaration 
of "fact" tells us that it's:


%P0%
%JR%Read this as 'a function mapping numbers to numbers'.  Now let's see how we 
%JL%can use this idea to write "factlist" and "squarelist" as a single higher- 
%JR%order function.  The new function needs two parameters, the original list, 
and the function that's applied inside it.  Its declaration will be:





%JR%The 'shape' of "alllist" will be the same as "factlist" and "squarelist", but 
%JL%the function we apply to each element of the list will be the formal 
parameter:






We use "alllist" like this:










%JR%Notice that there's no argument list after "square" or "fact" in the 
%JL%application of "alllist", so this construction won't be confused with 
%JR%functional composition.  "fact( 3 )" represents a function application, but 
"fact" by itself represents the unevaluated function.


%JR%Higher-order functions can also be polymorphic.  We can use this idea to 
%JL%write a more powerful version of "alllist" that will apply an arbitrary 
%JR%function to every element of a list of objects of arbitrary type.  This 
version of the function is usually known as "map":








%JR%The definition now uses two type variables "alpha" and "beta".  Each one 
%JL%represents the same actual type throughout one instance of "map", but the two 
%JR%types can be different.  This means we can use any function that maps alphas 
to betas to generate a list of betas from any list of alphas.
%P0%
%JR%The actual types aren't restricted to scalars, which makes "map" rather more 
%JL%powerful than we might realise at first sight.  Suppose we've got a suitably 
polymorphic function that finds the length of a list:












%JR%We can use "map" to apply "length" to every element of a list of words 
defined by "wordlist":






%JR%In this example "alpha" is taken to be a "list ( char )" and "beta" to be a 
%JL%num, so the type of the function must be "( list ( char ) -> num )". "length" 
fits the bill if "gamma" is taken to be a character.
%P0%
%C%%H2%Common patterns of recursion%H2%

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







%JR%The underlying pattern consists of processing each element in the list and 
%JL%accumulating a %H4%single%H4% value that forms the result.  In "sum", each element 
%JR%contributes its value to the final result.  In "length" the contribution is 
%JL%always "1" irrespective of the type or value of the element, but the pattern 
is identical.  Functions that display this pattern are of type:





%JR%In the function definition, the equation for a non-empty list parameter will 
%JL%specify an operation whose result is a "beta".  This is "+" in the case of 
%JR%"length" and "sum".  One argument of the operation will be a list element and 
%JL%the other will be defined by a recursive call, so the type of the operation 
needs to be:





%JR%This operation differs between applications, so it will be supplied as a 
%JL%parameter.  Finally we need a parameter of type "beta" to specify the base 
%JR%case result.  The final version of the function is usually known as "reduce".  
%JL%In the following definition, the symbol "!" introduces a comment, which 
finishes with another "!" or with a newline:








%P0%
%JR%To use "reduce" as a replacement for "sum" we'll need to supply the standard 
%JL%function "+" as an actual parameter.  We can do this if we prefix it with the 
%JR%symbol %H2%nonop%H2% to tell the compiler we don't want to use it as an infix 
operator:






%JR%When we use "reduce" as a replacement for "length", we're not interested in 
%JL%the first argument of the reduction operation because we always add "1" 
whatever the list element is.  This function ignores its first argument:






We use "_" to represent any argument we don't want to refer to.






%JR%Like "map", "reduce" is much more powerful than it first appears because the 
%JL%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:







%P0%
%JR%Actually this isn't strictly polymorphic as its declaration suggests, because 
%JL%it uses the built-in function "<", which is only defined over numbers and 
%JR%characters, but it shows the kind of thing we can do.  When we use it to 
reduce a list of characters:






%JR%we can see that it actually sorts them.  The sorting method (insertion sort) 
%JL%isn't very efficient, but the example shows something of the power of 
%JR%higher-order functions and of "reduce" in particular.  It's even possible to 
%JL%use "reduce" to get the effect of "map", but that's left as an exercise for 
the reader as they say.


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













%JR%We can use this kind of tree to define a more efficient sort.  An %H4%ordered%H4% 
%JL%binary tree has the property that all the objects in its left subtree 
%JR%logically precede the node object and all those in its right subtree are 
%JL%equal to the node object or logically succeed it.  We can build an ordered 
%JR%tree if we have a function to insert new objects into an already-ordered 
tree, such as:








%P0%
%JR%We can sort a list by converting its elements into an ordered tree using 
%JL%"instree", then flattening the tree back into a list.  This is very easy to 
specify using the two kinds of reduction we've defined:














%C%%H2%Anonymous functions%H2%

%JR%When we used "map" and "reduce", we had to define extra functions like "fact" 
%JL%and "square" to pass in as paramteters.  This is a nuisance if we don't need 
%JR%them anywhere else in the program and especially if they're trivial, like 
%JL%"sum" or "addone".  For on-the-spot use in cases like this, we can use an 
%JR%anonymous function called a %H4%lambda%H4%-%H4%expression%H4%.  Here's a lambda-expression 
corresponding to "sum":





%JR%The symbol "%H2%lambda%H2%" introduces the function and  "x" and "y" are its formal 
%JL%parameters.  The expression "x + y" is the function definition.  The part 
%JR%after "%H2%lambda%H2%" is just a recursion equation without the "---" and with "=>" 
%JL%instead of "<=".  Here's another lambda-expression used as the actual 
parameter of "reduce":






%JR%There can be more than one recursion equation in the lambda- expression.  
%JL%They're separated from each other by the symbol "|" and pattern-matching is 
%JR%used to select the appropriate one.  Here's an example that uses 
%JL%pattern-matching in a lambda-expression to avoid division by zero when the 
function it defines is executed:





%P0%
%C%%H2%Functions that create new functions%H2%

%JR%As we've seen, Hope functions possess 'full rights' and can be passed as 
%JL%actual parameters like any data object.  It'll be no surprise to learn that 
%JR%we can return a function as the %H4%%H4%result%H4%%H4% of another function.  The result can 
%JL%be a named function or an anonymous function defined by a lambda-expression.  
Here's a simple example:










%JR%As we can see from trying "makestep", its result is an anonymous function 
%JL%that adds a fixed quantity to its single argument.  The size of the increment 
%JR%was specified as an actual parameter to "makestep" when the new function was 
%JL%created, and has become 'bound in' to its definition.  If we try the new 
function, we'll see that it really does add "3" to its actual parameter:






%JR%There are %H4%two%H4% applications here.  First we apply "makestep" to "3", then the 
%JL%resulting anonymous function is applied to "10".  Finally, here's a function 
that has functions as both actual parameter and result:






%JR%"twice" defines a new function that has a single argument and some other 
%JL%function "f" bound into its definition.  The new function has the same type 
as "f".  We can see its effect using a simple function like "square":







%P0%
%JR%The new function applies the bound-in function to its argument twice.  We can 
%JL%even bind in "twice" itself, generating a new function that behaves like 
%JR%"twice" except that the function eventually bound in will be applied four 
times:








%P0%
%C%%H2%In conclusion%H2%

%JR%In this article you've been introduced to the ideas of functional programming 
%JL%through one of the new generation of functional languages.  You saw how a 
%JR%Hope program is just a series of functions that are regarded as definitions 
%JL%of parts of a data structure - the 'results' of the program - and how the 
%JR%powerful idea of higher-order functions allows us to capture many common 
program patterns in a single function.


%JR%Some of these ideas will already be familiar to users of LISP, but they 
%JL%appear in a purer form in Hope, because there are no mechanisms for updating 
%JR%data structures like LISP's SETQ and RPLACA or for specifying the order of 
%JL%evaluation like GO and PROG.  Unlike LISP programs, Hope programs are free 
%JR%from side-effects and possess the mathematical property of %H4%referential 
transparency%H4%.


%JR%You also saw features that are primitive or lacking in LISP and in most 
%JL%imperative languages.  The %H2%data%H2% declaration lets you define complex data 
%JR%types without worrying about how they're represented and pattern- matching 
%JL%lets you decompose them, so you can use abstract data types directly without 
%JR%writing access procedures and without the need to invent lots of new names.  
%JL%The typing mechanism lets the compiler check that you're using data objects 
%JR%in a correct and consistent way, while the idea of polymorphic types stops 
%JL%the checking from being too restrictive and lets you define common data 
'shapes' with a single function.


%JR%Higher-order functions and polymorphic types allow us to write programs that 
%JL%are very concise.  Programmers are more productive and their programs are 
%JR%easier to understand and to reason about.  The property of referential 
%JL%transparency improves our ability to reason about programs still further and 
%JR%makes it possible to transform them mechanically into programs that are still 
%JL%provably correct, but more efficient in their use of space or time.  Finally, 
%JR%referential transparency keeps the meaning of Hope programs independent of 
%JL%the order they're evaluated in, making them ideal for parallel evaluation on 
%JR%suitable machines.  You'll be seeing a lot more of Hope and languages like it 
in the future.
%CO:B,12,73%

















sqrt ( x )



writeln ( 1.0 + sqrt ( x ) ) ; 












%H2%function%H2% max ( x, y : INTEGER ) : INTEGER ;
%H2%begin%H2%
%H2%if%H2% x > y
   %H2%then%H2% max := x
   %H2%else%H2% max := y
%H2%end%H2% ;









writeln ( max ( z, 0 ) ) ;






max ( a, max ( b, c ) )














%H2%function%H2% MaxOf3 ( x, y, z : INTEGER ) : INTEGER ;
%H2%begin%H2%
  MaxOf3 := max ( x, max ( y, z ) )
%H2%end%H2% ;





MaxOf3 ( a, b, c )











































%H2%dec%H2% max : num # num -> num ;
























--- max ( x, y ) <=  %H2%if%H2% x > y %H2%then%H2% x %H2%else%H2% y ;







































max ( 10, 20 ) + max ( 1, max ( 2,3 ) ) ;
%H4%23 : num%H4%










%H2%dec%H2% MaxOf3 : num # num # num -> num ;
--- MaxOf3 ( x, y, z ) <= max ( x, max ( y, z ) ) ;













%H2%function%H2% mult ( x, y : INTEGER ) : INTEGER ;
%H2%var%H2% prod  : INTEGER ;

%H2%begin%H2%
  prod := 0 ;
  %H2%while%H2% y > 0 %H2%do%H2% 
    %H2%begin%H2%
 prod := prod + x ;
 y := y - 1
    %H2%end%H2% ;
  mult := prod
%H2%end%H2% ;














%H2%dec%H2% mult : num # num -> num ;
--- mult ( x, y ) <= 0 + x + x + ...








mult ( x, y )        and       mult ( x, y-1 ) + x







--- mult ( x, y ) <= mult ( x, y-1 ) + x ;










--- mult ( x, y ) <= %H2%if%H2% y = 0 %H2%then%H2% 0 %H2%else%H2% mult ( x, y-1 ) + x ;
















%H2%infix%H2% mult : 8 ;
%H2%dec%H2% mult : num # num -> num ;
--- x mult y <= %H2%if%H2% y = 0 %H2%then%H2% 0 %H2%else%H2% x mult ( y - 1 ) + x ;



































( 2, 3 )       or        ( 'a', true )







%H2%dec%H2% time24 : num -> num # num # num ;
--- time24 ( s ) <= ( s div 3600,
                 s mod 3600 div 60,
                 s mod 3600 mod 60  ) ;








time24 ( 45756 ) ;
%H4%( 12,42,36 ) : ( num # num # num )%H4%







[ 1, 2, 3 ]







10 :: [ 20, 30, 40 ]





[ 10, 20, 30, 40 ]













[ a + 1, b - 2, c * d ]





a + 1 :: ( b - 2 :: ( c * d :: nil ) )






"cat"        [ 'c', 'a', 't' ]        'c' :: ( 'a' :: ( 't' :: nil ) )
























%H2%for%H2% i := n %H2%downto%H2% 1 %H2%do%H2% write ( i ) ;






%H2%dec%H2% nats : num -> list ( num ) ;
--- nats ( n ) <= %H2%if%H2% n = 0 %H2%then%H2% nil %H2%else%H2% n :: nats ( n-1 ) ;






nats ( 10 ) ;
%H4%[ 10,9,8,7,6,5,4,3,2,1 ] : list ( num )%H4%














...  %H2%else%H2% nats ( n-1 ) :: n ;







--- nats ( n ) <= %H2%if%H2% n = 0 %H2%then%H2% nil %H2%else%H2% nats ( n-1 ) <> [ n ] ;


















%H2%dec%H2% sumlist : list ( num ) -> num ;







--- sumlist ( x :: y ) ...







sumlist ( [ 1, 2, 3 ] )






--- sumlist ( x :: y ) <= x + sumlist ( y ) ;








sumlist ( nil ) 







--- sumlist ( nil ) <= 0 ;


























%H2%infix%H2% cat : 4 ;
%H2%dec%H2% cat : list( num ) # list( num ) -> list ( num ) ;
--- ( h :: t ) cat l <= h :: ( t cat l ) ;
--- nil cat l <= l ;
























mult x, y





( mult ( x ), y )




--- mult ( x, y ) <= ...















%H2%infix%H2% mult : 8 ;
%H2%dec%H2% mult : num # num -> num ;
--- x mult 0          <= 0 ;
--- x mult succ ( y ) <= ( x mult y ) + x ;












writeln ( ( x + y ) * ( x + y ) ) ;





z := x + y ; writeln ( z * z ) ;







%H2%let%H2% z == x + y %H2%in%H2% z * z ;







%H2%let%H2% z == z + 1 %H2%in%H2% z * z ;










z * z %H2%where%H2% z == x + y ;











%H2%dec%H2% time12 : num -> num # num ;
--- time12 ( s ) <= ( %H2%if%H2% h > 12 %H2%then%H2% h-12 %H2%else%H2% h, m ) %H2%where%H2%
               ( h, m, s ) == time24 ( s ) ;














%H2%dec%H2% firsttry : list ( char ) -> list ( char ) ;
--- firsttry ( nil )    <= nil ;
--- firsttry ( c :: s ) <= %H2%if%H2% c = ' '
                        %H2%then%H2% nil
                        %H2%else%H2% c :: firsttry ( s ) ;







firsttry ( "You may hunt it with forks and Hope" ) ;
%H4%"You" : list ( char )%H4%








%H2%dec%H2% firstword : list ( char ) -> list ( char ) # list ( char ) ;
--- firstword ( nil )    <= ( nil, nil ) ;
--- firstword ( c :: s ) <= %H2%if%H2% c = ' '
                         %H2%then%H2% ( nil, s )
                         %H2%else%H2% ( ( c :: w, r ) %H2%where%H2% 
                                ( w, r ) == firstword ( s ) ) ;







firstword ( "Hope springs eternal ..." ) ;
%H4%( "Hope","springs eternal ..." ) : ( list ( char ) # list ( char ) )%H4%






%H2%dec%H2% wordlist : list ( char ) -> list ( list ( char ) ) ;
--- wordlist ( nil )    <= nil ;
--- wordlist ( c :: s ) <= %H2%if%H2% c = ' '
                        %H2%then%H2% wordlist( s )
                        %H2%else%H2% ( w :: wordlist ( r )%H2% where%H2% 
                             ( w, r ) == firstword ( c :: s ) ) ;





wordlist ( "  While there's life there's Hope  " ) ;
%H4%[ "While","there's","life","there's","Hope" ] : list ( list ( char ) )%H4%



















































%H2%typevar%H2% alpha ;
%H2%infix%H2% cat : 8 ;
%H2%dec%H2% cat : list ( alpha ) # list ( alpha ) -> list ( alpha ) ;








[ 1,2,3 ]  cat  [ 4,5,6 ]         and         "123"  cat  "456"






[ 1,2,3 ]  cat  "456"

























%H2%data%H2% vague == yes ++ no ++ maybe ;








%H2%dec%H2% evade : vague -> vague ;
--- evade ( yes )   <= maybe ;
--- evade ( maybe ) <= no ;








%H2%data%H2% tree == empty ++ tip ( num ) ++ node ( tree # tree ) ;






















%H2%dec%H2% sumtree : tree -> num ;
--- sumtree ( empty )         <= 0 ;
--- sumtree ( tip ( n ) )     <= n ;
--- sumtree ( node ( l, r ) ) <= sumtree ( l ) + sumtree ( r ) ;








sumtree ( node ( node ( tip ( 1 ),
                   node ( tip ( 2 ),
                          tip ( 3 ) ) ),
            node ( node ( empty,
                          tip ( 4 ) ),
                   tip ( 5 ) ) ) ) ;

























%H2%data%H2% tree ( alpha ) == empty ++
                  tip ( alpha ) ++
                  node ( tree ( alpha ) # tree ( alpha ) ) ;












%H2%dec%H2% flatten : tree ( alpha ) -> list ( alpha ) ;
--- flatten ( empty )         <= nil ;
--- flatten ( tip ( x ) )     <= x :: nil ;
--- flatten ( node ( x, y ) ) <= flatten ( x ) <> flatten ( y ) ;




flatten( node ( tip ( 1 ), node ( tip ( 2 ), tip ( 3 ) ) ) ) ;
%H4%[ 1, 2, 3 ] : list ( num )%H4%


flatten( node ( tip ( "one" ),
           node ( tip ( "two" ),
                  tip ( "three" ) ) ) ) ;
%H4%[ "one","two","three" ] : list ( list ( char ) )%H4%


flatten( node ( tip ( tip ( 'a' ) ),
           node ( tip ( empty ),
                  tip ( node ( tip ( 'c' ),
                               empty ) ) ) ) ) ;
%H4%[ tip ( 'a' ),empty,node ( tip ( 'c' ), empty) ] : list ( tree ( char ) )%H4%





















%H2%dec%H2% square : num -> num ;
--- square ( n ) <= n * n ;


%H2%dec%H2% squarelist : list ( num ) -> list ( num ) ;
--- squarelist ( nil )    <= nil ;
--- squarelist ( n :: l ) <= square ( n ) :: squarelist ( l ) ;







%H2%dec%H2% fact : num -> num ;
--- fact ( 0 )          <= 1 ;
--- fact ( succ ( n ) ) <= succ ( n ) * fact ( n ) ;


%H2%dec%H2% factlist : list ( num ) -> list ( num ) ;
--- factlist ( nil )    <= nil ;
--- factlist ( n :: l ) <= fact ( n ) :: factlist ( l ) ;











num -> num







%H2%dec%H2% alllist : list ( num ) # ( num -> num ) -> list ( num ) ;







--- alllist ( nil, f )    <= nil ;
--- alllist ( n :: l, f ) <= f ( n ) :: alllist ( l, f ) ;





alllist ( [ 2,4,6 ], square ) ;
%H4%[ 4,16,36 ] : list ( num )%H4%


alllist ( [ 2,4,6 ], fact ) ;
%H4%[ 2,24,720 ] : list ( num )%H4%














%H2%typevar%H2% alpha, beta ;
%H2%dec%H2% map : list ( alpha ) # ( alpha -> beta ) -> list ( beta ) ;
--- map ( nil, f ) <= nil ;
--- map ( n :: l, f ) <= f ( n ) :: map ( l, f ) ;












%H2%typevar%H2% gamma ;
%H2%dec%H2% length : list ( gamma ) -> num ;
--- length ( nil )    <= 0 ;
--- length ( n :: l ) <= 1 + length ( l ) ;


length ( [ 2,4,6,8 ] ) + length ( "cat" ) ;
%H4%7 : num%H4%






map ( wordlist ( "The form remains, the function never dies" ), length ) ;
%H4%[ 3,4,8,3,8,5,4 ] : list ( num ) ;%H4%













%H2%dec%H2% sum : list ( num ) -> num ;
--- sum ( nil )    <= 0 ;
--- sum ( n :: l ) <= n + sum ( l ) ;









( list ( alpha ) -> beta )









( alpha # beta -> beta )









%H2%dec%H2% 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 ) ) ;







reduce ( [ 1,2,3 ], nonop +, 0 ) ;
%H4%6 : num%H4%







%H2%dec%H2% addone : alpha # num -> num ;
--- addone ( _ , n ) <= n + 1 ;





reduce ( "a map they could all understand", addone, 0 ) ;
%H4%31 : num%H4%







%H2%dec%H2% insert : alpha # list ( alpha ) -> list ( alpha ) ;
--- insert ( i, nil )    <= i :: nil ;
--- insert ( i, h :: t ) <= %H2%if%H2% i < h
                         %H2%then%H2% i :: ( h :: t )
                         %H2%else%H2% h :: insert ( i, t ) ;







reduce ( "All sorts and conditions of men", insert, nil ) ;
%H4%"     Aacddefiillmnnnnoooorssstt" : list ( char )%H4%

















%H2%data%H2% tree ( alpha ) == empty ++
                  node ( tree ( alpha ) # alpha # tree ( alpha ) ) ;

%H2%dec%H2% 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 ) ) ) ;










%H2%dec%H2% instree : alpha # tree ( alpha ) -> tree ( alpha ) ;
--- instree ( i, empty ) <= node ( empty, i, empty ) ;
--- instree ( i, node ( l, v, r ) ) <=
         %H2%if%H2% i < v
          %H2%then%H2% node ( instree ( i, l ), v, r )
          %H2%else%H2% node ( l, v, instree ( i, r ) ) ;






%H2%dec%H2% sort : list ( alpha ) -> list ( alpha ) ;
--- sort ( l ) <= redtree( reduce ( l, instree, empty ), nonop ::, nil ) ;


sort ( "Mad dogs and Englishmen" ) ;
%H4%"   EMaadddegghilmnnnoss" : list ( char )%H4%
















%H2%lambda%H2% ( x, y ) => x + y









reduce ( [ "toe","tac","tic" ], %H2%lambda%H2% ( a, b ) => b <> a, nil ) ;
%H4%"tictactoe" : list ( char )%H4%









map ( [ 1,0,2,0,3 ], %H2%lambda%H2% ( 0 )          => 0
                     %H2%|%H2% ( succ ( n ) ) => 100 div succ ( n ) ) ;
%H4%[ 100,0,50,0,33 ] : list ( num )%H4%










%H2%dec%H2% makestep : num -> ( num -> num ) ;
--- makestep ( i ) <= lambda ( x ) => i + x ;


makestep ( 3 ) ;
%H4%lambda ( x ) => 3 + x : num -> num%H4%









makestep ( 3 ) ( 10 ) ;
%H4%13 : num%H4%







%H2%dec%H2% twice : ( alpha -> alpha ) -> ( alpha -> alpha ) ;
--- twice ( f ) <= lambda ( x ) => f ( f ( x ) ) ;







twice ( square ) ;
%H4%lambda ( x ) => square( square ( x ) ) : num -> num%H4%

twice ( square ) ( 3 ) ;
%H4%81 : num%H4%







twice ( twice ) ;
%H4%lambda ( x ) => twice ( twice ( x ) )%H4%
%H4%: ( alpha -> alpha ) -> ( alpha -> alpha )%H4%

twice ( twice ) ( square ) ( 3 ) ;
%H4%43046721 : num%H4%
%CO:C,12,61%%CO:D,12,49%%CO:E,12,37%%CO:F,12,25%%CO:G,12,0%