variables.tex

%!TEX root = reference.tex
\chapter{Variables}
\label{variables}

\index{variable}
\index{expressions!variable}

A \ntRef{Variable} is a placeholder that denotes a value. Variables may be used to denote many kinds of values -- arithmetic values, complex data structures and programs.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{Variable}&\arrow&\ntRef{Identifier}
\end{eqnarray*}
\vskip-1.5ex\caption{Variables}\label{variableFig}
\end{figure}

\begin{aside}
Any given variable has a single type associated with it and may only be bound to values of that type.\footnote{We sometimes informally refer to a variable being `bound' to a value X (say). This means that the value associated with the variable is X.}
\end{aside}

Variables have a `scope' -- a syntactic range over which they are defined. Variables can be said to be `free' in a given scope -- including functions that they are referenced within.

Variables can be classified into `single-assignment' variables (variables that denote values and are therefore not reassignable) and `re-assignable' variables. The latter have a different type signature that signals the re-assignable property.

\section{Variable Declaration}
\label{VariableDeclaration}
\index{variable!declaration of}

A \ntRef{VariableDeclaration} is a \ntRef{Definition} or an \ntRef{Action} that explicitly denotes the declaration of a variable. \ntRef{VariableDeclaration}s may appear in \ntRef{ThetaEnvironment}s and \ntRef{Action}s.
\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{VariableDeclaration}&\arrow&\q{def}\,\ntRef{Pattern}\ \q{is}\ \ntRef{Expression}\\
&\choice&\q{var}\ \ntRef{Identifier}\ \q{:=}\ \ntRef{Expression}
\end{eqnarray*}
\caption{Variable Declaration}\label{variableDeclarationFig}
\end{figure}

\index{single assignment variable}
The left-hand side of a single assignment declaration may be a \emph{Pattern}. This permits multiple variables to be declared in a single statement. This, in turn, facilitates the handling of functions that return more than one value.

For example, assuming that \q{split} partitions a \q{list} into a front half and a back half, returning both in a 2-tuple, the declaration:
\begin{lstlisting}
def (L,R) is split(Lst)
\end{lstlisting}
will bind the variables \q{L} and \q{R} to the front and back halves respectively.

\index{reassignable variable}
A re-assignable variable is declared using the form:
\begin{lstlisting}[mathescape=true]
var $\ntRef{Variable}$ := $\ntRef{Expression}$
\end{lstlisting}

\begin{aside}
Unlike single assignment variable declarations, the re-assignable variable declaration is restricted to defining individual variables.
\end{aside}

\begin{aside}
It is not possible to declare a variable without also giving it a value.
\end{aside}

\subsection{Variable Scope}
\label{scope}
\hypertarget{Scope}{}
\index{scope!variables, of}
\index{variable scope}

In general, the scope of a variable extends to include the entire context in which it is declared. In the case of a variable declaration in a \ntRef{ThetaEnvironment}, the scope includes the entire \ntRef{ThetaEnvironment} and any associated bound element. In the case of an \ntRef{ActionBlock} the scope extends from the action following the declaration through to the end of the enclosing \ntRef{ActionBlock}.

The precise rules for the scope of a variable are slightly complex but result in a natural interpretation for the scopes of variables:

\begin{itemize}
\index{pattern}
\item Variables that are defined in patterns are limited to the element that is `naturally' associated with that pattern:
\begin{itemize}
\item Variables declared in the head pattern of an equation or other rule are scoped to that equation or rule.
\index{conditional expression}
\index{expressions!conditional}
\index{loop!for@\q{for}}
\item If a pattern governs a conditional expression or statement, variables declared in the pattern extend to the `then' part of the conditional but not to any `else' part.
\item If a pattern governs a \q{for} loop, or a \q{while} loop, then variables declared in the pattern extend to the body of the loop. (See Section~\vref{forLoop} and Section~\vref{whileLoop}).
\end{itemize}
\item Variables that are defined in a \ntRef{Condition} are bound by the scope of the \ntRef{Condition}.
\item Variables that are declared in a \ntRef{ThetaEnvironment} extend to all the  definitions in the \ntRef{ThetaEnvironment} and to any bound expression or action.
\begin{aside}
In particular, variables defined within a \ntRef{ThetaEnvironment} may be \emph{mutually recursive}.
\begin{aside}
Note that it is \emph{not} permissible for a non-program variable to be involved in a mutually recursive group of variables. I.e., if a group of mutually recursive of variables occurs in a \ntRef{ThetaEnvironment} then all the variables must be bound to functions or other program elements.
\end{aside}
\end{aside}
\item Variables that are \q{import}ed into a package body from another package extend to the entire body of the importing \q{package}.
\item Variables that are declared in an \ntRef{ActionBlock} extend from the end of their \ntRef{VarDeclaration} to the end of the block that they are defined in. The scope of a variable does not include its \ntRef{VarDeclaration}.

It is not permitted for a variable to be declared more than once in a given action block.
\end{itemize}

\subsection{Scope Hiding}
\label{scopeHiding}
\index{scope!hiding}
\index{variable scope,hiding}
It is not permitted to define a variable with the same name as another variable that is already in scope. This applies to variables declared in patterns as well as variables declared in \ntRef{ThetaEnvironment}s.

For example, the function:
\begin{lstlisting}
fun hider(X) is let{
  def X is 1;
} in X
\end{lstlisting}
is \emph{not} permitted because there would be two \q{X} variables with overlapping scope.
\begin{aside}
The reason for this rule is that scope hiding can be extremely confusing. The meaning of \q{X} in the \q{hider} function is very likely to be misunderstood by programmers and by others reading the program. There could be long distances between a local declaration of a variable and the same variable occurring in an outer scope.
\end{aside}

\section{Re-assignable Variables}
\label{reassignableVars}

\index{variable!re-assignable}
Re-assignable variables serve two primary roles within programs: to hold and represent state and to facilitate several classes of algorithms that rely on the manipulation of temporary state in order to compute a result.

In order to facilitate program combinations -- including procedural abstraction involving re-assignable variables -- there are additional differences between re-assignable variables and single-assignment variables.

\subsection{The \q{ref} Type}
\label{refType}
\index{ref type@\q{ref} type}
\index{type!ref@\q{ref}}
Re-assignable variables have a distinguished type compared to single-valued variables. The type of a re-assignable variable takes the form:
\begin{lstlisting}[mathescape=true]
ref $\ntRef{Type}$
\end{lstlisting}
rather than simply \ntRef{Type}. For example, given the declaration:
\begin{lstlisting}
var Ix := 0
\end{lstlisting}
the variable \q{Ix} has type \q{ref integer}; whereas the declaration:
\begin{lstlisting}
def Jx is 0
\end{lstlisting}
results in the variable \q{Jx} having type \q{integer}.

In addition to the different type, there are two operators that are associated with re-assignable variables: \q{ref} and \q{!} (pronounced \emph{shriek}). The former is used in situations where a variable's name is intended to mean the variable itself -- rather than its value. The latter is the converse: where an expression denotes a reference value that must be `dereferenced'.

\subsection{Re-assignable Variables in Expressions}
\label{referRef}
\index{referring to re-assignable variables!in expressions}
There are two modes of referring to re-assignable variables\footnote{Here we automatically include local variables, theta variables and record fields in this discussion.} in expressions: to access the value of the variable and to access the variable itself. The primary reason for the latter may be to assign to the variable, or to permit a later assignment.

By default, an undecorated occurrence of a variable denotes access to the variable's value. Thus, given a variable declaration:
\begin{lstlisting}
var Cx := 0
\end{lstlisting}
then the reference to \q{Cx} in the expression:
\begin{lstlisting}
Cx+3
\end{lstlisting}
is understood to refer to the value of the variable:
\begin{lstlisting}
!Cx+3
\end{lstlisting}
This is formalized in the inference rule:
\begin{prooftree}
\AxiomC{\typeprd{E}{V}{\q{ref }T}}
\UnaryInfC{\typeprd{E}{V}{T}}
\end{prooftree}

If an expression is prefixed by the \q{ref} operator then this value interpretation is suppressed. I.e., if the expression has a \q{ref}erence type, then prefixing the expression with a \q{ref} suppresses this default `dereferencing' semantics:

\begin{prooftree}
\AxiomC{\typeprd{E}{V}{\q{ref }T}}
\UnaryInfC{\typeprd{E}{\q{ref }V}{\q{ref }T}}
\end{prooftree}

In the case that it is necessary to manually dereference an expression, the \q{!} operator may be used to achieve that:
\begin{prooftree}
\AxiomC{\typeprd{E}{Ex}{\q{ref }T}}
\UnaryInfC{\typeprd{E}{\q{!}Ex}{T}}
\end{prooftree}

\subsection{Re-assignable Variables in Patterns}
\label{reVarInPattern}
\index{referring to re-assignable variables!in patterns}
Patterns are used to introduce variables as well as to denote an implicit equality test. The semantics of re-assignable variables in patterns mirrors that of expressions: an undecorated reference to a re-assignable variable\footnote{It must be the case that there is a prior declaration or introduction of the variable that denotes it as re-assignable.} it understood to refer to the value of the variable.

A pattern of the form:
\begin{lstlisting}[mathescape=true]
ref $\ntRef{Identifier}$
\end{lstlisting}
is understood to refer to the introduction of a re-assignable variable.

For example, the procedure definition head:
\begin{lstlisting}
prc assign(ref X,V) do X:=V
\end{lstlisting}
introduces the variable \q{X} as a re-assignable variable. 
\begin{aside}
When used in patterns of procedures (or other program rules), \q{ref}erence arguments \emph{must} be accompanied by \q{ref} expressions when the procedure is called. Thus, the \q{assign} procedure can be called only by explicitly \q{ref}erring to a variable:
\begin{lstlisting}
assign(ref X,34)
\end{lstlisting}
\begin{aside}
This example shows that it is straightforward to abstract over assignment when designing procedures.
\end{aside}
\end{aside}
The type of a \q{ref} pattern is also a \q{ref} type:
\begin{prooftree}
\AxiomC{\typeprd{E}{V}{T}}
\UnaryInfC{\typeprd{E}{\q{ref }V}{\q{ref }T}}
\end{prooftree}
\begin{aside}
The type of the \q{assign} procedure above is:
\begin{lstlisting}
for all t such that (ref t,t)=>()
\end{lstlisting}
\end{aside}

\section{Variable Assignment}
\label{variableAssignment}
\index{assignment to variables}
\index{variables!assignment to}

Assignment is an action that replaces the value of a re-assignable variable with another value. The variable being re-assigned must have a \q{ref} type -- there is no `implicit' assignability of a variable or field.

Assignment is defined in Section~\vref{assignment}.

\subsection{Modifying Fields of Records}
\label{fieldModify}
Assignability of variables does \emph{not} automatically imply that the value of the variable is itself modifiable. Thus, given a variable declaration such as:
\begin{lstlisting}
var P := someone{ name="fred"; age=23 }
\end{lstlisting}
the assignment:
\begin{lstlisting}
P.age := 24
\end{lstlisting}
is not valid -- because, while we can assign a new value to \q{P}, that does not confer an ability to modify the value that \q{P} has.

However, by marking a \emph{field} of a record type as a \q{ref} type, then we \emph{can} change that field of the record. Thus, for example, if the type of \q{person} were:
\begin{lstlisting}
type person is person{
  name has type string;
  age has type ref integer;
}
\end{lstlisting}
then the assignment:
\begin{lstlisting}
P.age := 24
\end{lstlisting}
is valid.
\begin{aside}
Note that one may change a suitably declared field of a record even when the variable 'holding' the record it not itself re-assignable.
\begin{lstlisting}
P is someone{ name="fred"; age := 23 }
\end{lstlisting}
I.e., re-assignability depends only on whether the target is re-assignable.
\end{aside}