The Hope compiler can spot many common kinds of error by checking the types of all objects in expressions. This is harder than checking at run-time, but more efficient and saves the embarrassment of discovering an error at run-time in a rarely-executed branch of the air traffic control system we just wrote.
However, strict type-checking can be a nuisance if we want to perform some operation that doesn't depend on the type of the data. Try writing a Pascal procedure to reverse an array of either 10 integers or 10 characters and you'll see what I mean.
Hope avoids this kind of restriction by allowing a function to operate on more than one type of object. We've already used the standard constructors :: and nil to define a list ( num ), a list ( char ) and a list ( list ( char ) ). The standard equality function = will compare any two objects of the same type. Functions with this property are called polymorphic. Pascal's built-in functions abs and sqr and operations like > and = are polymorphic in a primitive kind of way.
We can define our own polymorphic functions in Hope. The function cat we defined above will concatenate lists of numbers, but we can use it for lists containing any type of object. To do this we first declare a kind of `universal type' called a type variable. We use this in the declaration of cat where it stands for any actual type:
typevar alpha ;
infix cat : 8 ;
dec cat : list ( alpha ) # list ( alpha ) -> list ( alpha ) ;
This says that cat has two parameters that are lists and defines a list,
but it doesn't say what kind of object is in the list. However, alpha
always stands for the same type throughout a given declaration, so all the
lists must contain the same type of object. The expressions:
[ 1,2,3 ] cat [ 4,5,6 ]
and
"123" cat "456"
are correctly-typed applications of cat and define a list ( num ) and a
list ( char ) respectively, while the expression:
[ 1,2,3 ] cat "456"
isn't because alpha can't be interpreted as two different types. The
interpretation of a type variable is local to a declaration so it can have
different interpretations in other declarations without confusion.
Of course it only makes sense for a function to be polymorphic as long as the equations defining it don't make any assumptions about types. In the case of cat the definition uses only :: and nil, which are polymorphic themselves. However, a function like sumlist uses + and can only be used with lists of numbers as parameters.