Rosetta defines several type categories that include elemental, composite, function, constructed, and facet types. The first of these categories, the elemental types, defines types as collections of atomic values. Element literals provide a mechanism for specifying element values in a specification. All elemental types are subtypes of the element
type and include numbers, boolean values and characters, infinite values, and the the bottom
value.
The number
type is the supertype of all definable number values. Subtypes of number
include complex
, real
, integer
, natural
, and bit
as well as specific subtypes to aid in constraining number values further for specification purposes. Number literals provide a mechanism for specifying number values in specifications.
The boolean
type defines the two literal Boolean values true
and false
along with the traditional Boolean operations. Distinct from the bit
type, the boolean
type provides an abstract means for specifying logical sentences and for specifying conditional properties.
The character
type defines a mechanism for specifying and manipulating Unicode values. Unicode is used throughout Rosetta to promote readable specifications and use of international character sets. The character
literals provide a mechanism for defining Unicode values in a specification. The character
type provides operations similar to those used in ASCII and Unicode character systems, allowing characters to be used in traditional ways.
Rosetta provides a Boolean type consisting of the values true
and false
denoted by the type boolean
. The notation:
b::boolean;
declares a new item, b
, of type boolean
. Operations provided over boolean provide a mechanism for specifying propositional statements in a traditional manner. Table 4.1 defines the collection of operations defined over all boolean
items.
Table 4.1. Operations defined over the boolean
type
Operator | Syntax | Result Type |
---|---|---|
Logical negation |
|
|
Logical conjunction and disjunction |
|
|
Logical nand and nor |
|
|
Logic al exclusive or and nor |
|
|
Logical implication |
|
|
Boolean to bit |
|
The unary not
and binary and
and or
operators provide basic logical operations over boolean
items. Examples of their application include:
true and true == true false or false == false false or true == true false and true == false not false == true
The nand
, nor
, xor
, and xnor
operators provide compound logical functions and are constructed from the basic logical operations. Although not semantically necessary, they provide shorthand for more complex, standard operations. Some examples of their application and definition include:
A nand B == not(A and B) A nor B == not(A or B) A xor B == ((not A)and B)or ((not B)and A) A xnor B == (A and B)or ((not A)and (not B))
The various implication operators are also compound logical functions defined over disjunction. The logical implication operators, =>
and implies
, are equivalent and define logical implication. The implied by operator, <=
, is simply the inverse of the implies operation. Some examples of the application and definition of these operators are:
A implies B == not A or B A => B == A implies B B <= A == A implies B
The only operation on boolean
that does not return a boolean
is the boolean-to-bit operation. This operation facilitates moving easily between the two types. In Rosetta, the boolean
and bit
types are distinct, with boolean
having no association with numbers and bit
being a subtype of natural
(defined later). Examples of application of this operation include:
%true == 1 %false == 0 %1 == true %0 == false
In these examples, the boolean-to-bit operation is used as a bit-to-boolean operation. The same operator symbol is used for both conversions, allowing the definition:
%(%A) == A
When dealing with bottom
argument values, operators over boolean
are non-strict. If any argument to a boolean
operator is the value bottom
, but determining the value of the operator does not require evaluating bottom
, then the result is the prescribed value. Otherwise, the result is bottom
. Consider the following examples, where one argument is bottom
, yet the value of the operator can be determined:
false and bottom == false true or bottom == true false implies bottom == true
In other cases, both operands must be known to determine a value other than bottom
for the expression:
bottom and true == bottom bottom or false == bottom bottom xor false == bottom bottom xor true == bottom
A good rule of thumb is that if the operator can be evaluated without evaluating bottom
, then it will evaluate to the appropriate value.
Rosetta provides a wide collection of numeric types specifying sets of values commonly used in system specification. Within the number types, subtypes are arranged hierarchically, with each subtype inheriting operations from its supertype. The number
type is the supertype of all number types. Each subtype adds new operations in addition to supporting operations from its supertype.
The complex
type is the most general of the traditional number types and is formed from real
and imaginary
numbers in the classical fashion. The real
type is further refined to define posreal
, negreal
, and integer
types. The integer
type is further refined to define posint
, negint
, and natural
. Finally, natural
is refined to define the bit
types used in traditional digital design.
The only elements of the number
type that are not also in complex
are the infinite values, infinity
and -infinity
. These values are used primarily for specifying values for integrals, differential equations, and limits. However, they are in all ways number values.
The type number
is the supertype of all Rosetta numbers and a subtype of element
. The number
type is used heavily in the definition of other types, providing a collection of all numeric scalars. Specifiers use the number
type to indicate that an item is simply a number. Given the declaration:
n :: number;
little can be inferred about the possible values of n
except that they will be some number type.
The number
type is useful when working on abstract specifications where an item type should be restricted to be a number, but with no other constraints. Although the complex
type contains virtually all useful numbers, using complex
can indicate that the specification in question must actually implement mechanisms for handling complex numbers.
Complex numbers are a direct subtype of number
and are the most general number
subtype. Denoted by the name complex
, the set of complex numbers is constructed by adding real
values to imaginary
values in the same fashion as in traditional mathematics. The imaginary constant, j
, is provided for this purpose. Expressions such as 3.124+4*j
and inc(x)+sin(2x)*j
result in complex
values, as their syntax would suggest. Other mechanisms, such as exponentiation, that generate complex values are also allowed.
Example 4.1. Using the Number Type
A structural specification describes a system by describing the components and interconnections that implement it. More specifically, a structural specification describes an architecture for a system. The following structural specification shows high-level architecture implementing serial composition of facet definitions:
facet comp[T::type](m::input T; n::output T)::state_based; facet serial(x::input number; z::output number)::state_based is y::integer; begin a: comp(x,y); b: comp(y,z); end facet serial;
This specification defines a simple system, where component a
accepts an input and communicates with component b, which generates an output. Note that all inputs and outputs are type number
, but the interconnection item, y
, is an integer
. The facet comp
is instantiated twice to represent the two components, but little is specified about comp other than its interface. Its interface uses polymorphic typing to allow any type to be communicated through the component, but the output type must be the same as the input type. When the components are instantiated with y
, the type of their inputs and outputs is integer
. Because the input to the component is specified as number
, a more general type than integer
, the serial component accepts a set of inputs larger than the component instantiating it. Thus, the specification will not type check properly. This problem is easily fixed by changing the interconnect variable type to integer
or by making the serial architecture more general by allowing arbitrary types.
Operators defined over complex
values are shown in Table 4.2 and include negation, sum and difference, multiplication and division, and exponentiation. The unary negation operator changes the sign of its argument while the unary identity operator returns its argument value. Examples of their application include:
-(3.0+4.0*j) == -3.0-4.0*j +(3.0+4.0*j) == 3.0+4.0*j
Table 4.2. Operators over the complex type
Operation | Syntax | Result Type |
---|---|---|
Negation and Identity |
|
|
Sum and Difference |
|
|
Product and Quotient |
|
|
Exponentiation |
|
|
The binary sum and difference operators are defined as traditional addition and subtraction of complex values. Examples of their application include:
(3.0+4.0*j) + (1.0-1.0*j) == 4.0+3.0*j (3.0+4.0*j) - (1.0-1.0*j) == 2.0+5.0*j
Similarly, binary product and quotient operators are defined as traditional multiplication and division of complex numbers. Examples of their application include:
(2.0+2.0*j) * (1.0+4.0*j) == (2.0+10.0*j-8.0) == 6.0+10.0*j (2.0+2.0*j) / (1.0+4.0*j) == (2.0+ 2.5*j-0.5) == 1.5+2.5*j
Because the sum and difference operators used in forming complex
values are the same sum and difference operators used elsewhere, care must be taken to parenthesize complex values so that their formation takes higher precedence, compared to the operations performed on them. Removing parentheses in the previous examples has very different results.
The range of all operations defined on complex
is also complex
. This implies that operations are closed over complex
and that their ranges cannot be restricted beyond complex
. Functions, such as real projection or complex conjugate, can be restricted beyond complex
and are presented subsequently.
In addition to unary and binary operators, a collection of predefined functions over complex
are defined in Table 4.3. Unary functions for finding the real part, complex part, absolute value, argument, and complex conjugate all return real, a subtype of complex
. The argument function’s return value is in radians, as are all Rosetta functions dealing with angles. Some examples of the application of these functions include:
re(2.1-1.5*j) == 2.1 im(2.1-1.5*j) == -1.5 arg(2.1-1.5*j) == 0.9505 abs(2.1-1.5*j) == 2.587 conj(2.1-1.5*j) == 2.1+1.5*j
Table 4.3. Functions over the complex type
Function | Syntax | Result Type |
---|---|---|
Real and Imaginary parts |
|
|
Absolute value or modulus |
|
|
Argument or phase |
|
|
Complex conjugate |
|
|
Trigonometric functions |
|
|
| ||
| ||
Hyperbolic trig functions |
|
|
| ||
| ||
Exponential (base e) |
|
|
Square root |
|
|
Logarithms |
|
|
| ||
Floor and ceiling |
|
|
Truncation and rounding |
|
|
Signum |
|
|
Functions for finding the floor, ceiling, and rounding complex
values all return complex
values determined in the traditional fashion. Examples of the application of these functions include:
floor(2.1-1.5*j) == 2.0-1.0*j ceiling(2.1-1.5*j) == 3.0-2.0*j trunc(2.1-1.5*j) == 2.0-1.0*j round(2.1-1.5*j) == 2.0-2.0*j
The signum function over complex values returns a unit vector in the direction of the original value. In the following expression, sgn
returns a vector of length 1 in the direction of the original vector:
sgn(2.1-1.5*j) == 0.8137-0.5812*j
A complete set of trigonometric operations is defined over complex numbers. The operations include the basic trigonometric functions for sine, cosine, and tangent as well as the hyperbolic trigonometric functions and inverse functions. Example applications include:
sin(2.0+3.0*j) arcsin(2.0+3.0*j) sinh(2.0+3.0*j) arcsinh(2.0+3.0*j)
The sqrt
function is provided as a shorthand for x^(1/2)
. The language definition constrains sqrt(x)
value to one of the square roots of x
. The function should be constrained further when specific roots are desired. For example, the following two equivalences both satisfy the base definition for sqrt
:
sqrt(4.0) == 2.0 sqrt(4.0) == -2.0
The definition simply states that a square root function must return a legal root, not a specific legal root.
Similarly, a collection of logarithmic and exponentiation functions is defined that includes natural log, log base 10, log base 2, and exponentiation. Example applications include:
exp(2.0+3.0*j) log(2.0+3.0*j) log10(3.0+2.0*j) log2(3.0+2.0*j)
Log base 2 is rarely, if ever, used for complex numbers, but is defined for completeness and will be useful for many subtypes of complex
.
All trigonometric and logarithmic, functions are closed with respect to complex, the only exception being situations where operator forms are not allowed where their values are bottom
, indicating an error. Such situations include division by 0 and tangent of 1.0. Some examples of illegal expressions whose value is bottom
include:
3.0/0.0 == bottom tan(0.0) == bottom log(0.0) == bottom
Operators and functions defined for complex are strict. If any operand for a complex operator or function is bottom
, then the result of evaluating that function is bottom
. The implications of strictness are that if any operator is unknown or illegal, then the result of applying an operator or function is also undefined or illegal. This follows from the need to evaluate all arguments to mathematical operators and functions. This is in contrast to boolean
operators that can often be evaluated without evaluating every argument.
Both real and imaginary numbers are defined as subtypes of the complex numbers. Real numbers are the subtype of complex whose imaginary part is 0, while imaginary numbers are the subtype whose real part is 0. Real items are denoted using the type real, while imaginary numbers are denoted using the type imaginary and are typically formed by multiplying a real number by the imaginary root, j
. Table 4.4 lists predefined constants associated with real and imaginary types. The imaginary root is used to construct imaginary values from real values. The standard mathematical constant, pi
, has its canonical value, as does the exponential, e. Specifiers are free to design and package their own mathematical constants. However, these constants are provided by default in the base Rosetta modeling system.
Table 4.4. Predefined numeric constants
Constant | Syntax | Type |
---|---|---|
Imaginary root |
|
|
Pi |
|
|
Exponential root |
|
|
Table 4.5 defines operations available on real and imaginary numbers in addition to those provided for complex numbers. The min and max operations return the minimum and maximum values from their arguments, respectively. Examples of their application include:
2.14min
3.75 == 2.14 4.57*jmin
2.76*j = 2.76*j 2.14max
3.75 == 3.75 4.57*jmax
2.76*j = 4.57*j
Table 4.5. Additional operations on real and imaginary types
Operator | Syntax | Result Type |
---|---|---|
Minimum and maximum |
|
|
Ordering relations |
|
|
|
Min and max return types are the same as their associated argument types. If the arguments to either operation are imaginary, then the return type is imaginary, and similarly for real. Neither operator is defined for mixed imaginary and real values. For example, 4.75*j
max
2.76
is forbidden.
Ordering relations provide traditional ordering relationships between values. Examples of their application include:
2.14 < 3.75 == true 2.14 > 3.75 == false 2.14*j =< 2.14*j == true 2.14*j >= 3.75*j == false
All ordering relations are boolean and, like the min and max operations, are undefined if their arguments are not both real or imaginary. For example, 2.14*j < 3.75
is not allowed.
Subtype relationships imply that any real or imaginary value may be treated like a complex value. Any operator defined over complex values may be applied to combinations of real and imaginary operands, with the result treated as the same type defined for complex arguments. However, for many operators and functions, the return type is more restricted than is the entire complex type. By specifying those restricted types, static analysis tools such as type checkers can infer more detailed information about a specification. Thus, Rosetta defines the return types for operators and functions as the most restricted type that covers all possibilities.
Sum and difference operators are closed with respect to both real and imaginary. The sum or difference of two real or imaginary values is real or imaginary, respectively. If operands are of mixed type, sum and difference both result in a complex type. This should not be surprising, as the sum and difference operations are used to construct the complex type from real and imaginary. For example:
1.2::real + 2.4::real == 3.6::real (1.2*j)::imaginary + (2.4*j)::imaginary == (1.2*j)::imaginary (1.2*j)::imaginary + (2.4)::real == (2.4+(3.6*j))::complex
Product operations are closed over real
, but result in real
when applied to imaginary
and imaginary
when applied to mixed arguments. Again, this should not be surprising, as j*j
is equal to -1
. Examples include:
1.2::real * 2.0::real == 2.4::real (1.2*j)::imaginary * (2.0*j)::imaginary == -2.4::real 1.2::real * (2.0*j)::imaginary == (2.4*j)::imaginary
All operators and functions inherited from complex
remain strict. All operators defined for real
and imaginary
are strict. If any of their operands or arguments are bottom
, then they evaluate to bottom
. This again results from the need to evaluate every argument to evaluate a mathematical operator.
The posreal
and negreal
types are subtypes of real
that define the positive and negative real numbers, respectively. No additional operators are defined on either type, but the range of many operations on real
changes when considering positive or negative real numbers.
The negation operator becomes a conversion operator between the types. The negation of a posreal
results in a negreal
and the negation of a negreal
results in a posreal
. For example:
-2.354::negreal -(-2.354) == 2.354::posreal
The min
and max
operators can be further restricted. If either argument to the max
operator is a posreal
, then the result is a posreal
, while if either argument to the min
operator is a negreal
, the result is a negreal
. For example:
1.0::posrealmin
4.0::posreal == 1.0::posreal -1.0::negrealmin
4.0::posreal == -1.0::negreal -1.0::negrealmin
-4.0::negreal == -4.0::negreal 1.0::posreal max 4.0::posreal == 4.0::posreal -1.0::negreal max 4.0::posreal == 4.0::real -1.0::negreal max -4.0::negreal == -1.0::real
Sum and difference operators can both be thought of as sum operations by understanding the relation A-B == A+(-B)
. Both posreal
and negreal
are closed over addition. However, if sum is applied to mixed type operators, the result cannot be constrained beyond the real
type. For example:
3.0::posreal + 2.0::posreal == 5.0::posreal -3.0::negreal + -2.0::negreal == -5.0::negreal -3.0::negreal + 2.0::posreal == -1.0::real 3.0::posreal + -2.0::negreal == 1.0::real
Product and quotient operations follow the same rules. Every division operation can be expressed as a product operation, thus we can define the return type for product and apply the result to quotient. Product is closed over posreal
, while negreal
results in a posreal
. When operators are of mixed types, the result is always negreal
. For example:
1.2::posreal * 2.0::posreal == 2.4::posreal -1.2::negreal * 2.0::posreal == -2.4::negreal -1.2::negreal * -2.0::negreal == 2.4::real
Operators over real
inherited by posreal
and negreal
remain strict.
The integer
type is the subtype of real
that includes only integral values defined in the classical fashion. All operations defined over real
are defined over integer
. Three additional operations are listed in Table 4.6. The div
operator provides an integer division operation, while mod
and rem
provide a modulus and remainder operation, respectively. The distinction between remainder and modulus is subtle, frequently causing the operations to be confused. The modulus operator specifies the integer modulus of its left operand divided by its right operand and assumes the sign of its right operand. The remainder operator specifies the integer remainder of its left operand divided by its right operand and assumes the sign of its left operand. For example:
11 div 3 == 3 11 rem 3 == 2 11 mod -3 == -2
Table 4.6. New operations over integer type
Operator | Syntax | Return Type |
---|---|---|
Integer division |
|
|
Modulus |
|
|
Remainder |
|
|
All new operators and functions defined over integer
are strict.
Integer
operations inherited from real
obey similar closure rules. Negation, sum, and product operators over integer
are closed with the exception of division, which results in a real
. For example:
2::integer * 3::integer == 6::integer 2::integer / 3::integer == (2/3)::real 2::integer + 3::integer == 5::integer 2::integer - 3::integer == -1::integer
Rounding operations such as round
and trunc
, floor
and ceiling
produce integer
values for all real
values and are thus closed over integer
. However, with the exception of signum, such operators all reduce to the identity function.
The exponent operator and logarithmic operators are real
valued when applied to integer
. Although trigonometric functions are defined over integer
as asubtype of real
, they make little sense for discrete values.
Natural
is the subtype of integer
that includes only positive numbers and zero. The natural
type inherits all operators and functions from the integer
type, but introduces no new operations. Addition, multiplication, and exponentiation are both closed with respect to natural, as are div
, mod
, and rem
. Subtraction and division are of type integer
and real
, respectively. For example:
1::natural + 2::natural == 3::natural 2::natural * 2::natural == 4::natural 2::natural ^ 3::natural == 8::natural 7::natural div 2::natural == 3::natural 7::natural mod 2::natural == 1::natural 1::natural - 2::natural == -1::integer 1::natural / 2::natural == (1/2)::real
Rounding and truncating functions are all closed over natural
, as is the signum function. However, such functions are of limited use. Trigonometric and exponential functions are of type real
.
Posint
and negint
are subtypes of natural
and integer
, respectively. As their names imply, posint
is the set of natural numbers without 0 and negint
is the set of negative integers. Neither posint
nor negint
introduces new operations, but both inherit all operations from integer
. All operators and functions over natural
that are of natural
type are of posint
type when used over posint
. Other operators and functions are of the same type when applied to posint
as when applied to integer
. Some examples include:
-(1)::posint == -1::negint 1::posint + 2::posint == 3::posint 1::posint - 2::posint == -1::integer 2::posint * 3::posint == 6::posint 2::posint / 3::posint == (2/3)::real 2::posint ^ 3::posint == 8::posint 2::posint max 3::posint == 3::posint 2::posint min 3::posint == 2::posint
Operators and functions from integer
over negint
present a more complicated problem. Addition is the only operator closed with respect to negint
. Some examples include:
-(-1)::negint == 1::posint -1::negint + -2::negint == -3::negint -1::negint - -2::negint == 1::integer -2::negint * -3::negint == 6::posint -2::negint / -3::negint == (-2/-3)::real -2::negint ^ -3::negint == -(1/8)::posint -2::negint max -3::negint == -2::negint -2::negint min -3::negint == -3::negint
Bits are the subtype of natural numbers that includes only 1 and 0. Bit items are declared using the bit type and are used heavily in the specification of digital systems. Although all operators and functions defined on natural are also defined on bit, most specifiers use the Boolean functions introduced with the bit type. Table 4.7 lists new operators defined over the bit type. These operators parallel those specified for boolean; however, bit and boolean are distinct types. The %A
conversion operator is provided to convert between these types. Examples of the bit operators include:
not 1 == 0 1 and 0 == 0 1 or 0 == 1 1 xor 1 == 0 1 xnor 0 == 0 %1 == true %(%1) == 1
Table 4.7. New functions and operations defined over the bit type
Operator | Syntax | Return Type |
---|---|---|
Logical negation |
|
|
Conjunction and disjunction |
|
|
Negated operators |
|
|
Exclusive or operators |
|
|
Implication operators |
|
|
Like operations on boolean, operations defined for the bit type are non-strict. If arguments with values other than bottom
are sufficient to determine the value of an operator, then the operator evaluates to its value. Examples include:
0 and bottom == 0 1 or bottom == 1 0 implies bottom == 1
Other operations inherited from natural are not closed over bit. Thus, any operation on bit using these operators and functions is treated as an operation on natural.
The character
type is the collection of all UTF-32 values as defined in the Unicode Standard, Version 3.2 along with operations defined in Table 4.8. The ord
and char
functions move between the character
values and the natural
numbers. The ord
function accepts a character
value and specifies its associated Unicode value. The char
function is its inverse, taking a Unicode value and specifying its associated Unicode value. For example:
char(ord(c::character)) == c::character ord('a') == 16 061 ord('U+2132') == 162132
Table 4.8. Operators defined over the character type
Operator | Syntax | Return Type |
---|---|---|
Ordinal |
|
|
Character |
|
|
Relational Operations |
|
|
| ||
Capitalization |
|
|
Unicode constant former |
|
|
Character constant former |
|
|
The uc
and dc
functions change a character’s case to upper or lower case, respectively, when such a conversion is defined. When the upper and lower case distinction does not exist, these operations are identity functions. For example:
uc('a') == 'A' dc('A') == 'a' uc('1') == '1' dc('1') == '1'
Ordering functions defined over character are defined by mapping to their Unicode values and using ordering operators defined in natural
. A character is less than another if its associated Unicode value is less than the other’s Unicode value. For example, assuming that x
and y
are characters, x<y
and x=<y
are defined:
x < y == ord(x) < ord(y) x =< y == ord(x) =< ord(y)
Examples using ordering operations over character include:
'a' =< 'b' 'a' < 'b' 'b' >= 'b' 'b' > 'a'
All operations over character types are strict. If any operand to a character function is bottom
, then it is equal to bottom.
It is important to note that the character
and number
types are distinct. No subtype relationship exists between these types and neither inherits operators or functions from the other. Both inherit operators from the element type and its supertypes. Thus, statements such as 'c'<5
are not well defined statically because there is no less than function defined over character
and natural
. If an ordering relationship is defined over top
, that ordering relation will be used in the previous statement. No such ordering is defined in the base language.
Rosetta provides a supertype of all elemental types denoted as element
. The type element
consists of all values from boolean
, number
, and character
and contains all predefined, atomic Rosetta values. The element
type is rarely used in specifications, but plays an important role in the definition of other Rosetta types.
Rosetta introduces two types, top
and bottom
, that represent the supertype and subtype of all other types, respectively. The type top
consists of all Rosetta values and is a supertype of all other types. Formally, for any Rosetta type T
:
T =< top
Because Rosetta is reflective, this implies that top
contains not only traditional values such as numbers, characters, and sequences, but all possible types, functions, and facets. The following declaration defines a new x
that is of type top
:
x :: top
The top
type should rarely appear in specifications due to its generality. Nothing can be said about x
other than it must be a Rosetta value. Although this may seem advantageous at times, top
has the effect of removing all type information from anything it is associated with. What top
does provide is a mechanism for defining operations that apply to all Rosetta items, including Rosetta specifications themselves. If we define a function:
f(x:: top):: top;
it is defined over all Rosetta items. However, the declaration says nothing about the function’s resultant type. Any expression can be a legal formal parameter to f
, but nothing is known about its return value. Anytime top
is used in this way, all type information associated with the result of applying the function is lost. Care should be taken not to use top
to try and define polymorphic functions.
The bottom
type is a special type with a single value also called bottom
; this is used to indicate error results and divergent computations. It allows errors to be specified without violating type conditions. bottom
is the opposite of top
in that instead of being a supertype of all types, it is a subtype of all types. Formally, for any Rosetta type T
:
bottom =< T bottom in T
bottom
is inhabited by the single value bottom
used to represent the value of a divergent computation. Like top
, bottom
should rarely be used in specifications. However, it does play an important role in defining Rosetta semantics. For example, the function example
defines a function whose evaluation can result in bottom
:
example(x::real)::real is if not(x==0) then f(x) else bottom end if;
If the input parameter x
is ever 0
, then the function is defined to be bottom
, indicating an error condition. Because bottom
is a subtype of every type, the bottom
value always results in a type correct result.
Literals allow the user to write specific values in a Rosetta definition. Each elemental type has a mechanism for specifying literals. The number
type provides a simple syntax to support intuitive specification of integer, real, and complex values. In addition, a rich syntax is provided to specify numbers with arbitrary radix and exponentiation capabilities. The character
type provides a syntax for defining Unicode characters using character codes as well as simple literal characters for keyboard characters. The boolean
type provides the Boolean literals true
and false
for specifying propositional statements. Finally, the bottom literal bottom
provides a mechanism for denoting an undefined or error value.
Rosetta provides a mechanism for defining number literals in specifications that supports specifying numerical values ranging from simple decimal literals to exponential forms of numbers with arbitrary radix. The simplest number literals take the form of decimal digit strings with optional signs and a single decimal point. The following examples are all legal number literals of this form:
123 // Integer literal 12.3 // Real literal -123 // Negative integer literal -1.23 // Negative real literal
An exponent can be added to the literal value to specify the position of the radix point. The radix point position specifies the number of places the radix point should be moved to the left (negative point position) or right (positive point position). Expressing no radix position is the same as specifying the radix point as 0. The symbol e
is used to separate the radix position from the remainder of the number specification. The following examples show this literal notation:
1.23e5 == 123,000 // 1.23*105 1.23E-5 == 0.0000123 // 1.23*10-5 1.23e0 == 1.23 // 1.23*100
The most general form for number literals adds a radix, allowing specification of numbers in arbitrary bases up to 16. The radix is added to the front of a number literal and separated from the value using a backslash ("")
. When a radix is added, the radix point position must also be separated from the value using a backslash. Using this notation, number literals are specified using the form:
radix mantissa e pointposition
When a radix is specified, the mantissa becomes a sequence of based digits rather than decimal digits. To support bases up to base 16, the decimal digits are extended to include A-F
and a-f
in the classical manner. The radix point position is always specified in decimal regardless of the radix, and is optional. The backslash separating the radix point position from the mantissa is never optional if a radix is specified. The value 16234Ce4
is read “234C base 16 times 16 to the 4th power.” Some examples include:
105.2 // 5.2 in base 10 85.2 // 5.2 in base 8 16AABC // AABC in base 16 -105.2e-10 // –5.2*10–10 105.2e-10 // 5.2*10–10 165.2e-10 // 5.2*16– A base 16 -21 // –1 in binary -21e1 // –10 in binary
The backslash characters in a number literal are a part of its lexical structure and should not be viewed as operators: 105.2e-10
is a number literal and should be viewed in the same manner as 5.2e-10
. Thus, when a negation operator appears before literals of this form, it negates the entire value, not the radix value: -105.2e-10
is a negative value in the same manner as -5.2e-10
. The notation 10-5.2e-10
attempts to specify the negation as a part of the inner value, but is illegal in the notation. Although negations may appear in the radix point specification, the value must be unsigned.
In addition to values specified using the general form, three number constants are defined that can be used directly in specifications:
e // Exponential pi // Geometric pi j // Imaginary root
A number
literal may belong to several types. An extreme example of this is the literal 0
that belongs to every number
subtype. When a number literal appears in a specification, it assumes the most specific type from those of which it is a member. For example, the following literals are asserted to be of the specified type:
0::bit 1::bit 2::posint -2::integer 2.1::posreal -2.1::negreal (2.1+3.2*j)::complex
As we shall see later, this ensures that the appropriate type results when an operator is applied.
The literal infinity
and its negation -infinity
represent positive and negative infinite values. Although they are number values, they are not subtypes of any of the number
subtypes. Any mathematical operation defined thus far applied to infinite values will result in the number
type. Specifically:
1.3 + infinity == infinity::number 2 - infinity == -infinity::number
The infinite values are rarely used in this manner. The primary reason for their inclusion is with calculus functions such as limit and integral defined in the continuous time domain. There may be reasons to use infinite values in other kinds of specification, thus they are included in the number hierarchy.
To support specification across multiple languages and cultures, Rosetta uses the Unicode standard for character literals. The standard notation is 'U+XXXX'
or 'U-XXXX'
, where XXXX
is a hexadecimal constant specifying the associated Unicode character. The tick marks are a part of the specification syntax and are always used when specifying character literals. Examples of Unicode character specification include:
'U+00B1' // Plus/minus sign 'u+274f' // Lower right drop--shadowed white square 'U+10347' // Gothic letter IGGWS 'U+00FFFF' // Not a character 'U-0001040F' // Deseret capital letter yee
When the +
symbol delineates the Unicode value, the short character code is used. When -
is used, the full character code is specified.
Literal character values associated with keyboard symbols are specified using the notation 'x'
, where x
is the literal character. For example, 'E'
is the literal E
character, '@'
is the “at” character, ' '
is the space character. These characters may be specified using the Unicode notation. This specification form is provided for convenience and readability.
Unlike number
literals, character
has no define subtypes. Thus, all character
literals are simply of type character
:
'a'::character 'U+274f'::character 'U-0001040F'::character
The only two literals of type boolean
are the values true
and false
. Like character
, boolean
has no subtypes. Thus, all boolean
literals are simply of type boolean
:
true :: boolean false :: boolean
The undefined literal, called bottom and written as bottom
, specifies a value that has no definition and is illegal. In this chapter, whenever evaluating an expression results in something that is undefined, its value is bottom
. To facilitate using bottom
as an error specifier, we say that bottom
is an element of every type. Specifically, evaluating any expression, no matter what its type, may result in bottom
. The undefined literal is rarely used by specifiers. However, the language definition uses it heavily to denote undefined or illegal calculations.
Operations on number
, boolean
, and character
are defined with respect to operands and arguments of the same type. Addition, for example, is defined over types varying from bit
through complex
. By understanding the subtype hierarchy it is possible to determine specific operator instances for heterogeneous arguments.
Using the addition operator as an example, we can understand how Rosetta determines the specific operator instance to apply to any parameter pair. Knowing that, a type checker can determine the specific type associated with the addition operator application. Specifically, for any application (A::T0+B::T1)::T2
, we can determine the type T2
by treating the arguments A
and B
as the most specific type where a matching operator instance exists. For example, the following applications of +
demonstrate the approach:
0::bit + 2::natural == (0::natural + 2::natural)::natural -1::negint + 0::bit == (-1::integer + 0::integer)::integer 1.1::posreal + 2::posint == (1.1::posreal + 2::posreal)::posreal -1.1::negreal + 2.2::posreal == (-1.1::real + 2.2::real)::real
In each case, operands are treated as the most specific type where an instance of the addition operator exists. If such an instance cannot be found, then the expression is not properly typed and a type checker will indicate an error. The following examples show where an instance of addition cannot be found:
(0::bit + 'c'::character) (false::boolean + true::boolean) (true::boolean + 2.9::real)
In each case, no instance of the addition operator exists for the common supertypes of operand types. Bit
and character
share top
as their only common supertype and no addition operator is defined there. The same holds for boolean
and real
as well as for boolean
and boolean
.