


% ------------------------------------------------------------------------------
\subsection{Region Handles}
We write witnesses with an underline, and the first we discuss are the region allocation witnesses $\un{\rho_n}$. These are also called \emph{region handles} and are introduced into the program with the $\kletregion \ r \ \kin \ t$ expression. Reduction of this expression allocates a fresh handle $\un{\rho}$ and substitutes it for all occurrences of the variable $r$ in $t$. To avoid problems with variable capture we require all bound variables $r$ in the initial program to be distinct. Although region handles are not needed at runtime, we can imagine them to be operational descriptions of physical regions of the store, perhaps incorporating a base address and a range. For example, the following program adds two to its argument, while storing an intermediate value in a region named $r_3$.

\begin{tabbing}	
MM \= MMMMMx \= MMM \kill
\>	$\iaddTwo \ ::$ \> $ \forall r_1 \ r_2. \ \iInt \ r_1 \longtoa{\iRead r_1} \iInt \ r_2$ \\
\>	$\iaddTwo \ =$ 
		\> $\Lambda r_1 \ r_2. \ \lambda (x : \iInt \: r_1).$ \\
\>		\> $\kletregion \ r_3 \ \kin \ \isucc \ r_3 \ r_2 \ (\isucc \ r_1 \ r_3 \ x)$
\end{tabbing}
This program makes use of the primitive $\isucc$ function that reads its integer argument and produces a new value into a given region:
\begin{tabbing}	
MM 	\= MMMMx 	\= MMM \kill
	\> $\isucc \ :: \ \forall r_1 \ r_2. \ \iInt \ r_1 \longtoa{\iRead r_1} \iInt \ r_2$	
\end{tabbing}

Note the phase distinction between region variables $r_n$ and region handles $\un{\rho_n}$. Region handles are bound by region variables. As no regions exist in the store before execution, region handles may not occur in the initial program. Also, although the outer call to $\isucc$ reads a value in $r_3$, this effect is not observable by calling functions, so is masked and not included in the type signature of $\iaddTwo$. This is similar to the system of \cite{tofte:mlkit-4.3.0}.


% ------------------------------------------------------------------------------
\subsection{Witnesses of Constancy and Mutability}
\label{Witnesses:Constancy-and-Mutability}
The constancy or mutability of values in a particular region is represented by the witnesses $\un{\rconst \ \rho}$ and $\un{\rmutable \ \rho}$. Once again, these witnesses may not occur in the initial program. Instead, they are created with the $\iMkConst$ and $\iMkMutable$ witness type constructors which have the following kinds:

\begin{tabbing}
MM \= MMMMMM \= MMM \kill
\> $\iMkConst$   \> $:: \Pi (r : \%). \ \iConst \ r$ \\
\> $\iMkMutable$ \> $:: \Pi (r : \%). \ \iMutable\ r$ 
\end{tabbing}

Both constructors take a region handle and produce the appropriate witness. To ensure that both $\un{\rconst \ \rho_n}$ and $\un{\rmutable \ \rho_n}$ for the same $\un{\rho_n}$ cannot be created by a given program, we require the mutability of a region to be set at the point it is introduced. We introduce new regions with $\kletregion$, so extend this construct with an optional witness binding that specifies the desired mutability. If a function accesses values in a given region, and does not possess either a witness of constancy or mutability for that region, then it cannot assume either. For example, the following function computes the length of a list by destructively incrementing a local accumulator, then copying out the final value.

\begin{tabbing}
MM \= MMM \= M \= MM \= MMMM \= MMMMMMx \= M \= MM \kill
\> $\ilength$ 	\> $::$	\> $\forall a \ r_1 \ r_2. \ \iList \ r_1 \ a \longtoa{\iRead \ r_1} \iInt \ r_2$ \\
\> $\ilength$	\> $=$	\> $\Lambda a \ r_1 \ r_2. \ \lambda (\ilist : \iList \ r_1 \ a).$ \\
\> 		\> 	\> $\kletregion \ r_3 \ \kwith \ \{ w = \iMkMutable \ r_3 \} \ \kin $ \\
\>		\> 	\> $\klet$ 	\> $(\iacc$ 	\> $ : \iInt \ r_3)$	\> $= 0 \ r_3$ \\
\>		\>	\>		\> $(\ilength'$	\> $ : ...)$	\\
\>		\>	\>		\> \quad $= \lambda (\ixx : \iList \ r_1 \ a). $ \\
\>		\>	\>		\> \> $\kcase \ \ixx \ \kof$ \\
\>		\>	\>		\> \> \quad $\iNil$			  \> $\to$ \> $\icopyInt \ r_3 \ r_2 \ \iacc$ \\
\>		\>	\>		\> \> \quad $\iCons \ \_ \ \ixs$ \> $\to$ \> $\klet \ (\_ : ()) = \iincInt \ r_3 \ w \ \iacc$ \\ 
\>		\>	\>		\> \>					  \>	  \> $\kin \ \ilength' \ixs$ \\
\>		\> 	\> $\kin$	\> $\ilength' \ \ilist$
\end{tabbing}
where
\begin{tabbing}
MM \= MMMM \= MMMM \= MMMMMMMMx \= MM \= MMMMM \= MM \kill
\> $\icopyInt$	\> $:: \forall r_1 \ r_2.$ 
		\> $\iInt \ r_1 \longtoa{\iRead \ r_1} \iInt \ r_2$ 
\\
\> $\iincInt$	\> $:: \forall r_1. \iMutable \ r_1 \To$ 	
		$\iInt \ r_1 \longtoa{\iRead r_1 \lor \iWrite r_1} ()$ 
\end{tabbing}
The set after the $\kwith$ keyword binds an optional witness type variable. If the region variable bound by the $\kletregion$ is $r$, then the right of the witness binding must be either $\iMkConst \ r$ or $\iMkMutable \ r$. The type constructors $\iMkConst$ and $\iMkMutable$ may not occur elsewhere in the program. The $\ilength$ function above makes use of $\iincInt$ which requires its integer argument to be in a mutable region, and we satisfy this constraint by passing it our witness to the fact.


% ------------------------------------------------------------------------------
\subsection{Laziness and Witnesses of Purity}
\label{Witnesses:Purity}
Although we use call-by-value evaluation as the default, we can suspend the evaluation of an arbitrary function application with the $\isuspend$ operator:
\begin{tabbing}
MM \= MMMM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\isuspend$	\> $:: \forall a \ b \ e. \ \iPure \ e \To (a \toa{e} b) \to a \to b$
\end{tabbing}
$\isuspend$ takes a parameter function of type $a \toa{e} b$, its argument of type $a$, and defers the application by building a thunk at runtime. When the value of the thunk is demanded, the contained function will be applied to its argument, yielding a result of type $b$. As per \cite{launchbury:lazy}, values are demanded when they are used as the function in an application, or are inspected by a case-expression or primitive operator such as $\iupdate$. The constraint $\iPure \ e$ indicates that we must also provide a witness that the application to be suspended is observably pure. Witnesses of purity are written $\un{\rpure \ \sigma}$ where $\sigma$ is some effect. They can be created with the $\iMkPurify$ witness type constructor. For example, the following function computes the successor of its argument, but only when the result is demanded:
\begin{tabbing}
MM \= MMM \= M \= MMMM \= MMMMMMx \= M \= MM \kill
	\> $\isuccL$	\> $::$	\> $\forall r_1 \ r_2. \ \iConst \ r_1 \To \iInt \ r_1 \longtoa{\iRead \ r_1} \iInt \ r_2$ \\
	\> $\isuccL$ 	\> $=$	\> $\Lambda r_1 \ r_2 \ (w : \iConst \ r_1). \ \lambda (x : \iInt \ r_1). $ \\	
	\>		\> 	\> $\isuspend$ 	\> $(\iInt \ r_1) \ (\iInt \ r_2) \ (\iRead \ r_1) \ (\iMkPurify \ r_1 \ w)$ \\
	\> 		\>	\>		\> $(\isucc \ r_1 \ r_2) \ x$
\end{tabbing}
$\iMkPurify$ takes a witness that a particular region is constant, and produces a witness proving that a read from that region is pure. It has the following kind:
\begin{tabbing}
MM \= MMMMM \= MMM \kill
\> $\iMkPurify$	\> $:: \Pi (r : \%). \ \iConst \ r \rightarrow \ \iPure \ (\iRead \ r)$ 
\end{tabbing}
Reads of constant regions are pure because it does not matter when the read takes place, the same value will be returned each time. Note that in our system there are several ways of writing the effect of a pure function. As mentioned in \S\ref{Update:UpdatingIntegers} the effect term $\bot$ is manifestly pure. However, we can also treat any other effect as pure if we can produce a witness of the appropriate kind. For example, $\iRead \ r_5$ is pure if we can produce a witness of kind $\iPure \ (\iRead \ r_5)$.


% ------------------------------------------------------------------------------
\subsection{Witness Joining and Explicit Effect Masking}
Purity constraints extend naturally to higher order functions. Here is the definition of a lazy map function, $\imapL$, which constructs the first list element when called, but only constructs subsequent elements when they are demanded:
\begin{tabbing}
MM \= MMM \= M \= MMMMM \kill
	\> $\imapL$	\> $::$ \> $\forall a \ b \ r_1 \ r_2 \ e.$ \\
	\>		\> 	\> $\iConst \ r_1 \To \iPure \ e \To (a \toa{e} b) \to \iList \ r_1 \ a  \to \iList \ r_2 \ b$ 
\end{tabbing}
\begin{tabbing}
MM \= Mx \= Mx \= MMMMMx \= MMMM \= MMMxx \= MMMMMM \kill
	\> $\imapL$ \\
	\> \ $=$	\> $\Lambda a \ b \ r_1 \ r_2 \ e \ (w_1 : \iConst \ r_1) \ (w_2 : \iPure \ e).$ \\
	\>		\> $\lambda (f : a \toa{e} b) \ (\ilist : \iList \ r_1 \ a).$ \\
	\>		\> $\kmask \ (\iMkPureJoin \ (\iRead \ r_1) \ e \ (\iMkPurify \ r_1 \ w_1) \ w_2) \ \kin$ \\
	\> 		\> $\kcase \ \ilist \ \kof$ \\
	\> 		\> \> $\iNil$			\> $\to \iNil \ r_2 \ b$ \\
	\> 		\> \> $\iCons \ x \ \ixs$	
				\> $\to \iCons$ 
					\> $r_2 \ b \ (f \ x)$ \\
	\>		\> \>   \>	\> $(\isuspend$ \> $(\iList \ r_1 \ a) \ (\iList \ r_2 \ b) \ \bot \ \iMkPure$ \\
	\>		\> \>	\>	\>		\> $(\imapL \ a \ b \ r_1 \ r_2 \ e \ w_1 \ w_2 \ f) \ \ixs)$ 
\end{tabbing}
The inner case-expression in this function has the effect $\iRead \ r_1 \lor e$. The first part is due to inspecting the list constructors, and the second is due to the application of the argument function $f$ to the list element $x$. However, as the recursive call to $\imapL$ is suspended, $\imapL$ itself must be pure. One way to satisfy this constraint would be to pass a witness showing that $\iRead \ r_1 \lor e$ is pure directly to $\isuspend$. This works, but leaves $\imapL$ with a type that contains this (provably pure) effect term. Instead, we have chosen to explicitly mask this effect in the body of $\imapL$. This gives $\imapL$ a manifestly pure type, and allows us to pass a trivial witness to $\isuspend$ to show that the recursive call is pure.

The masking is achieved with the $\kmask \ \delta \ \kin \ t$ expression, which contains a witness of purity $\delta$ and a body $t$. The type and value of this expression is the same as for $t$, but its effect is the effect of $t$ minus the terms which $\delta$ proves are pure. In our $\imapL$ example we prove that $\iRead \ r_1 \ \lor \ e$ is pure by combining two other witnesses, $w_1$ which proves that the list cells are in a constant region, and $w_2$ which proves that the argument function itself is pure. They are combined with the $\iMkPureJoin$ witness type constructor which has the following kind:

\begin{tabbing}
MM \= MMM \kill
	\> $\iMkPureJoin$ $:: \Pi (e_1 : \ !). \ \Pi (e_2 : \ !). $ 
		$\iPure \ e_1 \to \iPure \ e_2 \to \ \iPure{(e_1 \lor e_2)}$ 
\end{tabbing}

Our $\imapL$ example also uses $\iMkPure$, which introduces a witness that the effect $\bot$ is pure. Note that our type for $\imapL$ now contains exactly the constraints that are \emph{implicit} in a lazy language such as Haskell. In Haskell, all algebraic data is constant, and all functions are pure. In our language, we can suspend function applications as desired, but doing so requires the functions and data involved to satisfy the usual constraints of lazy evaluation.








% --- Laziniess in O'CAML ------------------------------------------------------------------------
There is a related problem in strict languages such and O'Caml. In O'Caml we can define an immutable list type as follows.
\begin{tabbing}
MM \= MMMMM \= M \= MMMMM \= MMMM \kill
	\> $\ktype \ 'a \ list \ = \iNil \ | \ \iCons \ \kof \ 'a \ * \ 'a \ \ilist$
\end{tabbing}

Suppose we wrote several list functions using this type, then decide that we need a lazy version of $\imap$ that only creates the list elements when they are demanded by the surrounding program. The standard O'Caml libraries supply a type $'a \iLazy.t$ that represents the value of a suspended computation of type $'a$. The evaluation of expressions is suspended with the $\klazy$ keyword, and suspensions are forced with the $\iforce$ function which has type $`a \ \iLazy. t \to a$. Here is a version of the list type where the tail can be a represented by a suspended computation.
\begin{tabbing}
MM \= MMMMM \= M \= MMMMM \= MMMM \kill
	\> $\ktype \ 'a \ list \ = \iNil \ | \ \iCons \ \kof \ 'a \ * \ ('a \ \ilist) \iLazy.t$
\end{tabbing}

Once again, as we have to change the structure of our type to use a language feature (laziness this time), we now have to go back and refactor existing code. We must insert calls to $\klazy$ and $\iforce$ into every function that operates on this new list structure. Note that even functions that build or consume the list in a strict way must be changed, because the type of the tail has changed. Suppose we wanted to write a functions that 

% -----
section{Regions, destructive update, and mutability constraints}
Another important source of side effects is the destructive update of data. The usual way to introduce destructive update into a functional language is to use reference types. Following \cite{talpin:type-and-effect-discipline} we write $\iRef \ r \ a$ as the type of a reference cell that holds an object of type $a$. The $r$ is a region variable that is used to represent the location and aliasing properties of the reference in the store. To read the value contained in a reference we use the following function:
\begin{tabbing}
MM \= MMMMM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\ireadRef$	\> $:: \forall r \ a. \ \iRef \ r \ a \longtoa{\iRead \ r} a$ 
\end{tabbing}
This function takes a reference, and returns the value contained within. Note that as references are mutable, reading one must be treated as a side effect, hence the $\iRead \ r$ term. We use \% as the kind of regions, so the kinds of $\iRef$ and $\iRead$ are $\iRef :: \% \to * \to *$ and $\iRead :: \% \to \ !$. Updating the value of a reference is accomplished with the $\iwriteRef$ function which has the following type:
\begin{tabbing}
MM \= MMMMM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\iwriteRef$	\> $:: \forall r \ a. \iMutable \ r \To \iRef \ r \ a \to a \longtoa{\iWrite \ r} ()$
\end{tabbing}
This function takes a reference, a new value, and destructively updates the reference to hold the new value. The $\iWrite \ r$ effect records that it updates objects in the region named $r$, and thus \emph{interferes} with any other function that also has an effect on $r$. This interference means that applications of $\iwriteRef$ cannot be reordered with any other functions that access the same region, such as when performing compiler optimisations, without risking changing the meaning of the program. The $\iMutable \ r$ term is a \emph{region constraint} that indicates that only mutable references may be updated. Note that with this formulation, reference cells are not automatically mutable. Instead, they are constrained to be mutable when the are passed to calls to $\iwriteRef$, because the ability to write to a reference requires that it support mutability. If we never write to it, it doesn't need to be mutable.





We use effect typing \cite{lucassen:polymorphic-effect-systems,talpin:type-and-effect-discipline} to track the effects of impure function such as $\iprintSquare$, and annotate its function arrow with the effect it has when it evaluates. We use $\iConsole$ as the effect of reading and/or writing to the console.
 \begin{tabbing}
MM \= MMMMMMM \= MM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\iprintSquare :: \iInt \longtoa{\iConsole} \iInt$ 
	\\ [1ex]
	\> $\iprintSquare \ x$ 	\> $= \kdo \ \{ \ \iprint \ x; \ x * x \ \}$ 
\end{tabbing}
Once we have annoated $\iprintSquare$, we can then modify the type of $\isuspend$ to only accept function parameters which are pure. We do this via an extension to the Haskell type classing system and write:
\begin{tabbing}
MM \= MM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\isuspend :: \forall (a : *) \ (b : *) \ (e : \ !). \iPure \ e \To (a \longtoa{e} b) \longtoa{\bot} a \longtoa{\bot} b$
\end{tabbing}
The variable $e$ is an \emph{effect variable} and we assign it kind $!$, a mneumonic for ``something's happening!''. The term $\iPure \ e$ is an \emph{effect constraint}, which can be constrasted with standard value-type constraints such as $\iEq \ a$ and $\iOrd \ a$. We arrange effects as a lattice, and use $\bot$ as the effect of pure functions. Note that the $\isuspend$ function itself is pure, so we use $\bot$ on the two right-most arrows. However, the parameter function is \emph{constrained} to be pure, so we write $\iPure \ e$. In this paper we usually elide kind annotations on quantified variables, as well as $\bot$ annotations on function arrows, so instead write:
\begin{tabbing}
MM \= MM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\isuspend :: \forall a \ b \ e. \iPure \ e \To (a \longtoa{e} b) \to a \to b$
\end{tabbing}
Type class constraints can also be thought of as logical predicates, so we define:

\bigskip
\begin{tabular}{lll}
$\iPure \ \bot$		& $\equiv$	& $\rtrue$ \\[1ex]
$\iPure \ \iConsole$	& $\equiv$	& $\rfalse$
\end{tabular}
\bigskip

Now, suppose we tried to suspend the application of an impure function, such as $\isuspend \ \iprintSquare \ 5$. This application would give rise to the constraint $\iPure \iConsole$, which is false, indicating a type error. Returning to the definition of $\imap_{LH}$, as the application of the parameter function is suspended, if we use the new type for $\isuspend$ then the type of $\imap_{LH}$ becomes:

\begin{tabbing}
MM \= MM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\imapLH :: \forall a \ b \ e. \ 
			\iPure \ e \To (a \longtoa{e} b) \to \iList \ a \to \iList \ b$ \\
	\> $\imapLH \ f \ \ilist$ \\
	\> \ $= \kcase \ \ilist \ \kof$ \\
	\> \> $\iNil$			\> $\to \iNil$ \\
	\> \> $\iCons \ x \ \ixs$	\> $\to \iCons \ (\isuspend \ f \ x) \ (\imap_{LH}  f \ \ixs)$ 
\end{tabbing}

Note that the purity constraint now appears on the type of the parameter function, so our $\ibadSquares$ example from \S\ref{Strict-and-head-lazy-mapping} is now rejected as desired.





% -- Heap Objects
\begin{tabbing}
MM 	\= Mx \= MMMMMMMM \= 
MM 	\= Mx \= MMMMMMMMMMMM \kill
	\textbf{Alternatives} \> \>  \> \textbf{Heap Objects} \\
	$\ialt$	\> $::=$ 	\> \ $K_i \ \ov{x}^i \to t$
\>	$\iobj$	\> $::=$	\> \ $C_K \ \ov{v}$
\end{tabbing}



\subsection{Expressing T monads in Disciple}
Note that $\trm{T}^\sigma \ a$ style computation types are straightforward to express in Disciple, because we can define data types that have effect parameters. For example, eliding region and closure information we can write:

\medskip
\begin{tabular}{lll}
	$\kdata \ T \ e_1 \ a = \iMkT \ (() \toa{e_1} a)$
\end{tabular}
\medskip

Our $T \ e_1 \ a$ data type simply encapsulates a function that produces a value of type $a$ when applied to the unit value (), while having an effect $e_1$. The monadic return and bind operators are defined as follows:

\medskip
\begin{tabular}{lll}
	$\ireturnT$	
	& $::$	& $\forall a. \ a \to T \ \bot \ a$ 
	\\[1ex]
	\mc{3}{$\ireturnT \ x \ = \iMkT \ (\lambda (). \  x)$}
\end{tabular}

\begin{tabbing}
M	\= MMM \= M \= MMMM \kill
	\> $\ibindT$ 
	\> $::$		
	\> $\forall a \ b \ e_1 \ e_2. \ T \ e_1 \ a \to (a \to T \ e_2 \ b) \to T \ (e_1 \lor e_2) \ b$ 
\end{tabbing}
\vspace{-2em}
\begin{tabbing}
M	\= MMMMMMMMMMM \= MMMMMMMMMMMMMMMM \= MMMM \kill
	\> $\ibindT \ (\iMkT \ f_1) \ \imf_2$
	\> $= \iMkT \ (\lambda (). \ \kcase \ \imf_2 \ (f_1 \ ()) \ \kof$
	\> $\iMkT \ f_2 \to f_2 \ ())$
\end{tabbing}


Although we can directly express T monads in a language with an effect system, the reverse is not true. A monadic system requires all effects to be encapsulated within a computation type such as T, and the function arrow, $\to$, must be pure. However, an effect system allows arbitrary function applications to have effects, and we can add these effects as annotations to the arrows, $\to{\sigma}$.






We now return to the question of how to define a mutable list type. As we will see, we do use reference, but not directly in the definition of lists. We write $\iRef \ r \ a$ as the type of a reference cell that holds an value of type $a$. As before, a reference is only taken to be mutable if its region variable has a $\iMutable$ constraint. To read the value contained in a reference we use the following function:
\begin{tabbing}
MM \= MMMMM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\ireadRef$	\> $:: \forall r \ a. \ \iRef \ r \ a \longtoa{\iRead \ r} a$ 
\end{tabbing}
This function takes a reference, and returns the value contained within. If the reference is mutable then reading it is a side-effect, hence the $\iRead \ r$ term. Updating reference with a new value is accomplished with the $\iwriteRef$ function which has the following type:
\begin{tabbing}
MM \= MMMMM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\iwriteRef$	\> $:: \forall r \ a. \ \iMutable \ r \To \iRef \ r \ a \to a \longtoa{\iWrite \ r} ()$
\end{tabbing}


% -------------------------------------
\subsection{The list type}
If we were to use reference types directly, then we could define the type of updateble lists to be as follows:
\begin{tabbing}
MM \= MMMMM \= M \= MMMMM \= MMMM \kill
	\> $\kdata \ \iList \ r \ a = \iNil \ | \ \iCons \ (\iRef \ r \ a) \ (\iRef \ r \ (\iList \ r \ a))$
\end{tabbing}
Adding a reference in both the head and tail positions of the list allows us to write functions that change the list elements, as well as changing its structure, such as by destructively inserting a new element. However, as discussed in \S\ref{Introduction}, if we were to add references in this way we would no longer be able to use our original $\imap$ function, because it does not call $\ireadRef$ to read the embedded references.



Now, as we would still like to use our $\iwriteRef$ function to help update this list, we will create references to the head and tail on the fly. This is done with the following functions:
\begin{tabbing}
MM \= MMMMMM \= M \= MMMMM \= MMMM \kill
	\> $\irefTo_{\iCons,1}$	\> $:: \forall r \ a. \iList \ r \ a \to \iRef \ r \ a$ \\[1ex]
	\> $\irefTo_{\iCons,2}$	\> $:: \forall r \ a. \iList \ r \ a \to \iRef \ r \ (\iList \ r \ a)$
\end{tabbing}
The $\irefTo_{\iCons,1}$ function creates a reference to the head of a $\iCons$-cell, and $\irefTo_{\iCons,2}$ creates a reference to its tail. Applying these functions to a $\iNil$ list causes a run-time error. Note that the references returned by these functions point \emph{inside} the supplied $\iCons$-cell. For example, if we evaluate $\ilist = [1, 2, 3]$ and then $\iref = \irefTo_{\iCons,2} \ilist$ then the following objects are produced in the store:

\begin{center}
\includegraphics[scale=0.5]{fig/list123-refTail}
\end{center}

When we use $\iwriteRef$ to update the value of $\iref$, it is the tail pointer in the first $\iCons$-cell that is modified. Note that in the types of $\irefTo_{\iCons,1}$ and $\irefTo_{\iCons,2}$, the returned reference shares the same region variable as the list. This means that if we pass the reference to $\iwriteRef$ then the list is also marked as mutable.



% --- Several Region Variables ------------------------------------------------
\subsection{Types with Several Region Variables}
Algebraic data types can contain more than one region variable. For example, we could define a vector of two integers as follows:
\medskip

\begin{tabular} {lll}
	& $\kdata \ \iListInt \ r_a \ r_b = \iINil \ | \ \iICons \ (\iInt \ r_b))$ \\[1ex] 
	& $\ivec = \iICons \ r_1 \ (2 \ r_2) \ (\iICons \ r_1 \ (3 \ r_2) \ (\iINil \ r_1))$
\end{tabular}

Note that the outer $\iList$ constructor is in region $r_1$, while the two integer objects are in regions $r_2$ and $r_3$. Having three region variables in this type gives us three degrees of freedom for mutability. Constraining $r_1$ to be mutable allows us to update the pointers in the $\iVec$ constructor so they point to different objects. Constraining $r_2$ or $r_3$ to be mutable allows us to update the values in the integer objects directly.

\begin{center}
\includegraphics[scale=0.6]{fig/list-regions}
\end{center}

Note that the outer $\iList$ constructor is in region $r_1$, while the two integer objects are in regions $r_2$ and $r_3$. Having three region variables in this type gives us three degrees of freedom for mutability. Constraining $r_1$ to be mutable allows us to update the pointers in the $\iVec$ constructor so they point to different objects. Constraining $r_2$ or $r_3$ to be mutable allows us to update the values in the integer objects directly.



\subsection{Updating algebraic data}

Here is an example function that destructively inserts a new element into a list.

\begin{tabbing}
MM 	\= MMMMMM \= MMMMMM \= MM \= MMx \= MMM \= MMM \kill
	\> $\iinsertAfter$ \> $:: \forall r_1 \ r_2 \ a. \ \iInt \ r_1 \to a \to \iList \ r_2 \ a \longtoa{e_1} ()$ \\
	\>		\> $\rhd \ e_1 = \iRead \ r_1 \lor \iRead \ r_2 \lor \iWrite \ r_2, \ \iMutable \ r_1$  
\end{tabbing}
\vspace{-1em}
\begin{tabbing}
MM 	\= MM \= MMMMMM \= MM \= MMx \= MMM \= MMM \kill
	\> $\iinsertAfter \ \iindex \ \ielem \ \ilist$	\\
	\> \ $= \kcase \ \ilist \ \kof$	\\
	\> 	\> $\iNil$		\> $\to \ierror \ ...$ \\
	\> 	\> $\iCons \ x \ \ixs$	\> $\to \kif \ \iindex == 0$ \\
	\> 	\>			\> \> $\kthen$ 
						\> $\iupdate_{Cons,1} \ \ilist \ (\iCons \ \ielem \ \ixs)$ \\
	\> 	\>			\> \> $\kelse$ \> $\iinsertAfter \ (\iindex-1) \ \ielem \ \ixs$
\end{tabbing}

Note that in the type signature for $\iinsertAfter$, the $\iRead \ r_1$ effect comes from comparing and subtracting the $\iindex$ value. The $\iRead \ r_2$ effect is due to the inspection of the list by the case-expression, and the $\iWrite \ r_2$ effect comes from updating it. The fact that $\iinsertAfter$ reads the constants 0 and 1 is not observable to calling functions, so the effects on these values can be masked.


\textbf{No fabricated region witnesses (nofab)}: Region witnesses constructors may only be used in the witness list associated with a $\kletregion$, and not in a type applied directly to a term. This ensures that conflicting witnesses cannot be created in other parts of the program. For example:
$$
\begin{aligned}
	& \kletregion \ r \ \kwith \ \{ w_1 = \iMkConst \ r \} \ \kin \\
	& \dots \ \iupdate_{\iCons,1} \ (\iMkMutable \ r) \ t_1 \ t_2 \ \dots
\end{aligned}
$$


The term $\kletregion \ r \ \kwith \ \{ \ov{w_i = \delta_i} \} \ \kin \ t$ binds a region variable $r$ which is in scope in both the witness bindings $\ov{w_i = \delta_i}$ and the body $t$. The witness bindings set the properties of the new region, and introduce witnesses to those properties at the same time. The use of $\kletregion$ imposes some additional syntactic constraints on the program which ensure that conflicting region witnesses cannot be created.
\smallskip

The $\iupdate_{K,i}$ operator takes the location of a store object and a new value. If the constructor tag in the object matches $K$, then its $i$-th field is updated with the new value. The update function also requires a witness that the object to be updated is in a mutable region. If the constructor tag in the object does not match $K$, then evaluation fails with a run-time error.

\textbf{Well-formedness of region witnesses}: In the list of witness bindings $\ov{w_i = \delta_i}$, each $\delta_i$ must be either $\iMkConst \ r$ or $\iMkMutable \ r$, and the list may not mention both. Note that although we have only presented two region constraints so far, as our system naturally extends to others we associate a \emph{list} of witnesses with $\kletregion$ and include this rule. We discuss the $\iBlocked$ constraint in \S\ref{conclusion}.


\begin{tabbing}
MM \= MMM \= MM \= MM \= MMMMM \= MM \kill
\> $\islowSucc :: \forall r_1 \ r_2. \ \iInt \ r_1 \longtoa{\iRead \ r_1} \iInt \ r_2$ \\
\> $\islowSucc =$ \\
\>	\> $\Lambda r_1 \ r_2. \ \lambda (x : \iInt \ r_1)$ \\
\> 	\> $\kletregion \ r_3 \ \kwith \ \{ w = \iMkMutable \ r_3 \} \ \kin $ \\
\>	\> $\klet$ 	\> $(y$  \> $: \iInt \ r_3)$	\> $= \icopyInt \ r_1 \ r_3 \ x$ \\
\>	\> 		\> $(\_$ \> $: ())$		\> $= \iupdateInt \ r_3 \ r_1 \ w \ y \ x$ \\ 
\>	\> $\kin$	\> $\icopyInt \ r_2 \ r_3 \ y$
\end{tabbing}




Now, if we take $x$ to have the type $\iInt \ r_5$, the application $\isuspend \ \isucc \ x$ leads to the effect constraint $\iPure \ (\iRead \ r_5)$, but $\iRead \ r_5$ is not the $\bot$ which this constraint requires. However, suppose $r_5$ was constant. Read effects on constant regions can be safely ignored, because it does not matter when a particular read takes place, the same value will be returned each time. We satisfy the $\iPure \ (\iRead \ r_5)$ constraint by \emph{purifying} the $\iRead \ r_5$ effect, that is, we require $x$ to have the type $x :: \iConst \ r_5 \To \iInt \ r_5$. During type inference, if a region variable such as $r_5$ already has a mutability constraint then it cannot additionally be made constant. In this case our system reports a \emph{purity conflict}. The error message includes the location of the term that caused the region to be constrained as mutable, along with the suspension that requires it to be constant.

For example, consider the following erroneous program fragment:
\begin{tabbing}
MM \= MM \= MMM \= MMMMMMM \= MMMM \kill
	\> \kdo \> $x$			\> $= 5$ \\
	\> 	\> $\isix$		\> $= \isuspend \ \isucc \ x$  \\
	\>	\> ... \\ 
	\>	\> $\iupdateInt \ x \ 23$ \\
	\>	\> ... \\
	\>	\> $\iprint \ \isix$ 
\end{tabbing}



% --- counter example impure functions being suspended


 In particular, the constraints on $\imapL$ ensure that the following erroneous program is rejected:
\begin{tabbing}
MM \= MM \= MMM \= MMMMMMM \= MMMM \kill
	\> \kdo \> $\ixs$		\> $= [1, 2, 3]$ \\
	\> 	\> $\iys$		\> $= \imapL \ \isucc \ \ixs$  \\
	\>	\> ... \\ 
	\>	\> $\iinsertAfter \ 1 \ 5 \ \ixs$ \\
	\>	\> ... \\
	\>	\> $\iprint \ \iys$ 
\end{tabbing}

This program is similar to the one from \S\ref{Witnesses:Purity} except that now we are using a higher order function $\imapL$. Note that if the list $\iys$ is not demanded until after the application of $\iinsertAt$, then this program will print $[2, 3, 6, 4]$ instead of $[2, 3, 4]$, a behaviour we reject as invalid.


% --- Soundness

It is impossible to create a witness with kind $\iPure \ (\iWrite \ r)$. It is also impossible to create one of kind $\iPure \ (\iRead \ r)$ if one of kind $\iMutable \ r$ can also be created. To see why this is, recall from \S\ref{Witnesses:Constancy-and-Mutability} that the restriction on where $\iMkConst$ and $\iMkMutable$ can be used prevents witnesses of kinds $\iMutable \ r$ and $\iConst \ r$ from existing in the same program, for the same variable $r$. As $\iMkPurify$ is the only way to produce a witness of the form $\iPure \ (\iRead \ r)$, and 

serves as the only bridge between witnesses proving properties of regions and witnesses proving properties of effects, applications of impure functions cannot be suspended.

As a counter example, consider what would happen if we introduced a type variable $\ibadness$ into the type environment which had the kind $\iPure \ (\iWrite \ r_1)$.
\begin{tabbing}
MM \= MM \= MM \= MMMMMMM \= MMMMM \= MMMM \kill
	\> $\Lambda r_2.$ \\
	\> $\kletregion \ r_1 \ \kwith \ \{ w = \iMkConst \ r_1 \} \ \kin$ \\
	\> $\klet$	\> $(x$		\> $: \iInt \ r_1)$	\> $= 5 \ r_1$ \\
	\> 		\> $(\isix$	\> $: \iInt \ r_2)$	\> $= \isuspend$ \> $(\iInt \ r_1) \ (\iInt \ r_2) \ (\iRead \ r_1)$ \\
	\>		\>		\>			\> 		 \> $(\iMkPurify \ r_1 \ w) \ \isucc \ x$ \\
	\>		\> ... \\ 
	\>		\> $(\_$	\> $: ())$		\> $= \iupdateInt \ r_1 \ r_2 \ \ibadness \ x \ (23 \ r_2)$ \\
	\> $\kin$	\> ... \\
\end{tabbing}
As the application of $\isucc$ is suspended, its result will only be computed when it is demanded. However, the $\iupdateInt$ statement destructively updates the $x$ value, so if the thunk is not forced before this update, then in the body of the let-expression the $\isix$ will have the value $24$ instead of $6$.

Note that this behaviour is not \emph{unsound} in the sense that the program will crash, fail, encounter a runtime type error or otherwise ``go wrong''. However, permitting such programs would prevent us from performing optimisations that change the order in which values are inspected. In a sense, we require suspended function applications to be pure because we do not associate effects with value types such as $\iInt \ r$. We require thunks to act like ``values'', even though such values are represented by suspended computations. As per Haskell, we allow the inspection of a value to diverge, but not to exhibit any other computation-like behaviour. 
