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.