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 deﬁned 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 deﬁne 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 deﬁned to return elements of a function
deﬁnition. Thus, it is natural to call these functions using functions as parameters.
When thinking about image and mapping functions, Iminimum, maximum, and
quantiﬁer functions, the common practice is to start with a set of items and per-
form a speciﬁed 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 quantiﬁers 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 difﬁcult to read and understand.
Rosetta introduces a standard notation to allow a more natural expression of
higher-order properties involved in quantiﬁcation associated w ith sets. The fol-
lowing notation is equivalent to ﬁnding 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 deﬁned 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)
speciﬁes 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 identiﬁed
and the expression deﬁned, 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.