

% -------------------------------------------------------------------------------------------------
\section{Witnesses of Distinctness}
\label{WitnessesOfDistinctness}
In the example in the previous section we eliminated the second call to $\iunbox$ by specialising for the case where the first argument was constant. This got the job done, but was a bigger hammer than necessary. The only property that we really needed was that the two arguments did not alias, that is, they were distinct. With this in mind, we define a new witness kind and its associated constructor that expresses this directly.

\code{
\iDistinct	& :: \% \to \% \to \Diamond 					& (\trm{witness kind constructor}) \\
\iMkDistinct 	& :: \Pi(r_1 : \%). \Pi(r_2 : \%).~ \iDistinct~ r_1~ r_2	& (\trm{witness type constructor})
}

A witness of kind $\iDistinct~ r_1~ r_2$ guarantees that regions $r_1$ and $r_2$ are not aliases, meaning that objects in region $r_1$ do not alias objects in region $r_2$. We write the type level witness as $\un{\rdistinct~ \varphi_1~ \varphi_2}$, for some region types $\varphi_1$ and $\varphi_2$. Before discussing how these witnesses are introduced into the program, we will revisit the example from the previous section. This time, we specialise it for the case where the two arguments are distinct, without also requiring that the first is constant:

\code{	
	\mc{5}{\Lambda r_1~ r_2.~ 
		\Lambda (w_1 : \iDistinct~ r_1~ r_2).~ 
		\Lambda (w_2 : \iMutable~ r_2).~ 
		\lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{4}{\kletregion~ r_3~ \kwith~ w_3 = \iMkConst~ r_3~ \kin} \\
	\klet	& (x_1	& \hspace{-1em}: \iInt_\#)
				& = \iunbox~ r_1~ x 
				& \iRead~ r_1
		\\
		& \_	& 	& = \iupdateInt~ r_2~ r_3~ w_2~ y~ (0~ r_3) 
				& \iRead~ r_3 \lor \iWrite~ r_2
		\\
	\kin	& \mc{3}{\ibox~ r_1~ (\iadd_\#~ x_1~ (\iunbox~ r_3~ (\ibox~ r_3~ (\iadd_\#~ x_1~ 1_\#))))}
				& \bot
}

As we have this new witness, the effects $\iRead~ r_1$ and $\iWrite~ r_2$ are guaranteed not to interfere. Due to this, it is also safe to move the $x_1$ binding across the call to $\iupdateInt$ so that is closer to its use site. This will help to reduce the number of registers required when compiling to native machine code. We can also apply the $\iunbox/\ibox$ identity to yield our final version:

\code{	
	\mc{5}{\Lambda r_1~ r_2.~ 
		\Lambda (w_1 : \iDistinct~ r_1~ r_2).~ 
		\Lambda (w_2 : \iMutable~ r_2).~ 
		\lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{4}{\kletregion~ r_3~ \kwith~ w_3 = \iMkConst~ r_3~ \kin} \\
	\klet	& \_	& 	& = \iupdateInt~ r_2~ r_3~ w_2~ y~ (0~ r_3) 
				& \iRead~ r_3 \lor \iWrite~ r_2
		\\
		& (x_1	& \hspace{-1em}: \iInt_\#)
				& = \iunbox~ r_1~ x 
				& \iRead~ r_1
		\\
	\kin	& \mc{3}{\ibox~ r_1~ (\iadd_\#~ x_1~ (\iadd_\#~ x_1~ 1_\#))}
				& \bot
}

With this code, although there is nothing preventing a caller from instantiating both $r_1$ and $r_2$ with the same type (say, $\un{\rho_5}$) our system ensures that the resulting function cannot be called. We do this by ensuring that there is no way to produce a witness of kind $\iDistinct~ \un{\rho_5}~ \un{\rho_5}$. In fact, this part turns out to be surprisingly easy.

As with witnesses of constancy and mutability, we tie the creation of witnesses of distinctness to $\kletregion$. Recall from EvLetRegion in Fig. \ref{fig:TermEvaluation} that the reduction of an expression such as $\kletregion~ r~ \kwith ~\{\ov{w_i = \delta_i}\}~ \kin~ t$ first allocates a fresh region label $\rho$, then substitutes the handle $\un{\rho}$ for all occurrences of $r$ in both the witness set $\ov{\delta_i}$ and the body $t$. The fact that $\un{\rho}$ is fresh means that it cannot alias with any existing handles. Also, as region handles do not appear in binding positions, they behave like type constructors and are not substituted for one another. Clearly, we must prevent terms such as $\iMkDistinct~ r_1~ r_1$ from appearing in the initial program, but as with $\iMkConst$ and $\iMkMutable$, requiring all occurrences of $\iMkDistinct$ to appear in the witness set associated with a $\kletregion$ reduces this to a simple syntactic check. For example, consider the following function:

\code{
	\Lambda (r_1 : \%).~ ... \\
	\kletregion~ r_2~ \kin~ ... \\
	\kletregion~ r_3 \kwith~ \{ w_3 = \iMkDistinct~ r_1~ r_3;~ w_4 = \iMkDistinct~ r_2~ r_3 \}~ \\
	\kin~ ... ~w_3~ ... ~w_4~ ... \\
}

Now, suppose we apply this function to the region handle $\un{\rho_1}$, and then reduce the outer $\kletregion$. Doing this leaves us with the following state:

\code{	H, \rho_1, \rho_2 
	~~;
	& \kletregion~ r_3 
	~\kwith~ \{ w_3 = \iMkDistinct~ \un{\rho_1}~ r_3;~ w_4 = \iMkDistinct~ \un{\rho_2}~ r_3 \}~ \\
		& \kin~ ... ~w_3~ ... ~w_4~ ... 
}
By EvLetRegion, the next step is to allocate a fresh region handle (say $\un{\rho_3}$), substitute it into the witness set, reduce the witness expressions to normal form, and then substitute these for $w_3$ and $w_4$ in the body. The corresponding evaluation and kinding rules are as follows:

\[	\begin{array}{rlrr}
		{H,~ \rho_1,~ \rho_2 ~;~ \iMkDistinct~ \un{\rho_1}~ \un{\rho_2}}
		& \lto~ \un{\rdistinct~ \rho_1~ \rho_2}
		& \rho_1 \ne \rho_2
		&(\trm{EwDistinct})
	\\[1ex]
		{\Gamma ~|~ \Sigma,~ \rho_1,~ \rho_2}
		 ~ \judgea{K} ~ \un{\rdistinct~ \rho_1~ \rho_2}
		& ::~~ \iDistinct~ \un{\rho_1}~ \un{\rho_2}
		& \rho_1 \ne \rho_2
		& (\trm{KiDistinct})
	\end{array}
\]

Completing the reduction leaves us with:

\[	H, \rho_1, \rho_2, \rho_3 ~;~ ... ~\un{\rdistinct~ \rho_1~ \rho_3~}~ ... ~\un{\rdistinct~ \rho_2~ \rho_3}~ ...
\]

Once these witnesses have been created, the fact that we cannot substitute for their embedded region handles means that they cannot be changed. This aspect of our system arises naturally from the phase distinction between region variables and region handles, as first discussed in \S\ref{Language:NoStacks}. As the properties encoded by each witness are true at the time of creation, and as neither witnesses or the underlying properties of the store can be changed during evaluation, they must also be true at the time of use. 

Also, by inspection of our kinding rules, the only closed  (with no free variables), normal form type that can have a kind like $\iDistinct~  \un{\rho_1}~ \un{\rho_3}$ ~is~ $\un{\rdistinct~ \rho_1~ \rho_3}$. From this it follows that when we apply a function to type of kind $\iDistinct~  \un{\rho_1}~ \un{\rho_3}$ that type must be $\un{\rdistinct~ \rho_1~ \rho_3}$. Our Progress theorem shows that such a reduction is always possible. It then follows that when we pass such a witness, the corresponding property of the store is always true. 

Note that our use of witnesses to guarantee non-aliasing is weaker than that provided by a ``real'' aliasing analysis such as \cite{guo:pointer-analysis} or \cite{smith:alias-types}. These systems can recover (an approximation to) aliasing relationships between objects at every point in the program, from an arbitrary sequence of update statements. In contrast, in our system the occurrence of a witness of kind $Distinct~ r_1~ r_2$ ensures that objects in regions $r_1$ and $r_2$ never alias, ever. The advantage of our approach is that it's practically free. With respect to the concrete implementation all we had to add was the kind and superkind of $MkDistinct$ and $Distinct$, and a trivial syntactic check on the form of $\kletregion$. Now we can implement aliasing aware optimisations without also writing a heavy-duty analysis or adding further type machinery.
