
\section{Optimisation}
We consider the \emph{full-laziness} transform \cite{peyton-jones:let-floating} as an example optimisation in our system. This transform is similar to the `lifting expressions out of loops' optimisation done in compilers for imperative languages. In the following program, note that if we could lift the expression $g \ (\ilength \ \ixs)$ out of the inner function then we could save its recomputation for each application.  We have elided some of the type applications to make the presentation clearer.
\begin{tabbing}
MM \= MM \= MM \= MM \= MMMMM \= MMMMM\kill
	\> $\Lambda (r_3 : *). \ \Lambda (e_1 : \ !). \ \lambda (g : \iInt \ r_3 \toa{e_1} \iInt \ r_3).$ 
	\\
	\> $ \kletregion \ r_4 \ \kwith \ \{ \ w_1 = \iConst \ r_4 \ \} \ \kin$ 
	\\
	\> $\kdo$
	   \> $(\ixs : \iList \ r_4 \ (\iInt \ r_3))$  $= ...$
	\\
	\> \> $f$	\> $= \lambda y. \ \kdo \ \{ \ n \ = g \ (\ilength \ \ixs); \ n + y \ \}$ 
	\\
	\> \> $\imap \ f \ \ixs$
\end{tabbing}
We will specialise the above function for the case when $g$ is pure. This allows us to perform the lift, but as we cannot guarantee that $f$ will be called at least once, we wrap the lifted expression in a suspension to guard against the case when it diverges. We also add an extra type parameter to bind the appropriate witness of purity, which ensures that the specialised version can only be applied to a function that meets this new constraint.
\begin{tabbing}
MM \= MM \= MM \= MM \= MMMM \= MMMMM \kill
	\> $\Lambda (r_3 : *). \ \Lambda (e_1 : \ !). \ \Lambda (w_2 : \iPure \ e_1). \ \lambda (g : \iInt \ r_3 \ \toa{e_1} \iInt \ r_3).$
	\\ 
	\> $\kletregion \ r_4 \ \kwith \ \{ \ w_1 = \iConst \ r_4 \ \} \ \kin$ 
	\\
	\> $\kdo$
	   \> $(\ixs : \iList \ r_4 \ (\iInt \ r_3))$  $= ...$
	\\
	\> \> $n$ 	\> $= \isuspend$	\> \> $(\iMkPureJoin \ (\iMkPurify \ r_4 \ w_1) \ w_2)$  \\
	\> \>		\>			\> \> $(\lambda \_ . \ g \ (\ilength \ \ixs)) \quad ()$ 
	\\
	\> \> $f$	\> $= \lambda y. \ n + y$  \\
	\> \> $\imap \ f \ \ixs$
\end{tabbing}
When we suspend a function application we must prove to the suspend operator that the application is pure. We have done this with the witness construction $(\iMkPureJoin \ (\iMkPurify \ r_4 \ w_1) \ w_2)$. This construction has kind $\iPure \ (\iRead \ r_4 \lor e_1)$, where $\iRead \ r_4$ is due to $\ilength$ inspecting the list, and $e_1$ is from applying the parameter function. Creating a witness serves as internal sanity check for our compiler, and if we cannot do so then there is a bug in our implementation.

