7.2 Alternate Higher-Order Function Notation 119
apply ran to is a function that accepts the elements of S as its inputs and evaluates
to the same value as
f. Such a function can be defined as:
<(x::S)::ret(f) is f(x)>
This function’s domain is the set S used as one parameter to image.Itsvalueisf
evaluated on its input. To define image we simply call ran on the result:
image(f,S) == ran(<(x::S)::ret(f) is f(x)>)
7.2 Alternate Higher-Order Function Notation
The functions dom, ran, and ret are defined to return elements of a function
definition. Thus, it is natural to call these functions using functions as parameters.
When thinking about image and mapping functions, Iminimum, maximum, and
quantifier functions, the common practice is to start with a set of items and per-
form a specified operation on that set. Mapping functions apply a transformation
to each element of a set, minimum and maximum return the appropriate value
from a set, and quantifiers check to see if a property holds for all or some values
from a set. Although each of these properties can be expressed using a higher-
order function, it can become difficult to read and understand.
Rosetta introduces a standard notation to allow a more natural expression of
higher-order properties involved in quantification associated w ith sets. The fol-
lowing notation is equivalent to finding the minimum value generated by
inc in
the earlier example:
min(x::natural | x+1)
Using this notation, the domain and value expression of the function are sep-
arated in a manner consistent with traditional notations. The interpretation of
this notation is to take all elements of
natural, apply the expression x+1, and
return the minimum resulting value. The mapping from this notation back to
the higher-order function is a simple syntactic manipulation. If S is a
set and
e is an expression defined over elements of S , then the following relationship is
always true:
min(x::S | e)
defs
min(<(x::S)::T
is e >)
Here the elements of the set are pulled out and used as a type in the function
former. The notation:
min(x :: natural | x)
specifies the minimum value in the set of natural numbers.
What makes this notation powerful is that
natural can be replaced by any set
and Rosetta forms the higher-order function. If the collection can be identified
and the expression defined, the preceding notation can be used to accomplish

Get System Level Design with Rosetta now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.