% ------------------------------------------------------------------------------
\section{Effect purification and constancy constraints}

As our list type contains region variables, we will revisit the type of $\imap$. This function has three sources of effects, inspecting the list cells during the case-expression, applying the parameter function, and the recursive call. Here is the definition of $\imap$ again, with its new type.

\begin{tabbing}
MM \= MM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\imap 	:: \forall a \ b \ r_1 \ r_2 \ e_1
			. \ (a \longtoa{e_1} b) 
				\to \iList \ r_1 \ a 
				\longtoa{e_1 \lor \iRead r_1} \iList \ r_2 \ b$ \\[1ex]
	\> $\imap \ \ilist$ \\
	\> \ $= \kcase \ \ilist \ \kof$ \\
	\> \> $\iNil$			\> $\to \iNil$ \\
	\> \> $\iCons \ x \ \ixs$	\> $\to \iCons \ (f \ x) \ (\imap  f \ \ixs)$ 
\end{tabbing}

Note both the type of the parameter function, and the right-most arrow are both annotated with $e_1$, which expresses the fact that $\imapL$ applies its parameter. Suppose we now want to write a version of map that suspends its recursive call, so the list cells are only constructed when they are demanded. We will call this function $\imap_{LT}$, where LT stands for Lazy Tail.

\begin{tabbing}
MM \= MM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\imap_{LT} \ f \ \ilist$ \\
	\> \ $= \kcase \ \ilist \ \kof$ \\
	\> \> $\iNil$			\> $\to \iNil$ \\
	\> \> $\iCons \ x \ \ixs$	
		\> $\to \iCons \ (f \ x) \ ((\isuspend \ (\imapL \ f)) \ \ixs)$ 
\end{tabbing}

Recall the type of $\isuspend$ which suspends a single function application. $\isuspend$ places a purity constraint on the parameter function to ensure that the value of the returned suspension will not depend on when it is evaluated.
\begin{tabbing}
MM \= MM \= MMMMMM \= MMMMM \= MMMM \kill
	\> $\isuspend :: \forall a \ b \ e_1 . \ \iPure \ e_1 \To (a \longtoa{e_1} b) \to a \to b$
\end{tabbing}
As $\imap_{LT}$ suspends its recursive call, which has the effect $e_1 \lor \iRead \ r_1$, and leads to the constraint $\iPure \ (e_1 \lor \iRead \ r_1)$. Now, we can satisfy the first part of this constraint simply by requiring the parameter function to be pure itself, $\iPure \ e_1$. We satisfy the second part by requiring the region $r_1$ to be constant, that is, never permitting it to be updated. A read of a constant region is pure, because it does not matter \emph{when} we read it, we will always get the same result. The final type for $\imap_{LT}$ is as follows.

\begin{tabbing}
MM 	\= MMM \= M \= MMMMM \= MMMM \kill
	\> $\imap_{LT}$	\> $::$	 	\> $ \forall a \ b \ r_1 \ r_2 \ e_1. 
						\ (a \longtoa{e_1} b) \to \iList \ r_1 \ a \to \iList \ r_2 \ b$ \\
	\>		\> $\rhd$	\> $\iConst \ r_1, \ \iPure \ e_1$ \\
\end{tabbing}
