

% -------------------------------------------------------------------------------------------------
\subsection{Region Sets}
\note{Talk about explosion in the number of witnesses required. $n^2$ in number of regions. Really want region sets.}

\code{
\iDistinctSet	& :: \%\% \to \Diamond 				& (\trm{witness kind constructor}) \\
\iMkDistinctSet & :: \Pi(s_1 : \%\%). \iDistinctSet~ s_1	& (\trm{witness type constructor})
}


Note that a while a witness of kind, say, $\iDistinct~ \%\{r1, r2, r3\}$ guarantees that these three regions are distinct, it also guarantees that subsets of them are distinct. For example, we also know that the properties witnessed by $\iDistinct~ \%\{r1, r2\}$, and $\iDistinct~ \%\{r2, r3\}$ are true. We introduce another constructor that encodes this fact. 

\[	\iMkDistinctNarrow :: \Pi(s_1 : \%\%).~ \Pi(s2 \subseteq s1 : \%\%).~ 
		\iDistinctSet~ s_1 \to \iDistinctSet~ s_2
\]



\note{Add an intro to aliasing first. Extension to existing system. Reuse idea of a witness. Want to track propagate informtion about aliasing instead of trying to recover it, ref existing analysis}.

Suppose we are compiling the following function:

\[
\begin{array}{lll}
	\mc{3}{\Lambda r_1.~ \Lambda r_2.~ \Lambda (w_1 : \iMutable~ r_1).~ 
	\lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{3}{\kletregion~ r_3~ \kin} \\
	\klet 	& \_ 	& = \iupdateInt~ r_1~ r_2~ w_1~ x~ (add~ r_1~ r_3~ r_3~ y~ (93~ r_3)) \\
		& z	& = \iadd~ r_1~ r_3~ r_3~ y~ (42~ r_3)  \\
	\kin	& \mc{2}{... ~x~ ... ~y~ ... ~z~ ...}
\end{array}
\]

Where $\iupdateInt$ and $\iadd$ have the following types:

\[
\begin{array}{lll}
	\iupdateInt 
		& :: & 
		\forall r_1 r_2.~ 
		Mutable~ r_1 
		\To~ Int~ r_1 
		\to~ Int~ r_2 
		\longtoa{Read~ r_2 ~\lor~ Write~ r_1} ()			
\\
	\iadd	& :: &
		\forall r_1 r_2 r_3.~
		\iInt~ r_1 \to \iInt~ r_2 \longtoa{\iRead~ r_1 \lor \iRead~ r_2} \iInt~ r_3
\end{array}
\]


We would like optimise the function by performing the local unboxing transformation \note{cite}. We write the type of unboxed integers as $\iInt_\#$ and make use of the following operators:

\[
\begin{array}{lll}
	\ibox		& :: & \forall r_1.~ \iInt_\# 	\to \iInt~ r_1 \\
	\iunbox		& :: & \forall r_1.~ \iInt~ r_1 \longtoa{\iRead~ r_1} \iInt_\#  \\[0.5ex]
	\iadd_\#	& :: & \iInt_\# \to \iInt_\# \to \iInt_\#
\end{array}
\]

In this presentation, unboxed integers do not appear in the heap and cannot be destructively updated. Due to this, reading them does not cause an effect, so they do not need to be annotated with region variables. Using the above operators we can rewrite our function as follows: 

\[
\begin{array}{lll}
	\mc{3}{\Lambda r_1.~ \Lambda r_2.~ \Lambda (w_1 : \iMutable~ r_1).~ 
	\lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{3}{\kletregion~ r_3~ \kin} \\
	\klet 	& \_ 	& = \iupdateInt~ r_1~ r_2~ w_1~ x~ (box~ r_3~ (add_\#~ (\iunbox~ r_2~ y~)~ 93_\#)) \\
		& z	& = \ibox~ r_3~ (\iadd_\#~ (\iunbox~ r_2~ y~)~ 42_\#)  \\
	\kin	& \mc{2}{... ~x~ ... ~y~ ... ~z~ ...}
\end{array}
\]

Although we haven't exposed any $\ibox/\iunbox$ pairs that could be eliminated, we have exposed a common subexpression $(\iunbox~ r_2~ y)$. However, it is only safe to common up these expressions unless we know that the values $x$ and $y$ are distinct objects, that is, they do not alias. In this case we could rewrite the above as:

\[
\begin{array}{lll}
	\mc{3}{\Lambda r_1.~ \Lambda r_2.~ \Lambda (w_1 : \iMutable~ r_1).~ 
	\lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{3}{\kletregion~ r_3~ \kin} \\
	\klet 	& y'	& = \iunbox~ r_2~ y \\
		& \_ 	& = \iupdateInt~ r_1~ r_2~ w_1~ x~ (box~ r_3~ (add_\#~ y'~ 93_\#)) \\
		& z	& = \ibox~ r_3~ (\iadd_\#~ y'~ 42_\#)  \\
	\kin	& \mc{2}{... ~x~ ... ~y~ ... ~z~ ...}
\end{array}
\]

On the other hand, if $x$ and $y$ were aliases, then the old value of $x~/~y$ would no longer be overwritten by the call to $\iupdateInt$ before it is unboxed the second time. This would change meaning of the program. We can see this more clearly by expanding the original, unboxed version to A-normal form and annotating each binding with the effects it causes:

\[
\begin{array}{llll}
	\mc{4}{\Lambda r_1.~ \Lambda r_2.~ \Lambda (w_1 : \iMutable~ r_1).~ 
	\lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} 				\\
	\mc{4}{\kletregion~ r_3~ \kin} 							\\
	\klet 	& v_1	& = \iunbox~ r_2~ y 				& \iRead~ r_2	\\
		& v_2	& = add_\#~ v_1~ 93_\# 				& \bot		\\
		& v_3	& = box~ r_3~ v_2 				& \bot		\\
		& \_ 	& = \iupdateInt~ r_1~ r_2~ w_1~ x~ v_3 	\qq	& \iRead~ r_3 \lor \iWrite~ r_1 \\
		& v_4	& = \iunbox~ r_2~ y~ 				& \iRead~ r_2	\\
		& v_5	& = \iadd_\#~ v_4~ 42_\# 			& \bot		\\
		& z	& = \ibox~ r_3~ v_5  				& \bot		\\
	\kin	& \mc{2}{... ~x~ ... ~y~ ... ~z~ ...}
\end{array}
\]

\bigskip
We can see now that commoning up bindings $v_1$, $v_4$ is equivalent to floating $v_4$ across the three bindings before it. This is only valid if the effects $\iRead~ r_3 \lor \iWrite~ r_1$ and $\iRead~ r_2$ do not interfere. Reads do not interfere with reads, leaving us with the requirement that $\iWrite~ r_1$ does not interfere with $\iRead~ r_2$.  This in turn requires that $r_1$ and $r_2$ are distinct regions. We discuss how to track this information in the next section.

\subsection{Witnesses of No Aliasing}
We extend our general framework with the kind of witnesses that guarantee that a set of regions are \emph{distinct}, that is, they do not alias.

\[	\iDistinct :: \%\% \to \Diamond
\]

The atomic kind $\%\%$ is the kind of sets of region variables. Using this kind we can now write a version of the function from the previous section that makes the fact that its arguments must be in distinct regions explicit. 
\[
\begin{array}{lll}
	\mc{3}{\Lambda r_1.~ \Lambda r_2.~ \Lambda (w_1 : \iMutable~ r_1).~ \Lambda (\_ : \iDistinct~ \{r_1, r_2\}).} \\
	\mc{3}{\lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{3}{\kletregion~ r_3~ \kin} \\
	\klet 	& y'	& = \iunbox~ r_2~ y \\
		& \_ 	& = \iupdateInt~ r_1~ r_2~ w_1~ x~ (box~ r_3~ (add_\#~ y'~ 93_\#)) \\
		& z	& = \ibox~ r_3~ (\iadd_\#~ y'~ 42_\#)  \\
	\kin	& \mc{2}{... ~x~ ... ~y~ ... ~z~ ...}
\end{array}
\]

The type-level term $\{r_1, r_2\}$ gives the set of region variables that must be distinct. Note that we have used an underscore (\_) for the binder of the new witness because it not occur anywhere in the body of the function. Rather, the witness is needed to show that this specialised version can only be called when the particular property holds. Alternatively, we could give the new witness a binding variable, and say that the transform that produces this code is only valid when the witness is in scope.

Our task is then to build a mechanism to construct a witness of this kind, and to ensure that they can only be constructed with the associated property holds. This turns out to be surprisingly simple, because when we introduce fresh regions with a $\kletregion$ expression, we know for sure that they don't alias with any others. To do this we modify $\kletregion$ so that we can introduce several regions at once, and to use the following constructor in its witness list:

\[	\iMkDistinct :: \Pi(s_1 : \%\%) \to \iDistinct~ s_1
\]

Note that a while a witness of kind, say, $\iDistinct~ \%\{r1, r2, r3\}$ guarantees that these three regions are distinct, it also guarantees that subsets of them are distinct. For example, we also know that the properties witnessed by $\iDistinct~ \%\{r1, r2\}$, and $\iDistinct~ \%\{r2, r3\}$ are true. We introduce another constructor that encodes this fact. 

\[	\iMkDistinctNarrow :: \Pi(s_1 : \%\%).~ \Pi(s2 \subseteq s1 : \%\%).~ 
		\iDistinct~ s_1 \to \iDistinct~ s_2
\]

\note{we can do the subset test statically because the set of region variables is always flat, that is, we don't have a complex expression involving union or intersection operators. Distinct witnesses are strongest (hold the most information) when they are created. We can weaken them by applying $\iMkDistinctNarrow$, but we do not join information from multiple Distinct witnesses together. }

\note{example that calls fn from previous section}

\note{why this is sound. Show single set of letregion, region handles going into store. Region handles are fresh. Region handles are never substituted for other region handles. }

\note{Check Benton / Kennedy's higher order store paper, what's the complication?}

\note{Reference other approaches to aliasing}



The only way we could create witnesses 


At the point the regions are introduces we know that they are distinct, just need to propagate this information through the program. Also know that the new regions don't alias with existing regions, because the new regions are guaranteed to be fresh. \note{Syntactic restrictions on created witnesses}.



\note{Explosion of number of witnesses required}

\code{
\iDistinctSet	& :: \%\% \to \Diamond 				& (\trm{witness kind constructor}) \\
\iMkDistinctSet & :: \Pi(s_1 : \%\%). \iDistinctSet~ s_1	& (\trm{witness type constructor})
}


Note that a while a witness of kind, say, $\iDistinct~ \%\{r1, r2, r3\}$ guarantees that these three regions are distinct, it also guarantees that subsets of them are distinct. For example, we also know that the properties witnessed by $\iDistinct~ \%\{r1, r2\}$, and $\iDistinct~ \%\{r2, r3\}$ are true. We introduce another constructor that encodes this fact. 

\[	\iMkDistinctNarrow :: \Pi(s_1 : \%\%).~ \Pi(s2 \subseteq s1 : \%\%).~ 
		\iDistinctSet~ s_1 \to \iDistinctSet~ s_2
\]
