numbers.tex

%!TEX root = reference.tex
\chapter{Numeric Expressions}
\label{numbers}
\index{expressions!arithmetic}

The basis of artithmetic expressions are several contracts: the \q{arithmetic} contract which provides definitions of the familiar `calculator' functions of \q{+}, \q{-}, \q{*} and \q{/}; the \q{math} contract which defines the extended set of mathematical functions; the \q{trig} contract which defines standard trigonometric functions; and the \q{bitstring} contract which gives definitions for bitwise manipulation of integer values.

\section{The \q{arithmetic} Contract}
\index{contract!arithmetic@\q{arithmetic} contract}
\label{arithmeticContract}

The \q{arithmetic} contract -- in Program~\vref{arithmeticContractProg} -- defines a minimum set of functions that should be supported by any arithmetic type.

\index{type!contracts! arithmetic@\q{arithmetic}}
\index{arithmetic contract@\q{arithmetic} contract}
\begin{program}
\begin{lstlisting}
contract arithmetic over t is {
  (+) has type (t,t)=>t;
  (-) has type (t,t)=>t;
  (*) has type (t,t)=>t;
  (/) has type (t,t)=>t;
  (%) has type (t,t) => t;
  abs has type (t)=>t;
  __uminus has type (t)=>t;
  zero has type t;
  one has type t;
}
\end{lstlisting}
\caption{The Standard \q{arithmetic} Contract\label{arithmeticContractProg}}
\end{program}

In addition to the \q{arithmetic} contract, the \q{math} contract -- defined in Program~\vref{mathContract} -- defines additional functions that go beyond the standard `calculator' functions.

\begin{aside}
In the standard system, the \q{arithmetic} contract is implemented for \q{integer}s, \q{long}s, \q{float}s and \q{decimal}s. However, it is possible for the programmer to implement \q{arithmetic} for other types.
\end{aside}

\subsection{\q{+} -- addition}
\label{plusFunction}
\index{arithmetic contract@\q{arithmetic} contract!+@\q{+}}
\q{+} is part of the standard \q{arithmetic} contract.
\begin{lstlisting}
(+) has type for all t such that (t,t)=>t where arithmetic over t
\end{lstlisting}

The \q{+} function adds its two arguments together and returns the result.

Depending on the type of the argument, different arithmetic will be invoked. For example
\begin{lstlisting}
X+4
\end{lstlisting}
denotes an \q{integer} addition (and \q{X} must be an \q{integer} variable); whereas
\begin{lstlisting}
Y+5.6
\end{lstlisting}
denotes a \q{float} addition.

\subsection{\q{-} -- subtraction}
\label{minusFunction}
\index{arithmetic contract@\q{arithmetic} contract!-@\q{-}}
\q{-} is part of the standard \q{arithmetic} contract.
\begin{lstlisting}
(-) has type for all t such that (t,t)=>t where arithmetic over t
\end{lstlisting}

The \q{-} function subtracts the second argument from the first and returns the result.

\subsection{\q{*} -- multiplication}
\label{timesFunction}
\index{arithmetic contract@\q{arithmetic} contract!*@\q{*}}
\q{*} is part of the standard \q{arithmetic} contract.
\begin{lstlisting}
(*) has type for all t such that (t,t)=>t where arithmetic over t
\end{lstlisting}
The \q{*} multiplies its two arguments together and returns the result.

\subsection{\q{/} -- division}
\label{divideFunction}
\index{arithmetic contract@\q{arithmetic} contract!/@\q{/}}
\q{/} is part of the standard \q{arithmetic} contract.
\begin{lstlisting}
(/) has type for all t such that (t,t)=>t where arithmetic over t
\end{lstlisting}
The \q{/} function divides the first argument by the second and returns the result.


\subsection{\q{abs} -- absolute value}
\label{abdFunction}
\index{arithmetic contract@\q{arithmetic} contract!abs@\q{abs}}
\q{abs} is part of the standard \q{arithmetic} contract.
\begin{lstlisting}
abs has type for all t such that (t)=>t where arithmetic over t
\end{lstlisting}

The \q{abs} function returns the absolute value of its argument.

\subsection{\q{\_\_uminus} -- unary minus}
\label{unaryMinus}
\index{arithmetic contract@\q{arithmetic} contract!uminus@\q{\_\_uminus}}
\q{\_\_uminus} is part of the standard \q{arithmetic} contract.
\begin{lstlisting}
(__uminus) has type for all t such that (t)=>t where arithmetic over t
\end{lstlisting}
The \q{\_\_uminus} function negates its argument. This function is rarely invoked explicitly by the programmer; it is automatically generated by the compiler with unary-minus expressions. I.e., the expression
\begin{lstlisting}
-X
\end{lstlisting}
is interpreted as a call to \q{\_\_uminus}:
\begin{lstlisting}
__uminus(X)
\end{lstlisting}

\subsection{\q{zero} -- arithmetic zero}
\label{zero}
\index{arithmetic contract@\q{arithmetic} contract!zero\q{zero}}
\q{zero} is part of the standard \q{arithmetic} contract.
\begin{lstlisting}
zero has type for all t such that t where arithmetic over t
\end{lstlisting}

The \q{zero} value returns the `additive zero' for the arithmetic type. It must obey the following axiom:

\begin{lstlisting}[escapechar=|]
|\emph{X}|+zero=|\emph{X}|
\end{lstlisting}
for all \q{\emph{X}} of type \q{t}.

The primary advantage of \q{zero} is that it makes it easier to write generic arithmetic functions; for example:

\begin{lstlisting}
fun fact(N) where N=zero is one
 |  fact(N) default is N*fact(N-one)
\end{lstlisting}


\subsection{\q{one} -- arithmetic unit}
\label{one}
\index{arithmetic contract@\q{arithmetic} contract!one\q{one}}
\q{one} is part of the standard \q{arithmetic} contract.
\begin{lstlisting}
one has type for all t such that t where arithmetic over t
\end{lstlisting}

The \q{one} value returns the `additive unit' for the arithmetic type.  It must obey the following axiom:

\begin{lstlisting}[escapechar=|]
|\emph{X}|*one=|\emph{X}|
\end{lstlisting}
for all \q{\emph{X}} of type \q{t}.

Like \q{zero}, the primary advantage of \q{one} is that it makes it easier to write generic arithmetic functions.

\section{The \q{largeSmall} Contract}
\label{largeSmall}
The \q{largeSmall} contract defines two values that are supposed to represent the largest and smallest legal values respectively of a type. The contract itself is very simple:
\begin{program}
\begin{lstlisting}
contract largeSmall over t is {
  largest has type t;
  smallest has type t;
}
\end{lstlisting}
\caption{The \q{largeSmall} Contract}\label{largeSmallProg}
\end{program}

The \q{largeSmall} contract is implemented for \q{integer}s, \q{long} integers, and \q{float} by default.

\subsection{\q{smallest} -- smallest value}
\begin{lstlisting}
smallest has type for all t such that t where largeSmall over t
\end{lstlisting}

The \q{smallest}  value is the smallest legal value of the type. For example, the smallest \q{long} value corresponds to $-2^{63}-1$.

\begin{aside}
It is not always possible to explicitly write down the smallest value of a type. In particular, it is not possible to write the smallest \q{long} value in decimal numbers.
\begin{aside}
It is possible, however, to write it in hexadecimal:
\begin{lstlisting}
0x8000000000L
\end{lstlisting}
\end{aside}
\end{aside}

\subsection{\q{largest} -- largest value}
\begin{lstlisting}
largest has type for all t such that t where largeSmall over t
\end{lstlisting}

The \q{largest}  value is the largest legal value of the type. For example, the largest \q{float} value is \q{1.7976931348623157E308}.

\begin{aside}
As with the \q{smallest} value; it is not necessarily the case that it is possible to explicitly write the \q{largest} value of a type.
\end{aside}

\section{Bit Manipulation Functions}
\label{bitString}

The \q{bitstring} contract defines a set of bit manipulation functions.

\begin{aside}
In the standard system, the \q{bitstring} functions are only implemented by the \q{integer} and \q{long} types.
\end{aside}

\begin{aside}
The bitstring functions require an explicit \q{import} before using them:
\begin{lstlisting}
import bitstring;
myPk is package { ...
\end{lstlisting}
\end{aside}

\index{type!contracts!bitstring@\q{bitstring}}
\index{bitstring contract@\q{bitstring} contract}
\begin{program}
\begin{lstlisting}
contract bitstring over t is {
    (.&.) has type (t,t)=>t;
    (.^.) has type (t,t)=>t;
    (.|.) has type (t,t)=>t;
    (.<<.) has type (t,t)=>t;
    (.>>.) has type (t,t)=>t;
    (.>>>.) has type (t,t)=>t;
    (.~.) has type (t)=>t;
    (.#.) has type (t)=>integer;
}
\end{lstlisting}
\caption{The Standard \q{bitstring} Contract\label{bitstringContractDef}}
\end{program}

\subsection{\q{.\&.} Bit-wise Conjunction}
\label{bitAnd}
\begin{lstlisting}
(.&.) has type for all t such that (t,t)=>t where bitstring over t
\end{lstlisting}

The \q{.\&.} operator returns the bit-wise conjunction of two values.

\subsection{\q{.|.} Bit-wise Disjunction}
\label{bitOr}
\begin{lstlisting}
(.|.) has type for all t such that (t,t)=>t where bitstring over t
\end{lstlisting}

The \q{.|.} operator returns the bit-wise disjunction of two values.

\subsection{\q{.\^{}.} Bit-wise Exclusive-or}
\label{bitXor}
\begin{lstlisting}
(.^.) has type for all t such that (t,t)=>t where bitstring over t
\end{lstlisting}

The \q{.\^{}.} operator returns the bit-wise exclusive of two values.

\subsection{\q{.<<.} Bit-wise Left Shift}
\label{bitLeft}
\begin{lstlisting}
(.<<.) has type for all t such that (t,t)=>t where bitstring over t
\end{lstlisting}

The \q{.<<.} operator left-shifts the left hand argument by the number of bits indicated in the right argument. It is effectively multiplication by a power of 2.

\subsection{\q{.>>.} Bit-wise Arithmetic Right Shift}
\label{bitRight}
\begin{lstlisting}
(.>>.) has type for all t such that (t,t)=>t where bitstring over t
\end{lstlisting}

The \q{.>>.} operator right-shifts the left hand argument by the number of bits indicated in the right argument. The most significant bit is replicated in the shift. It is effectively division by a power of 2.

\subsection{\q{.>>>.} Bit-wise Logical Right Shift}
\label{bitRightLogic}
\begin{lstlisting}
(.>>>.) has type for all t such that (t,t)=>t where bitstring over t
\end{lstlisting}

The \q{.>>>.} operator right-shifts the left hand argument by the number of bits indicated in the right argument. The most significant bits of the result are replaced by zero. This operator is sometimes known as logical right shift.

\subsection{\q{.\~\xspace.} Bit-wise Logical Complement}
\label{bitComplement}
\begin{lstlisting}
(.~.) has type for all t such that (t)=>t where bitstring over t
\end{lstlisting}

The \q{.\tlda.} operator forms the logical or 1's complement of its argument.

\subsection{\q{.\#.} Bit Count}
\label{bitCount}
\begin{lstlisting}
(.#.) has type for all t such that (t,t)=>t where bitstring over t
\end{lstlisting}

The \q{.\#.} operator computes the number of non-zero bits in its argument.


\section{Trigonometry Functions}
\label{trigContract}
The \q{trig} contract -- see Program~\vref{trigContractDef} -- defines standard trigonometry functions.

\begin{aside}
By default, the \q{trig} contract is only implemented over \q{float}ing point numbers.
\end{aside}

\begin{aside}
All the \q{trig} functions assume that the angles that they accept (or return) are expressed in radians.
\end{aside}

\index{type!contracts! trig@\q{trig}}
\index{trig contract@\q{trig} contract}
\begin{program}
\begin{lstlisting}
contract trig over t is {
  sin has type (t)=>t;
  asin has type (t)=>t;
  sinh has type (t)=>t;
  cos has type (t)=>t;
  acos has type (t)=>t;
  cosh has type (t)=>t;
  tan has type (t)=>t;
  atan has type (t)=>t;
  tanh has type (t)=>t;
}
\end{lstlisting}
\caption{The Standard \q{trig} Contract\label{trigContractDef}}
\end{program}

\subsection{\q{sin} -- Sine Function}
\begin{lstlisting}
sin has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{sin} function returns the Sine of its argument -- expressed in radians.

\subsection{\q{asin} -- Arc Sine Function}
\begin{lstlisting}
asin has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{asin} function returns the Arc Sine of its argument -- expressed in radians.

\subsection{\q{sinh} -- Hyperbolic Sine Function}
\begin{lstlisting}
sinh has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{sinh} function returns the hyperbolic sine of its argument -- expressed in radians.

The hyperbolic sine of X is defined to be $(e^X - e^{-X})/2$.

\subsection{\q{cos} -- Cosine Function}
\begin{lstlisting}
cos has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{cos} function returns the cosine of its argument -- expressed in radians.

\subsection{\q{acos} -- Arc Cosine Function}
\begin{lstlisting}
acos has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{acos} function returns the arc cosine of its argument -- expressed in radians.

\subsection{\q{cosh} -- Hyperbolic Cosine Function}
\begin{lstlisting}
cosh has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{cosh} function returns the hyperbolic cosine of its argument -- expressed in radians.

The hyperbolic cosine of X is defined to be $(e^X + e^{-X})/2$.

\subsection{\q{tan} -- Tangent Function}
\begin{lstlisting}
tan has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{tan} function returns the tangent of its argument -- expressed in radians.

\subsection{\q{atan} -- Arc Tangent Function}
\begin{lstlisting}
atan has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{atan} function returns the Arc Tangent of its argument -- expressed in radians.

\subsection{\q{tanh} -- Hyperbolic Tangent Function}
\begin{lstlisting}
tanh has type for all t such that (t)=>t where trig over t
\end{lstlisting}

The \q{tanh} function returns the hyperbolic tangent of its argument -- expressed in radians.

The hyperbolic tangent of X is defined to be $sinh(X)/cosh(X)$.

\section{Numeric Display Functions}
\label{numberDisplay}

The numeric display functions allow the representation of numbers as \q{string} values.

\subsection{\q{display} -- Display a number}
\label{displayNumFun}

The \q{display} function can be used to display a numeric value.
\begin{lstlisting}[escapechar=|]
display has type (|\ntRef{Type}|)=>string
\end{lstlisting}
The \q{display} function relies on the \q{ppDisp} function which is part of the \q{pPrint} contract -- see Program~\vref{ppContractProg}.

\subsection{\q{\_format} -- Format a number as a string}
\label{formatNumber}
\begin{lstlisting}[escapechar=|]
_format has type (|\ntRef{Type}|,string)=>pP
\end{lstlisting}
where \q{\emph{Type}} is one of \q{integer}, \q{long} or \q{float}.

The \q{\_format} function is part of the \q{formatting} contract -- see Program~\vref{formatContractProg}.

The format string for integral values determines how the number is formatted. For example, the result of
\begin{lstlisting}
"--$(-15):-   0;--"
\end{lstlisting}
is
\begin{lstlisting}
"--  -15--"
\end{lstlisting}

The grammar for legal formatting codes for integral values may be given in the regular expression:
\begin{lstlisting}
`[P+-]?([09 ,.])+[P+-]`
\end{lstlisting}
I.e., a sign specification, followed by digit specifications optionally mixed with thousands markers and periods, terminated by an optional sign specification.

The grammar for legal formatting codes for \q{float} values is a little more complex:
\begin{lstlisting}
`[P+-]?[09 ,.]+([eE][+-]?[09 ]+)?[P+-]?
\end{lstlisting}
I.e., the format string for \q{float} values permits the exponent to be printed as well as the mantissa. If the exponent part is missing and if the \q{float} value cannot be represented in the available precision without an exponent then an exception will be \q{raised}.

The complete list of formatting codes for formatting numeric values is:

\begin{description}
\item[\q{9}] A digit is displayed if it is significant. I.e., if it is non-zero or there is a non-zero digit to the left of the digit.
\item[\q{0}] A zero character is used for numeric values. It always results in a digit being displayed. For example, the value of
\begin{lstlisting}
"--$(5):00;--"
\end{lstlisting}
is the string
\begin{lstlisting}
"--05--"
\end{lstlisting}

\item[\q{\spce{}}] A space character is similar to the \q{0} code; except that a leading space is displayed instead of a leading zero. 

For example, the value of
\begin{lstlisting}
"--$(5):00;--"
\end{lstlisting}
is the string
\begin{lstlisting}
"-- 5--"
\end{lstlisting}

\begin{aside}
Signs are treated specially with the \q{\spce{}} code: any produced sign character is migrated past leading spaces -- with the result that the sign character is always abutted to the digits.

For example, the result of
\begin{lstlisting}
"--$(-15):-   0;--"
\end{lstlisting}
is
\begin{lstlisting}
"--  -15--"
\end{lstlisting}
The \q{\spce{}} code is especially useful for lining up columns of figures where a leading space is preferred over leading zeroes.
\end{aside}

\item[\q{.}] A period is displayed if there is a digit to the left.

This is used for showing currency values -- when they are represented internally as pennies but should be displayed as dollar values -- and for floating point numbers.
\item[\q{,}] A comma is displayed if there is a digit to the left. 

This is used for displaying values in the `thousands' notation. For example, the value of
\begin{lstlisting}
"--$(120345567):999,999,999,999;--"
\end{lstlisting}
is the string:
\begin{lstlisting}
"--120,345,567--"
\end{lstlisting}

\item[\q{-}] Is used to control how signed values are presented. If the value is negative then a \q{-} character is displayed; if the value is positive then a space is displayed.

\begin{aside}
The \q{-} \ntRef{FormatCode} may appear at either end of the display. A leading \q{-} results in the sign being displayed at the beginning -- before any digits -- and a trailing \q{-} results in the sign appended to the end.
\end{aside}

\begin{aside}
\begin{aside}
If no `sign' code is present in the \ntRef{FormattingSpec} then nothing is displayed if the value is positive or negative.
\end{aside}
\end{aside}

\item[\q{+}] Always results in a sign being displayed. If the value is negative then a \q{-} character is displayed; otherwise a \q{+} character is displayed.

Like the \q{-} code, the \q{+} may appear at either end of the display format.

\item[\q{P}] The \q{P} code uses parentheses on either end of the value to indicate a negative value. If the value is positive then spaces are appended to either end; otherwise the number is enclosed in \q{()}'s.

\begin{aside}
The \q{P} code should be placed at \emph{both} ends of the \ntRef{FormattingSpec}.
For example, the expression:
\begin{lstlisting}
"Balance: $Amnt:P999900.00P; remaining"
\end{lstlisting}
where \q{Amnt} had value -563 would result in
\begin{lstlisting}
"Balance: (05.63) remaining"
\end{lstlisting}
\end{aside}
\item[\q{X}] Causes the integer to be formatted as a hexadecimal number; and a hexadecimal digit is displayed if it is significant. I.e., if it is non-zero or there is a non-zero digit to the left of the digit.

For example, this can be used to display the Unicode equivalent of a character:
\begin{lstlisting}
"Unicode: $C/$(C as integer):XXXXX;"
\end{lstlisting}

\end{description}

\section{Additional Arithmetic Functions}
\label{mathContract}
The \q{math} contract -- see Program~\vref{mathContractDef} -- defines additional functions.

\begin{aside}
The \q{math} contract is not implemented by all number types; in particular, it is implemented by \q{integer}, \q{long} and \q{float}; but is not implemented by \q{decimal}.
\end{aside}

\index{type!contracts! math@\q{math}}
\index{math contract@\q{math} contract}
\begin{program}
\begin{lstlisting}
contract math over t is {
  min has type (t,t)=>t;
  max has type (t,t)=>t;
  random has type (t)=>t;
  sqrt has type (t)=>t;
  cbrt has type (t)=>t;
  ceil has type (t)=>t;
  floor has type (t)=>t;
  round has type (t)=>t;
  log has type (t)=>t;
  log10 has type (t)=>t;
  exp has type (t)=>t
  (**) has type (t,t) => t;
}
\end{lstlisting}
\caption{The Standard \q{math} Contract\label{mathContractDef}}
\end{program}

\subsection{\q{min} -- minimum value}
\begin{lstlisting}
min has type for all t such that (t,t)=>t where math over t
\end{lstlisting}

The \q{min} function returns the smaller of its two arguments.

\subsection{\q{max} -- maximum value}
\begin{lstlisting}
max has type for all t such that (t,t)=>t where math over t
\end{lstlisting}

The \q{max} function returns the larger of its two arguments.

\subsection{\q{sqrt} -- square root}
\begin{lstlisting}
sqrt has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{sqrt} function returns the square root of its argument. If the argument is negative, the returned value is undefined.

\subsection{\q{cbrt} -- cube root}
\begin{lstlisting}
cbrt has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{cbrt} function returns the cube root of its argument. Note that $-cbrt(X)=cbrt(-X)$.

\subsection{\q{ceil} -- ceiling}
\begin{lstlisting}
ceil has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{ceil} function returns the nearest integral value that is equal to or larger than X.
\begin{aside}
For integral types,
\begin{lstlisting}
fun ceil(X)=X
\end{lstlisting}
\end{aside}

\subsection{\q{floor} -- floor}
\begin{lstlisting}
floor has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{floor} function returns the nearest integral value that is equal to or smaller than X.
\begin{aside}
For integral types,
\begin{lstlisting}
fun floor(X)=X
\end{lstlisting}
\end{aside}

\subsection{\q{round} -- round to closest integral}
\begin{lstlisting}
round has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{round} function returns the nearest integral value to its argument. 
\begin{aside}
For all values,
\begin{lstlisting}
fun round(X)=floor(X + 0.5)
\end{lstlisting}
\end{aside}


\subsection{\q{log} -- Natural Logarithm}
\begin{lstlisting}
log has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{log} function returns the natural logarithm of its argument.

\subsection{\q{log10} -- Logarithm Base 10}
\begin{lstlisting}
log10 has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{log10} function returns the base 10 logarithm of its argument.


\subsection{\q{exp} -- Natural Exponentiation}
\begin{lstlisting}
exp has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{exp} function returns the value $e^X$.

\subsection{\q{random} -- random number generation}
\index{random number generation}
\begin{lstlisting}
random has type for all t such that (t)=>t where math over t
\end{lstlisting}

The \q{random} function returns a number in the half-open range [0,X) where X is the argument of the function.
\begin{aside}
The argument of the \q{random} function must be a positive number. However, it can be any `normal' kind of arithmetic value.
\end{aside}
The number generated is the next in a sequence of numbers that is typically \emph{pseudo-random}: i.e., not actually random but statistically indistinguishable from random.

The type of the returned result is the same as the type of its argument.

\subsection{\q{**} -- exponentiation}
\label{powerFunction}
\index{math contract@\q{math} contract!**@\q{**}}
\q{**} is part of the standard \q{math} contract.
\begin{lstlisting}
(**) has type for all t such that (t,t)=>t where math over t
\end{lstlisting}
The \q{**} function raises the first argument to the power of the second.

For example, the expression
\begin{lstlisting}
X**3
\end{lstlisting}
denotes the cube of \q{X}.

\section{Numeric Ranges}
\label{numericRange}
The \q{range} type defines a numeric range. It is useful primarily in loops; for example:
\begin{lstlisting}
X is list of {all Ix where Ix in range(0,10,1) }
\end{lstlisting}
has, as its value:
\begin{lstlisting}
list of [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
\end{lstlisting}

\begin{aside}
Ranges are half-open: they include their beginning value but do not include their terminator value. This permits simpler merging of ranges:
\begin{lstlisting}[escapechar=|]
range(0,10,1)++range(10,20,1) |\ensuremath{\equiv}| range(0,20,1)
\end{lstlisting}
\end{aside}

\subsection{The \q{range} Type}
The \q{range} type is defined in Program~\vref{rangeTypeProg}.
\begin{program}
\begin{lstlisting}
type range of t where arithmetic over t and comparable over t 
  is range(t,t,t);
\end{lstlisting}
\caption{The Standard \q{range} Type\label{rangeTypeProg}}
\end{program}

Note that this is a constrained type. It is a generic type but is only defined for type arguments that are \q{comparable} and which are defined over \q{arithmetic}.

The \q{range} type implements the \q{sizeable} contract (see Section~\vref{sizeableContract}), the \q{iterable} contract (see Section~\ref{iterableContract}) and the \q{concatenate} (see Section~\vref{concatenateContract}) contracts. This means that \q{range} is suitable for controlling for loops:
\begin{lstlisting}
for Ix in range(0,10,1) do
  logMsg(info,"$Ix")
\end{lstlisting}
as well as for using in queries such as above.