
% -----------------------------------------------------------------------------
\section{Regions, Effects and Purity}
In Haskell and ML, references and arrays are distinguished values, and are the only ones capable of being destructively updated. This means that the structure of mutable data is necessarily different from the structure of constant data, which makes it difficult to write polymorphic functions that act on both. For example, if we use $\iIORef~\iInt$ as the type of a mutable integer and $\iInt$ as the type of a constant integer, then we would need $\ireadIORef$ to access the first, but not the second. On the other hand, if we were to treat all data as mutable, then every function would exhibit a side effect. This would prevent us from using code-motion style optimisations that depend on purity.

Instead, we give integers the type $\iInt~r$, where $r$ is a region variable, and constrain $r$ to be mutable or constant as needed. Our use of region variables is similar to that by \cite{talpin:type-and-effect-discipline}, where the variable $r$ is a name for a set of locations in the store where a run-time object may lie. However, we do not use regions for memory management as per \cite{tofte:mlkit-4.3.0}, due to the difficulty of statically determining when objects referenced by suspended computations can be safely deallocated. We define region variables to have kind $\%$, and use this symbol because pictorially it is two circles separated by a line, a mnemonic for ``this, or that''. The kind of value types is *, so the $\iInt$ type constructor has kind $\iInt :: \% \to *$. In our core language, a literal such as `5' is a data constructor that allocates a new boxed literal. For example, `5' has the following type:
\code{
	5  &::& \forall (r : \%).() \longtoa{\iAlloc~ r}~Int \ r
}
As in \cite{talpin:type-and-effect-discipline} we annotate function types with their latent effects, using $\iRead$, $\iWrite$ and $\iAlloc$ as the atomic effects. We organise compound effects as a join semi-lattice, collecting atomic effects with the $\lor$ operator. We use $\bot$ as the effect of a pure function, and unannotated function arrows are taken to have this effect. We also use a set-like subtraction operator where the effect $\sigma \setminus \sigma'$ contains the atomic effects that appear in $\sigma$ but not $\sigma'$. We use $!$ as the kind of effects, so $\iAlloc$ has kind $\iAlloc:: \% \to~ !$. The symbol ! is a mnemonic for ``something's happening!''. For the rest of this paper we will elide explicit kind annotations on binders when they are clear from context. 

When the size of an effect term becomes large, writing it directly over its function constructor ($\to$) becomes cumbersome. For this reason we sometimes introduce a new variable and write the effect of a function separately, such as:
\code{
	5  	&::	& \forall (r : \%).~() \longtoa{e_1}~ Int~r \\
		&\rhd	& e_1 = \iAlloc~ r
}
The symbol $\rhd$ is pronounced ``with''. Note that this new variable $e_1$ had been introduced for convenience only, is not quantified, and is not a parameter of the type. Writing effects this way is syntactic sugar, and $\rhd$ is not part of our formal type language. We can always translate such a sugared type back to the ``real'' type by writing all effect expressions over their corresponding arrows. 

Returning to the type of `5' we note several things. Firstly, the fact that `5' is a function which performs allocation is only directly visible in our core language. In the Disciple source language, the programmer can blissfully write $2 + 5$, and the appropriate `()' arguments are inserted automatically. Secondly, in DDC core we really do want `5' to be a function, because as we shall see in the next section, we allow the resulting boxed object to be destructively updated. Thirdly, as we shall see in \S\ref{section:constancy-and-constraint-exclucivity} if we know that we \emph{don't} want to update the returned object, then we can constrain the associate region to be, which will allow us to mask the $\iAlloc~ r$ effect. Finally, in \TODO{ref} we will show how to exploit information about constancy to use unboxed operations and avoid the actual allocation altogether. 


% -----------------------------------------------------------------------------
\subsection{Updating Integers}
\label{Update:UpdatingIntegers}
To update an integer we use the $\iupdateInt$ function which has type:
\code{
	updateInt
	 & ::	& \forall  r_1 r_2
			.~ Mutable~ r_1 
			\To~ Int~ r_1 
			\to~ Int~ r_2 
			\longtoa{\iRead~ r_2 ~\lor~ \iWrite~ r_1} ()			
}
This function reads the value of its second argument, and uses this to overwrite the first. The term $\iMutable~ r_1$ is a \emph{region constraint} that ensures that only mutable integers can be updated. When we apply $\iupdateInt$ we must pass a \emph{witness} (proof term) that guarantees that this constraint is satisfied, a point we discuss further in \S\ref{Witnesses}. Note that there is no temporal ordering implied by the way the effect $\iRead~ r_2 \lor \iWrite~ r_1$ is written. Operationally, $\iupdateInt$ must read its source before writing to its destination, but this information is not encoded by the type.


% -----------------------------------------------------------------------------
\subsection{Constancy and Constraint Exclusivity}
\label{section:constancy-and-constraint-exclucivity}
Suppose that we wish to \emph{prevent} a particular value from being updated. In this case we add a $\iConst$ constraint to the corresponding region variable. For example, we can write:
\code{
	pi	&::& Const \ r \To Float \ r
}
In our system we intend for the $\iConst$ and $\iMutable$ constraints to have the same meaning as the \texttt{const} and \texttt{mutable} type qualifiers of C \cite{foster:type-qualifiers}. However, note that Haskell-style type class constraints do not provide an equivalent exclusivity property. For example, suppose we also added a $\iMutable$ constraint to the above type:
\code{
	pi	&::& Mutable~ r \To Const~ r \To Float~ r
}
Although this type looks suspect, it is perfectly valid. That is, valid but not useful. We can write a term that is assigned this type, but such a term cannot be used. To access the inner $\iFloat$ we would need to pass witnesses that guarantee both the mutability and constancy of $r$, and we ensure that both of these cannot exist in the same program. The mechanism we use to achieve this is discussed in \S\ref{Witnesses}. 

Note that in our \emph{core} language it is possible to constrain a type to be both mutable in constant, but as this is a suspect operation, in our source language we flag it as an error it. We could perhaps add an auxiliary check to the core language to detect suspect constraints as well, but as they cannot actually ``break'' anything, we have not felt the need to so far.

For comparison, note that Haskell allows the programmer to constrain a type variable to be both $\iFractional$ and $\iIntegral$, even though the natural meaning of these constraints would imply that there should be no types that are instances of both. This is valid behaviour because Haskell type classes are \emph{open}, meaning new instances may be declared at any time. Perhaps a client programmer will define a new type where it makes sense for it to be both $\iFractional$ and $\iIntegral$, and give the required instances. In contrast, it is \emph{never} valid to discharge both constraints on our $\ipi$ example above, so we ensure this cannot be done. Doing so would cause optimisations that that depend on constancy of data, such as the full laziness transform, to become unsound. By this we mean that if we optimise a program assuming that some specific data is constant, but then it gets destructively updated anyway, then we cannot guarantee that the meaning of the unoptimised version is preserved.


% -----------------------------------------------------------------------------
\subsection{Updating Algebraic Data}
Along with primitive types such as $\iInt$ and $\iFloat$, the definition of an algebraic data type may also contain region variables. For example, we define our lists as follows:
\code{
	\mc{3}{\kdata~ List~ r~ a~ \kwhere} \\
	~~ Nil~	  &::&	\forall r~ a.~ () \longtoa{\iAlloc~ r} List~ r~ a \\
	~~ Cons~  &::&	\forall r~ a.~ a \to List~ r~ a~ \longtoa{\iAlloc~ r} List~ r~ a
	
}

Note that in our source language we have sugar that allows to programmer to omit the allocation effect and return type, but in core we simply write out the complete type of each constructor. Note that as in \TODO{ref} we have applied the $\iList$ constructor to a region variable ($r$). This variable identifies the region that contains the list cells, and can be constrained to be constant or mutable as needed. In the type of $\iNil$, the fact that $r$ only appears on the right of an arrow indicates that a freshly allocated $\iNil$ object is guaranteed not to alias with any existing objects. On the other hand, in the type of $\iCons$, the second argument and return type share the same region variable $r$, which means the new cons-cell is allocated into the same region as the existing cells. For example, the evaluation of the following expression produces the store objects shown below.
\code{
	list	&::& List~ r_5~ (Int~ r_6) 
\\
	list	&=&  Cons~ r_5~ (Int~ r_6)~ 
			(2~ r_6)~
			(Cons~ r_5~ 
				(Int~ r_6)~ 
				(3~ r_6)~ 
				(Nil~ r_5~ 
					(Int~ r_6)))
}

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

As the list cells and integer elements are in different regions, we can give them differing mutabilities. For example, if the type of $\ilist$ was constrained as follows, then we would be free to update the integer elements, but not the spine:
\code{
	list	
	 &::&	Const~ r_5
			\To \iMutable~ r_6
			\To \iList~ r_5~
				(\iInt~ r_6)
}
The definition of an algebraic type also introduces a set of update operators, one for each updatable component of the corresponding value. For our list type, as we could usefully update the head and tail pointers in a cons-cell, we get:
\code{
	update_{Cons, 0}
	 &::&	\forall r~ a.~
		Mutable~ r 
		\To \iList~ r~ a 
		\to a 
		\longtoa{\iWrite \ r} ()
\\
	update_{Cons, 1}
	 &::&	\forall r~ a.~
		Mutable~ r
		\To \iList~ r~ a
		\to \iList~ r~ a
		\longtoa{\iWrite \ r} ()
}

These operators both take a list and a new value. If the list contains an outer cons-cell, then the appropriate pointer in that cell is updated to point to the new value. If the list is not a cons, then a run-time error is raised.


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

\begin{flushleft}
\begin{tabular}{cc}
	\begin{minipage}{18em}
	$\kdata~ \iVec~ r_1~ r_2~ r_3~ \kwhere$ \\
	$~~~~ V ::  \iInt~ r_2 \to \iInt~ r_3 \longtoa{\iAlloc~ r_1} \iVec~ r_1~ r_2~ r_3 $ \\

	$\ivec = V~ r_5~ r_6~ r_7~ (9~ r_6)~ (5~ r_7)$
	\end{minipage}
	& 
	\begin{minipage}{13em}
	\includegraphics[scale=0.6]{fig/vector-regions}
	\end{minipage}
\end{tabular}
\end{flushleft}

\medskip
Note that the outer $V$ constructor is in region $r_5$, while the two integer objects are in regions $r_6$ and $r_7$. Having three region variables in this type gives us three degrees of freedom for mutability. The first variable $r_5$ is called the \emph{primary region variable} and corresponds to the outer constructor of the structure. Constraining this variable to be mutable allows us to update the pointers so they point to different objects. Constraining $r_6$ or $r_7$ to be mutable allows us to update the values in the integer objects directly.

Once again, note that all objects in the above structure are potentially mutable. Also, note that we do not need to modify the shape of their types, such as by inserting $\iRef$ constructors, to achieve this. We call this property \emph{arbitrary destructive update}.


% ------------------------------------------------------------------------------
\subsection{Laziness and Purity Constraints}
\label{section:laziness-and-purity-constraints}
Although we use call-by-value evaluation as the default, we can also suspend the evaluation of an arbitrary function application using the $\isuspend$ operator:
\code{
	\isuspend		
	 &::& \forall a~ b~ e.~ Pure~ e~ \To (a \toa{e} b) \to a \to b
}
The $\isuspend$ operator 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 $\kcase$-expression or primitive operator such as $\iupdate$. The constraint $\iPure \ e$ indicates that only function applications that do not exhibit visible side effects may be suspended. 

As usual, once an application has been suspended, determining \emph{when} it will finally be evaluated can be very difficult. Adding the purity constraint ensures that programs using laziness return predictable results, independent of when their thunks happen to be forced. This makes code analysis substantially easier, for both the programmer and compiler. Specifically, during optimisation we are free to suspend any pure function application, as this is guaranteed not the affect the ultimate result of the computation. We discuss this property further in \TODO{ref}. Note that in the semantics of a purely functional lazy language such as Haskell, every function application is automatically suspended, and thus comes with its own implicit purity constraint. By making both suspension and purity \emph{explicit}, we gain another degree of freedom, which allows us to support impure features such as arbitrary destructive update as well.

\smallskip
% -------------------------------------
\begin{flushleft}
\textbf{Design Descision:} Use $\iPure$ constraints instead of bottom effects on parameter functions.
\end{flushleft}
Consider the type of $\isuspend$ from the previous section. Here it is again, but with the elided $\bot$ effect annotations on the two right-most arrows added back in:
\code{
	\isuspend		
	 &::& \forall a~ b~ e.~ Pure~ e~ \To (a \toa{e} b) \toa{\bot} a \toa{\bot} b
}
Instead of using the $\iPure$ constraint, it would be possible to adjust the language design so that the purity of parameter functions was expressed by writing $\bot$ directly on the corresponding function arrow, like so:
\code{
	\isuspend		
	 &::& \forall a~ b.~ (a \toa{\bot} b) \toa{\bot} a \toa{\bot} b
}
Another option would be to name the effect of \emph{all} function arrows, and provide corresponding constraints:
\code{
	\isuspend		
	 &::& \forall a~ b~ e_1~ e_2~ e_3.~ Pure~ e_1 \To \iPure~ e_2 \To \iPure~ e_3~ \To (a \toa{e_1} b) \toa{e_2} a \toa{e_3} b
}
There are several reasons why we have chosen the first approach over the others. Firstly, note that the constraint $\iPure~ e$ naturally expresses a restriction on the possible values we can use for the first parameter of $\isuspend$. As we will see in \TODO{ref}, we can pass a parameter function that reads constant data, but not one that performs visible writes, as this not a pure action. In contrast, the $\bot$ annotations on the two right-most arrows don't correspond to restrictions. Rather, applying the $\isuspend$ function to its two arguments simply has no visible effect. If we were to add $\iPure$ constraints to the two right-most arrows, as in the third signature, then this wouldn't be helpful because these arrows naturally have effect $\bot$, which already satisfies the constraints.

The second signature is a more reasonable option than the third, but we have chosen not to use this form for two reasons: it would require an extra typing rule to support casting of effects on arrows, and it doesn't mate well with our type inference algorithm. For example, suppose we want to suspend an application of the following function:
\code{
	\isucc & :: & \forall r_1~ r_2.~ \iInt~ r_1 \longtoa{\iRead~ r_1 \lor \iAlloc~ r_2} \iInt~ r_2
}
The function $\isucc$ reads its integer argument, from any region, and returns a freshly allocated object containing the successor. To suspend an application of $\isucc$ using the first signature for $\isuspend$, we must satisfy the constraint $\iPure~ (\iRead~ r_1 \lor \iAlloc~ r_2)$. As discussed in \TODO{ref}, we do this by passing a witness to the fact that the effect is indeed pure. The witness passing mechanism comes ``for free'', because witnesses are just type information, and we already have type application (and abstraction) from System-F. In contrast, to use the second signature for $\isuspend$ we would need to cast the (instantiated) type of $\isucc$ to $\iInt~ r_1 \toa{\bot} \iInt~ r_2$. This casting would be an additional mechanism requiring an additional typing rule. \TODO{maybe eta-expand and mask the body, no have to create a new function}

With regards to type inference, we use an extended version of the system described in \TODO{cite}. This system names the effect of each function arrow with a variable, and returns more-than constraints for the variables. For example, performing type inference for a version of $\isucc$ would yield the following, where $\rhd$ separates the body of the type from the constraints on it:
\code{
	\isucc	& :: 	& \forall~ r_1~ r_2~ e_1.~ \iInt~ r_1 \longtoa{e_1} \iInt~ r_2 \\
		& \rhd	& e_1 \tme \iRead~ r_1 \lor \iAlloc~ r_2
}
Now, from a type inference mindset, the second signature for $\isuspend$ isn't particularly helpful. To suspend an application of $\isucc$ we would need to add a constraint such as $e_1 = \bot$ or $e_1 \tle \bot$, but general equality or less-than constraints on effect variables aren't a natural part of the Type and Effect Discipline \TODO{cite}. We also don't have a reason for the right of the constraint to be anything other than $\bot$. However, we \emph{do} support Haskell-style type class constraints on value types anyway, so adding $\iPure$ is a simple matter of extending the mechanism to support constraints on effect types as well as value types. Type inference and conversion between the inferred and core types is discussed further in \TODO{cite}.

