
\section{Sharing, Purity and the Full Laziness Transform}
\label{Optimisation}
In this section we consider the \emph{full-laziness} transform \cite{peyton-jones:modular-lambda-lifter} as an example optimisation using our system. In the following function, note that if we could lift the $n$ binding out of the inner function then we could save its recomputation for each application. We have elided some of the type annotations to make the presentation clearer.

\[ 
\begin{array}{llll}
	\mc{3}{\Lambda r_3~ e_1.~ \lambda(g : \iInt~ r_3 \toa{e_1} \iInt~ r_3).} \\
	\mc{3}{\kletregion~ r_4~ \kwith~ w_1 = \iMkConst~ r_4 ~ \kin} \\
	\klet 	& \mc{2}{(\ixs : \iList~ r_4~ (\iInt~ r_3)) = ...} \\
	 	& f & = \lambda y.~ \klet~ n ~=~ g~ (\ilength~ \ixs)~ \kin~ n ~+~ y \\
	\kin	& \mc{2}{\imap~ f ~ \ixs}
\end{array}
\]

We will specialise this function for the case when $g$ is pure. This will allow us to perform the lift, but as we cannot guarantee that $f$ will be applied at least once, we wrap the lifted expression in a suspension to guard against the case where it diverges. Doing this requires a witness that the $n$ binding is pure. We will assume that $\ilength$ has the same type as in \S\ref{Witnesses-of-Constancy-and-Mutability}, namely:

\[	\ilength ~::~ \forall a~ r_1~ r_2.~ \iList~ r_1~ a \toa{\iRead~ r_1} \iInt~ r_2
\]

As type of the list $\ixs$ is $\iList~ r_4~ (\iInt~ r_3)$, applying $\ilength$ to it causes the effect $\iRead~ r_4$. Applying the function $g$ to the result then causes the effect $e_1$, so the effect of the whole $n$ binding is $\iRead~ r_4 \lor e_1$. We know that $\iRead~ r_4$ is pure due to the witness $\iMkConst~ r_4$. We can then require $e_1$ to be pure by adding a new type parameter that binds an appropriate witness of purity. This ensures that the specialised version of our function can only be applied to an argument that meets this constraint. The result of the transform is as follows:

\[
\begin{array}{lll}
	\mc{3}{\Lambda r_3~ e_1.~  \Lambda(w_2 ~: \iPure~ e_1). 
		\ \lambda(g : \iInt~ r_3 \toa{e_1} \iInt~ r_3).} \\
	\mc{3}{\kletregion~ r_4~ \kwith~  w_1 = \iMkConst~ r_4 ~ \kin} \\
	\klet 	& \mc{2}{(\ixs : \iList~ r_4~ (\iInt~ r_3)) = ...} \\
		& n & = \isuspend~ (\iMkPureJoin~ (\iMkPurify~ r_4~ w_1)~ w_2)~ (\lambda \_.~ g~ (\ilength~ xs))~ () \\
		& f & = \lambda y.~ n ~+~ y \\
	\kin	& \mc{2}{\imap~ f ~ \ixs}
\end{array}
\]


% ---------------------------------------------------------
\subsection{Idempotency and Allocation Effects} 
In general, if we wish to lift a binding out of an enclosing lambda abstraction, that binding must satisfy two constraints. The first is that it can be safely reordered with other expressions in the abstraction, and the second is that it is idempotent. The first is needed because moving the binding changes the order of evaluation relative to the original abstraction. The second is needed because the lifted expression will tend to be evaluated less often, which is the whole purpose of performing the transform. Note that a function that returns a freshly allocated object is not idempotent. Now, although related work such as \cite{talpin:type-and-effect-discipline} and \cite{benton:relational-semantics-effect-transformations} uses allocation effects to account for this, we do not. In our system, an expression that produces a fresh object but has no other visible effects is still considered pure. Consider then the following expression:

\[
\begin{array}{lllll}
	\mc{4}{\Lambda r_1.~ \Lambda (w_1 : \iMutable~ r_1).} \\
	\klet 	& (f  & \hspace{-1em}: () \to \iInt~ r_1)	& = \lambda \_.~ 5~ r_1 \\
		& (x  & \hspace{-1em}: \iInt~ r_1)		& = f~ () \\
		& \_  &					& = \iupdateInt~ r_1~ r_1~ w_1~ x~ (42~ r_1) \\
	\kin	& f~ ()
\end{array}
\]

This expression defines an inner function $f$ that returns a freshly allocated `5' object each time it is applied. It then applies it, and destructively updates the result. As it stands, the result of the entire expression is also 5. However, if we were to ``optimise'' it by lifting the inner expression $(5~ r_1)$ out of the abstraction for $f$ then this would change its meaning:

\[
\begin{array}{lllll}
	\mc{4}{\Lambda r_1.~ \Lambda (w_1 : \iMutable~ r_1).} \\
	\klet 	& (y  & \hspace{-1em}: \iInt~ r_1)		& = 5~ r_1 \\
		& (f  & \hspace{-1em}: () \to \iInt~ r_1)	& = \lambda \_.~ y \\
		& (x  & \hspace{-1em}: \iInt~ r_1)		& = f~ () \\
		& \_  &						& = \iupdateInt~ r_1~ r_1~ w_1~ x~ (42~ r_1) \\
	\kin	& f~ ()
\end{array}
\]

Although our typing rules assign the expression $(5~ r_1)$ the pure effect $\bot$, the meaning of our program has changed, which makes our optimisation invalid. The trouble is that $(5~ r_1)$ is not idempotent, as it allocates a new object each time it is evaluated. However, the fact that it is not idempotent only matters because we destructively update its result. Without destructive update, there is no way to distinguish an expression that returns a fresh object, from one that returns the same object every time. 

This reveals that we do not actually need allocation effects to justify the full laziness transform. To lift a given expression out of an abstraction it is sufficient to show that it does not read or write mutable data, and that the resulting value cannot be updated. With this in mind, a poignant question is whether there any useful transformations that can \emph{only} be justified using the information provided by allocation effects. The answer, of course, is yes. Consider the following rewrite from \cite{benton:relational-semantics-effect-transformations}.

\[
\begin{array}{lllll}
	& \klet & x = exp;~  y = exp ~\kin~ (x, y) \\
\longto	& \klet & x = exp ~\kin~ (x, x)
\end{array}
\]

This is valid provided $exp$ does not read from any regions that it writes to, and performs no visible allocation. If it were to allocate its return value then we could distinguish the two elements of the pair by updating one and comparing both. However, note that the transform is also valid if $exp$ does not read from any regions that it writes to, and returns a value that is constrained to be constant. This yields a weaker transform, though we are not aware of any existing work that quantitatively compares the two. Note that this transform has a similar structure to full-laziness: they both save repeated computation by increasing the sharing of data. In summary, we choose to forgo allocation effects, simplify our analysis, and reduce the volume of effect information. However, we are not aware of any technical barrier to adding them as an extension to the existing system. 


