Suppose we are writing a compiler and need to define a data type to represent variables. We distinguish two sorts of variables, those taken from the source code, and fresh `dummy' variables which the compiler introduces itself. The source variables will be identified by their names, which we assume to be unique, and dummy variables will be numbered.

\begin{tabbing}
MM \= MM \kill
	\> $\kdata \ \iVar = \iSourceVar \ \iString \ | \ \iDummyVar \ \iInt$
\end{tabbing}

We will maintain a counter to generate new dummy variables. As many functions in our compiler will need to allocate fresh variables, we define this counter at top level, and use destructive update to increment it.

\begin{tabbing}
MM \= MM \kill
	\> $\icounter :: \iInt$ \\
	\> $\icounter = 0$
\end{tabbing}

\begin{tabbing}
MM \= MMM \= MMMM \= MMMM \kill
	\> $\inewVar :: () \to \iVar$ \\
	\> $\inewVar \ ()$ \\
	\> \ $ =\kdo$	\> $\ivar$	\> $= \iDummyVar \ (\icopy \ \icounter)$ \\
	\>		\> $\icounter$	\> $:= \icounter + 1$ \\
	\>		\> $\ivar$ 
\end{tabbing}

Our do-expressions contain a sequence of statements or non-recursive bindings, end with a statement, and are executed top to bottom. The value of the whole expression is the value of the last statement. We treat the statement $\icounter := \icounter + 1$ as sugar for $(:=) \ \icounter \ (\icounter + 1)$, where the $(:=)$ function updates its first argument with the value from the second. Our $\iInt$ type is boxed, so it is the counter object in the heap which is being updated.

Here is a data type to represent our abstract syntax tree, and a function to normalise it so the left of an application is always a value. 

\begin{tabbing}

\end{tabbing}

By definition, the application of an impure function to a given argument in a different context may return a different result. This means that changing the evaluation order of two impure functions can change their results. As the evaluation order of lazy programs can be very hard to characterise, when writing them we usually restrict ourselves to pure functions, and only use impure features in carefuly controlled circumstances. 


% This is true even when compiling a ``purely functional language'' \cite{sabry:purely} such as Haskell, as the language may be pure, but the programs written in it are not. Haskell is also lazy, and most implementations of laziness are based totally around the destructive update of thunks that represent suspended computations.



The machines that our programs run on are not pure functions, so when compiling them to object code we must inevitably introduce impure features such as IO and destructive update. However, during compilation we should not treat \emph{all} parts of a program as having side effects, as some powerful compiler optimisations such as the full laziness transform are only applicable to the pure fragments of a program. If we apply such optimisations to the impure fragments then we risk changing the meaning of the program. 

Suppose we are designing an intermediate language for our compiler. There are three overall approaches that we could take with respect to effects. Firstly, if the source language is pure then we could make the core language pure as well. This effectively ignores the problem, leaving it for subsequent intermediate languages to deal with. 

Secondly, we could leave the order in which impure functions are performed as undefined. By ``leave undefined'' we mean perhaps determined by the language semantics, but not always preserved by the compiler. For example, order of evaluation in GHC's core language \cite{sulzmann:system-Fc} is determined by its semantics, but compiler optimisations are not guaranteed to preserve this order. In practice, the evaluation order of impure functions is constrained by adding extra data dependencies via the state thread encoding. These extra dependencies ensure that evaluation order is not perterbed during optimisation, but the compiler does not reason about impurity directly.

Finally, we could treat impurity in disciplined way, expressing it as type information with an effect system \cite{lucassen:polymorphic-effect-systems,talpin:type-and-effect-discipline}, or with monadic computation types. This approach has the advantage that compiler optimisations can be guided by effect information, but such systems have so far only been applied to strict languages. One of the main considerations is that the evaluation of impure functions should not be suspended, either by the source program or in subsequent optimisations. Doing so would make the evaluation order of such functions dependent on the surrounding program, potentially changing its end result.

This paper shows how to use purity, constancy and mutability constraints to reason about side effects in an intermediate language that supports mixed strict and lazy evaluation. Our motto is ``purity requires constancy'', meaning that a function is only pure if all the data it reads is constant. Our language allows arbitrary data structures to be destructively updated, but such updates are only permitted to be visible to the strict fragments of the program, where evaluation order is well defined.

This system has been implemented in the Disciplined Disciple Compiler, where ``Disciple'' is the name of the language it compiles and ``Disciplined'' refers to our approach to effects. Although our core language is based on System-F, we will omit type abstractions and applications until we formally define it in \S\ref{Language}. Type inference and translation from the source to the core language is similar to that for Haskell compilers, and is discussed further in ... The next few sections discuss the motivation for our approach, \S\ref{Effect-typing-and-purity-constraints} .... and so on.


% --- 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. 
