
% ------------------------------------------------------------------------------
\section{Witnesses and Witness Construction}
\label{Witnesses}
We use dependently kinded proof witnesses to encode information about mutability and purity in the core language. A witness is a special type that can occur in the program being evaluated, and its occurrence guarantees a particular property of the program. The System-Fc \cite{sulzmann:system-Fc} language uses a similar mechanism to encode information about non-syntactic type equality. Dependent kinds were introduced by the Edinburgh Logical Framework (LF) \cite{avron:edinburgh-lf} which uses them to encode logical rules. 

In comparison with Haskell, we regard witnesses as akin to type level ``dictionaries'' that provide certain capabilities to the functions that require them. For example, consider the following Haskell function $\ipairEq$ which tests if two elements of a pair are equal.
\code{
	\ipairEq :: \forall a.~ \iEq~ a \To (a, a) \to Bool \\
	\mc{3}{\ipairEq~ (x, y) =~~ x == y}
}
In the type signature, the constraint $\iEq$ restricts the types that $a$ can be instantiated with to just those which support equality. This requirement arises because we have used $(==)$ to compare two values of type $a$. As well as being a type constraint, a Haskell compiler such as GHC would treat $\iEq~ a$ as the type of an extra parameter to $\ipairEq$. In this case, the parameter will include an appropriate function to compare the two elements of the pair. 

During compilation, the compiler will detect applications of $\ipairEq$ and add an extra argument appropriate to the type it is called at. For example, a GHC style translation of pairEq to its core language \TODO{cite} would yield something similar to:
\code{
	\ipairEq~~ =	
		& \mc{2}{\Lambda (a :  *).~ 
			 \lambda (\icomp : a \to a \to \iBool).~
			 \lambda (\ipair : (a, a)).} \\
		& \mc{2}{\kcase~ \ipair~ \kof} \\
		& \mc{2}{~~(x, y) \to \icomp~ x~ y}
}
An application of this function in the source language such as $\ipairEq~ (2, 3)$ would then be translated to $\ipairEq~ \iInt~ \iprimIntEq~ (\iPair~ \iInt~ 2 3)$, where $\iprimIntEq$ is the primitive equality function on integers. Returning to the translation of $\ipairEq$, the extra parameter binds \emph{evidence} \TODO{cite} that type $a$ really does support the equality operation --- and there is no better evidence than the function which performs it.

With the idea of ``evidence'' in mind, suppose that we were only interested in the fact that $\ipairEq$ requires $a$ to support equality, rather than how to actually evaluate this function at runtime. In the above translation we managed our evidence at the value level, by explicitly passing around a comparison function. Alternatively, we could manage it at type level:  
\code{
	\ipairEq~~ =
		& \mc{2}{\Lambda (a  : *).~ 
			 \Lambda (w      : \iEq~ a).~ 
			 \lambda (\ipair : (a, a)).} \\
		& \mc{2}{\kcase~ \ipair~ \kof} \\
		& \mc{2}{~~(x, y) \to (==)~ w~ x~ y}
}
In this new translation, the extra parameter ($w$) binds a \emph{proof term}. One step removed from value-level evidence, this type-level proof term serves as a \emph{witness} that type $a$ really does support equality, and this is recorded in its kind $\iEq~ a$ Note that we can also read the first part of the signature for $\ipairEq$ directly from its definition. The $\Lambda a : *.$ in the definition corresponds to $\forall a : *.$ in the signature, and $\Lambda w : \iEq~ a.$ corresponds to $\iEq~ a \To$.

How a particular calling function happens to manufacture its witnesses is of no concern to $\ipairEq$, though they do need to enter the system somehow. In the general case the caller has three options: require the witness to be passed in by an outer function, combine two witnesses into a third, or construct one explicitly. For our $\ipairEq~ (2, 3)$ example, the third option suffices, and we can translate the call to $\ipairEq~ \iInt~ (\iMkEq~ \iInt)~ (\iPair~ \iInt~ 2 3)$. The type level function $\iMkEq$ is a \emph{witness constructor} which takes a type $(\iInt in this case)$ and produces a witness of kind $\iEq~ a$. The expression $(\iMkEq~ a)$ is an axiom in our proof system, and it is valid to repeat it in the program when required. In contrast, when we discuss witnesses of constancy and mutability in \TODO{ref} their construction will be restricted to certain places in the program to ensure soundness. With this plumbing in place we can ensure our code is consistent with respect to which type support equality simply by type checking it in the usual way and then inspecting the way witnesses are constructed. 


For DDC core, we use the witness passing mechanism to manage five sorts of witnesses, which we will consider in turn: 

\begin{enumerate}
\item	Witnesses that a region has been created.
\item	Witnesses the all the data in a region is constant.
\item	Witnesses that data in a region may be updated.
\item	Witnesses that a particular function is visibly pure. 
\item	Witnesses that two regions are known to be distinct (do not alias).
\end{enumerate}

Some of our witnesses are mutually exclusive, specifically: if we have a witness that a region is constant, then our language design guarantees that a conflicting witness of mutability cannot exist in the same program. As far as compilation is concerned, the witness passing mechanism encodes explicit \emph{justification} for why a particular operation is allowable. Witnesses to region creation allow new objects to be allocated into the new region, and witnesses of mutability allow those objects to be updated. Witnesses of constancy are converted to witnesses of purity for given effects, which in turn allow functions that have those effects to be suspended. During optimisation, witnesses of distinctness allow us to reorder expressions that write to data that is known not to alias. In \TODO{ref} we will also show how to introduce more optimisation opportunities into an existing program by specialising functions for the case where the arguments are constant, or known to be distinct. 

Finally, note that although our formal operational semantics manipulates witnesses during reduction, in practice they are only used to reason about the program during compilation, and are not needed at runtime. Our compiler erases witnesses before code generation, along with all other type information.


% ------------------------------------------------------------------------------
\subsection{Region Handles}
\label{Witnesses:RegionHandles}
The first witnesses we discuss are the region allocation witnesses $\un{\rho}$. Syntactically, this expression consists of two parts. The plain $\rho$ is a label (name) for a particular region in the store, and the underline turns the label into a \emph{type}. Region allocation witnesses are also called \emph{region handles} and they are introduced into the program with the $\kletregion \ r \ \kin \ t$ expression. Although region handles are not needed at runtime, we can imagine them to be operational descriptions of physical regions of the store, perhaps incorporating a base address and a range. As an example, the following function adds two to its argument, while storing an intermediate value in the region $r_3$.
\code{
	\iaddTwo & :: & \forall r_1~r_2.~\iInt~r_1\longtoa{\iRead~r_1 \lor \iAlloc~r_2}\iInt~r_2 \\
	\iaddTwo 
	  &=&	\Lambda r_1~ r_2.~ \lambda(x:\iInt~ r_1). \\
	  & & 	\kletregion~ r_3~ \kin~ \isucc~ r_3~ r_2~ (\isucc~ r_1~ r_3~ x)
}

This function makes use of the primitive $\isucc$ function from \TODO{ref} that reads its integer argument and produces a new value into a given region:
\code{
	\isucc & :: & \forall r_1~ r_2.~ \iInt~ r_1 \longtoa{\iRead~ r_1 \lor \iAlloc r_2} \iInt~ r_2
}

In our semantics, once a region has been created, we use a second construct $\kwithregion$ to hold the region handle while the inner expression completes its evaluation. Like region handles $\un{\rho}$, with $\kwithregion$ construct does not exist in the initial program, as no regions have yet been created. 

The following reduction illustrates the operation of $\iaddTwo$, with $\kletregion$ and \\ $\kwithregion$ contracted to $\klr$ and $\kwr$ for space reasons. We write machine states as $H~;~t$ where $H$ is the store and $t$ is the term being reduced. For now, we will say that the store contains bindings written $l \mtoa{\rho} \mu$ where $l$ is an abstract location, $\mu$ is the data contained at that location, and $\rho$ is the label of the region that binding belongs to. We will discuss the form of data more precisely  in \S\ref{Language:DynamicSemantics}. The store also contains plain region labels $\rho$ which indicate that the corresponding region has been allocated and is ready to have bindings added to it.

\code{
		& ...
\\
\longtoa{*}	& \rho_5 
		& ;~ \kwr~ \un{\rho_5}~ \kin~ {\iaddTwo~\un{\rho_5}~\un{\rho_5}~(23~ \un{\rho_5}~ ())} 
\\
\eto		& \rho_5,~ l_1 \mtoa{\rho_5} 23
		& ;~ \kwr~ \un{\rho_5}~ \kin~ {\iaddTwo~ \un{\rho_5}~ \un{\rho_5}~ l_1} 
\\
\longtoa{*}	& \rho_5,~ l_1 \mtoa{\rho_5} 23
		& ;~ \kwr~ \un{\rho_5}~ \kin~ 
				\klr~ r_3~ \kin~ \isucc~ r_3~ \un{\rho_5}
				~(\isucc~ \un{\rho_5}~ r_3~ l_1) 
\\
\longto		& \rho_5,~ l_1 \mtoa{\rho_5} 23,~ \rho_6
		& ;~ 	\kwr~ \un{\rho_5}~ \kin~ 
			\kwr~ \un{\rho_6}~ \kin~
			\isucc~\un{\rho_6}~\un{\rho_5}
		 	~(\isucc~\un{\rho_5}~ \un{\rho_6}~ l_1)
\\
\longtoa{*}	& \rho_5,~ l_1 \mtoa{\rho_5} 23,~ \rho_6,~ l_2 \mtoa{\rho_6} 24
		& ;~	\kwr~ \un{\rho_5}~ \kin~ 
			\kwr~ \un{\rho_6}~ \kin~
			\isucc~ \un{\rho_6}~ \un{\rho_5}~ l_2
\\
\longtoa{*}	& \rho_5,~ l_1 \mtoa{\rho_5} 23,~ \rho_6,~ l_2 \mtoa{\rho_6} 24,~ l_3 \mtoa{\rho_5} 25
		& ;~	\kwr~ \un{\rho_5}~ \kin~ 
			\kwr~ \un{\rho_6}~ \kin~
			l_3
\\
\longto		& \rho_5,~ l_1 \mtoa{\rho_5} 23,~ \rho_6,~ l_2 \mtoa{\rho_6} 24,~ l_3 \mtoa{\rho_5} 25
		& ;~	\kwr~ \un{\rho_5}~ \kin~ 
			l_3
\\
\longto		& \rho_5,~ l_1 \mtoa{\rho_5} 23,~ \rho_6,~ l_2 \mtoa{\rho_6} 24,~ l_3 \mtoa{\rho_5} 25
		& ;~	l_3
}

At the beginning, region $\rho_5$ has already been allocated, and the reduction of $(23~ \un{\rho_5}~ ())$ adds a new binding into the heap. The $\kletregion$ expression ($\klr$) in the third statement allocates a fresh region label $\rho_6$ and its handle $\un{\rho_6}$ is substituted for $r_3$. Note the phase distinction between region variables $r_n$ and region handles $\un{\rho_n}$, as $\kletregion$ simultaneously allocates a region and introduces its handle, the occurrence of a handle in the program guarantees the fact that the corresponding region has been created, and is ready to have bindings added into it. To say this another way: the region handle $\un{\rho}$ ``witnesses'' the fact that the corresponding region $\rho$ has been created.

Returning to the definition of $\iaddTwo$, note that although an intermediate value is allocated into, and then read from $r_3$, this effect is not observable to calling functions. This means it can be masked and not included in the type signature. This similar to the system of \cite{talpin:type-and-effect-discipline}. Also, note that given two bindings $l_1 \mtoa{\rho_1} \mu_1$ and $l_2 \mtoa{\rho_2} \mu_2$, knowing that the region labels $\rho_1$ and $\rho_2$ are distinct, also implies the locations $l_1$ and $l_2$ are distinct. As we will see in \TODO{ref} the type of a given location includes its region handle, which is named after the region \emph{label}, and we exploit this fact to gain control over aliasing. These two benefits, masking and control over aliasing, are why we use region typing in our system. Note that these benefits are separate from the use of regions to perform stack based allocation and deallocation as per \TODO{cite}. In DDC core, although we could a stack allocation mechanism for some regions, the fact that we also support lazy evaluation means that we cannot use it for all. This is discussed further in \TODO{ref}.


% ------------------------------------------------------------------------------
\subsection{Witnesses of Constancy and Mutability}
\label{Witnesses-of-Constancy-and-Mutability}
The constancy or mutability of values in a particular region is encoded by the witnesses $\un{\rconst \ \rho}$ and $\un{\rmutable \ \rho}$. Once again, these are types that cannot occur in the initial program. Instead, they are created with the $\iMkConst$ and $\iMkMutable$ witness type constructors, which have the following kinds:
\code{
	\iMkConst	& :: & \Pi (r : \%).~\iConst~ r \\
	\iMkMutable	& :: & \Pi (r : \%).~\iMutable~ r
}
Both constructors take a region handle and produce the corresponding witness. We use the dependent binding operator $\Pi$ because while $r$ is a (region) type, the body of the abstraction, $\iConst~r$ is a \emph{kind}. This gives us ``dependent kinds''. This can be contrasted to systems with ``dependent types'', which have functions from values to \emph{types}.

To ensure that both $\un{\rconst \ \rho_n}$ and $\un{\rmutable \ \rho_n}$ for a particular $\un{\rho_n}$ cannot occur in the same program, we require the mutability (or constancy) of a region to be set at the point it is created. This is done by extending the $\kletregion$ construct with an optional set of witness bindings. For example, the following function drops a given number of elements from the front of a list, using a local, destructively updated counter to keep track of how many have been dropped so far.

\begin{tabbing}
MMMM \= MMM \= M \= MM \= MMMM \= MMMM \= M \= MM \kill
\> $\idrop$ 	\> $::$	  \> $\forall a~ r_1~ r_2.~ 
				\iInt~ r_1 
				\to \iList~ r_2~ a 
				\longtoa{e_1} \iList~ r_2~ a$ \\
\>		\> $\rhd$ \> $e_1 = \iRead~ r_1 \lor \iRead~ r_2 \lor \iAlloc~ r_2$ 
\\[1ex]
\> $\idrop$	\> $=$	  \> $\Lambda a~ r_1~ r_2.~ 
				\lambda (\inum  : \iInt~  r_1).~
				\lambda (\ilist : \iList~ r_2~ a).$ \\
\>\>\> $\kletregion~ r_3~ \kwith~ \{ w = \iMkMutable~ r_3 \}~ \kin $ \\
\>\>\> $\klet$ 	\> $(\icount$ 	\> $ : \iInt \ r_3)$	\> $= 0~ r_3~ ()$ \\
\>\>\>		\> $(\idrop'$	\> $ : ...)$ \\
\>\>\> 		\> \quad $=\lambda (\ixx : \iList~ r_1~ a).$ \\
\>\>\>		\> \quad $~~~~ \kcase~ \ixx~ \kof$ \\
\>\>\>		\> \quad $~~~~~~ \iNil$  		\> \> $\to~ \ixx$ \\
\>\>\>		\> \quad $~~~~~~ \iCons~ x~ \ixs$	\> \> $\to~ \kif~ \ieqInt ~ r_1~ r_3~ \inum~ \icount$ \\
\>\>\>		\> \> 					\> \> ~~~ $\kthen~ \iNil~ r_2~ ()$ \\
\>\>\>		\> \>					\> \> ~~~ $\kelse~~ \iincInt~ r_3~ w~ \icount;$ \\
\>\>\>		\> \>					\> \> ~~~~~~~~~~~ $\iCons~ r_2~ a~ x~ (\idrop~ xs)$ \\
\>\>\> $\kin$	\> $\idrop'~ \ilist$
\end{tabbing}

where
\code{
	\ieqInt	  &::& \forall r_1~ r_2.~ 
				\iInt~ r_1 \to 
				\iInt~ r_2 \longtoa{e_1}
				\iInt~ r_3 \\
		  &\rhd& e_1 = \iRead~ r_1 \lor \iRead~ r_2 \lor \iAlloc~ r_3
\\[1ex]
	\iincInt  &::& \forall r_1.~
				\iMutable~r_1 \To 
				\iInt~r_1 
				\longtoa{e_1} () \\
		&\rhd& e_1   = \iRead~r_1 \lor~\iWrite~r_1
}

The set after the $\kwith$ keyword in the $\kletregion$ construct binds the type expression that produces a witness of mutability for $r_3$. Similarly to the case with region handles, there is a phase distinction between type expressions that \emph{construct} witnesses, like $\iMkMutable~r_3$, and the actual normal form witnesses, like $\un{mutable~\rho_3}$. In our reduction semantics the former reduces to the latter, and only the former may appear in the initial program text. We discuss the details of reduction in \S\ref{Language}.

To ensure that ``rogue'' witnesses cannot be created, we place three simple syntactic restrictions on how the constructors $\iMkMutable$ and $\iMkConst$ may be used. We will discuss these restrictions further in a moment.

\begin{enumerate}
\item	Constructors $\iMkMutable$ and $\iMkConst$ may only appear in the set of witness bindings associated with a $\kletregion$.
\item	Either $\iMkMutable$ or $\iMkConst$ may be used in the set, but not both.
\item	If the $\kletregion$ binds a region variable $r$, then only that region variable may be used in the associated set.
\end{enumerate}

Returning to the definition of $\idrop$, note that as we call $\iincInt$ to destructively increment the integer value in $r_3$, this region must be mutable. This fact is encoded by the $\iMutable$ constraint in the type for $\iincInt$, which we satisfy by passing in our witness $w$. If the region $r_3$ happened to be constant instead of mutable, then by the syntactic restrictions on $\kletregion$, we would not have a suitable witness of mutability to pass to $\iincInt$. This provides the constraint exclusivity property discussed in \S\ref{section:constancy-and-constraint-exclucivity}

% -------------------------------------
\begin{flushleft}
\textbf{Design Decison:} Dependent kinds and syntactic restrictions.
\end{flushleft}

With respect to dependent kinds, a natural question is why we want to introduce such a ``heavy duty'' mechanism when we're just trying to track the mutability or constancy of regions. This seems like a simple, binary decision, yet we've introduced a whole new binding operator $\Pi$ into our type language, along with some auxiliary restrictions on the form of programs.

Suppose instead we were to annotate region variables directly, perhaps using $r^+$ for a mutable region, and $r^-$ for a constant one. There are several problems with this. Firstly, $r$ is a type variable, just like $a$ or $e_1$. These three variables have different kinds, namely regions, value types, and effects, but they are variables none the less. In our implementation, we use the same concrete data type to represent all three, the representation consisting of the name of the variable and its kind. Note then that there is never any reason to write $e_1^+$ or $e_1^-$, these two types being meaningless.

Consider also how we would write a function that only accepts a region parameter with a particular mutability. Using type abstraction for annotated regions would require us to manage annotations on binding occurrences as well, such as with $\Lambda (r^+ : \%).$ Of course, one of our stated goals is mutability polymorphism, so we also need to abstract over the mutability of the region. This leads us to a form like $\Lambda (m : \ ?).~  \Lambda (r^m : \%)$, where the $m$ variable gives us polymorphism over the mutability of $r$. We have used $\Lambda$ to bind $m$ because it is essentially type information (that is, it's not a value). If $m$ was not a type, then we would need to introduce separate abstraction and application forms into the type language anyway. This leaves us with the question of what kind to use for $m$. Perhaps we could introduce a new kind, such as $\iMutability$ and write $\Lambda (m : \iMutability).~  \Lambda (r^m : \%)$.  This new kind would classify two atomic type constructors namely $\iMutable : \iMutability$ and $\iConst : \iMutability$. This approach could work, but note that with our own system we can simply write $\Lambda (r : \%)$ to bind a region that is polymorphic in its mutability, without needing a separate abstraction. If the body of the abstraction requires mutability, then we write $\Lambda (r : \%).~ \Lambda (w : \iMutable~ r).$ This is no more verbose than before, and has the advantage that we do not need to attach extra information to the binding occurrences of variables. 

This brings us to the syntactic restrictions. Instead of using syntactic restrictions we could define two separate forms of $\kletregion$, perhaps $\kletconstregion$ and $\kletmutableregion$. Of course, the issue here is that now we have two keywords instead of one. This approach also makes it difficult to extend the system to track properties other than constancy and mutability. Although we do not discuss it further in this paper, in our full implementation we also have witnesses of kinds $\iLazy~ r$ and $\iDirect~ r$. The first indicates that the given region may contain thunks, and indicates to the runtime system that it must check for them when accessing objects in the associated region. On the other hand, $\iDirect~ r$ indicates that the region is guaranteed not to contain thunks, so the objects can be accessed directly. Like $\iConst$ and $\iMutable$, our $\iLazy$ and $\iDirect$ are mutually exclusive, and this property is checked with similar syntactic restrictions. Note that a region can be both $\iDirect$ and $\iConst$ or $\iDirect$ and $\iMutable$, so simply introducing additional keywords $\kletlazyregion$ and $\kletdirectregion$ would not be sufficient. There is also no reason not to allow the programmer to define their own properties. Perhaps we also want $\iDirty$ and $\iClean$ to distinguish between regions that contain objects that may or may not have been written to a file. 

The key points here are of \emph{orthogonality} and \emph{extensibility}. The properties of a region are not the region, and we don't want the language design to hinder further development. Finally, as we will see in the next section, we can also use dependent kinds to express rules relating our witnesses, and not just the witnesses themselves. 


% ------------------------------------------------------------------------------
\subsection{Laziness and Witnesses of Purity}
\label{Witnesses:Purity}
As discussed in \S\ref{section:laziness-and-purity-constraints}, although our language uses call-by-value evaluation as default, we can also suspend an arbitrary function application with the suspend operator:
\code{
	\isuspend		
	 &::& \forall a~ b~ e.~ Pure~ e~ \To (a \toa{e} b) \to a \to b
}
The constraint $\iPure~ e$ indicates that only observably pure applications may be suspended, so when we call $\isuspend$ we must pass a witness to this fact. Witnesses of purity are written $\un{\rpure \ \sigma}$ where $\sigma$ is some effect. They can be created with the following witness constructors:
\code{
	\iMkPureBot 	&::& \iPure~ \bot \\
	\iMkPurifyRead  &::& \Pi (r : \%).~ \iConst~ r \rightarrow \iPure~ (\iRead~ r) \\
	\iMkPurifyAlloc &::& \Pi (r : \%).~ \iConst~ r \rightarrow \iPure~ (\iAlloc~ r)
}
The first constructor expresses the axiom that the $\bot$ effect is manifestly pure. The second takes a witness that a particular region is constant, and produces that a read from it is pure, similarly for the second constructor. Reads of constant regions are pure because it does not matter when the read takes place, the same value will be returned each time. Likewise, the allocation of objects into constant regions is pure because it does not matter if we return a ``ready made'' (or memoised) object instead of a freshly allocated one. Without the ability to destructively the returned object, and without object identity, the caller cannot tell whether this object has indeed been freshly allocated, or not. 

If we have two witnesses of purity we can combine them into a third by overloading the $\lor$ operator. For example, if $w_1$ has kind $\iPure~ \sigma_1$ and $w_2$ has kind $\iPure~ \sigma_2$ then $w_1 \lor w_2$ has kind $\iPure~ (\sigma_1 \lor \sigma_2)$, for some effects $\sigma_1$ and $\sigma_2$. Here is an example that uses witnesses of purity, though we will give a new version in the next section that has a nicer type signature.
\begin{tabbing}
MMMM \= Mx \= MMMMMx \= MMMM \= MMMxx \= MMMMMM \kill
$\ilazyMap$ 	\> $::~~  \forall a~ b~ r_1~ r_2~ e_1$\\
		\> $.~~~~ \iPure~ e_1 
				\To	  \iConst~ r_1
				\To 	  \iConst~ r_2$ \\
		\> $\To (a \toa{e_1} b) 
				\to       \iList~ r_1~ a  
				\toa{e_2} \iList~ r_2~ b$  \\
		\> $\rhd~~ e_2 ~=~ e_1 \lor \iRead~ r_1 \lor \iAlloc~ r_2$
\end{tabbing}

\begin{tabbing}
Mx \= Mx \= MMMMx \= MM \= MMMxx \= MMMMMM \kill
$\ilazyMap$ \\
 \ $=$	\> $\Lambda a~ b~ r_1~ r_2~ e_1~ 
				(w_1 : \iPure~  e_1)~
				(w_2 : \iConst~ r_1)~
				(w_3 : \iConst~ r_2).$ \\
	\> $\lambda (f : a \toa{e_1} b) \ (\ilist : \iList \ r_1 \ a).$ \\
 	\> $\kcase \ \ilist \ \kof$ \\
 	\> \> $\iNil$			\> $\to \iNil~ r_2~ b~ ()$ \\
 	\> \> $\iCons \ x \ \ixs$ 	\> $\to \iCons~ r_2~ b~ (f~ x)$ \\
	\> \>   \>	\> $(\isuspend$ \> $(\iList~ r_1~ a)~ 
						(\iList~ r_2~ b)~ 
						(e_1 \lor \iRead~ r_1 \lor \iAlloc~ r_2)$ \\
	\> \>	\> 	\> 		\> $(w_1 \lor (\iMkPurifyRead~ r_1~ w_2) \lor (\iMkPurifyAlloc~ r_2~ w_3))$ \\
	\> \>	\>	\>		\> $(\ilazyMap~ a~ b~ r_1~ r_2~ e_1~ w_1~ w_2~ w_3~ f)~ \ixs)$ 
\end{tabbing}

The above function is a lazy version of $\imap$ that constructs the first element of the resulting list when it is called, but leaves subsequent elements to be constructed when they are demanded.

The inner $\kcase$-expression in this definition has the effect $e_1 \lor \iRead~ r_1 \lor \iAlloc~ r_2$. The first part is due to applying the parameter function $f$ to the element $x$, the second due to inspecting the input list, and the third due to allocating the list cells in the result. However, as the recursive call to $\ilazyMap$ is suspended, $\ilazyMap$ itself must be pure. We prove this fact by using the three existing witnesses, $w_1$ guarantees that the effect bound to the variable $e$ is itself pure, while $w_2$ and $w_3$ guarantee that the argument and returned lists are constant.

Note that there are several ways of writing the effect of a pure function. Firstly, the effect $\bot$ is manifestly pure, as it contains no atomic effect terms. However, we can also treat any other effect as pure provided we can produce a witness of the appropriate kind. Our $\ilazyMap$ function clearly must read the list it is applied to, so to force this effect to be pure we require $r_1$ to be constant, hence the $\iConst~ r_1$ constraint. A caller of $\ilazyMap$ must pass a witness that satisfies this constraint, which we bind to $w$, and then use to construct a witness that $\iRead~ r_1$ is pure. We call this process \emph{purifying} an effect, and the constraint $\iConst~ r_1$ is called the \emph{purifier} of $\iRead~ r_1$.


% ------------------------------------------------------------------------------
\subsection{Explicit effect masking}
\label{Explicit-Effect-Masking}
In the previous section, although we were able to construct a witness that $\ilazyMap$ was pure, its type signature still contained the effect term $e_1 \lor \iRead~ r_1 \lor \iAlloc~ r_2$. As as a caller of this function is guaranteed to possess the appropriate witnesses, it will also be able to prove that this effect is pure. However, the type of $\ilazyMap$ is somewhat unsatisfying, because we would prefer if the right-most function arrow had the manifestly pure effect $\bot$. 

We achieve the above by using the $\kmask$ construct, which casts the effect of its body to $\bot$ provided we can provide an appropriate witness of purity. 

\begin{tabbing}
MMMMx \= Mx \= MMMMMx \= MMMM \= MMMxx \= MMMMMM \kill
$\ilazyMap'$ 	\> $::~~  \forall a~ b~ r_1~ r_2~ e_1$\\
		\> $.~~~~ \iPure~ e_1 
				\To	  \iConst~ r_1
				\To 	  \iConst~ r_2$ \\
		\> $\To (a \toa{e_1} b) 
				\to       \iList~ r_1~ a  
				\to       \iList~ r_2~ b$
\end{tabbing}
\begin{tabbing}
Mx \= Mx \= MMMMMx \= MMMM \= MMMxx \= MMMMMM \kill
	$\ilazyMap'$ \\
	 \ $=$	\> $\Lambda a~ b~ r_1~ r_2~ e_1~ 
			(w_1 : \iPure~ e_1)~
			(w_2 : \iConst~ r_1)~
			(w_3 : \iConst~ r_2).$ 
\\
			\> $\lambda (f : a \toa{e_1} b)~ (\ilist : \iList~ r_1~ a).$ \\
			\> $\kmask~ (w_1 \lor (\iMkPurifyRead~ r_1~ w_2) \lor (\iMkPurifyAlloc~ r_2~ w_3))~ \kin$ \\
	 		\> $\kcase~ \ilist~ \kof$ \\
	 		\> \> $\iNil$			\> $\to \iNil~ r_2~ b$ \\
	 		\> \> $\iCons~ x~ \ixs$	
				\> $\to \iCons$ 
					\> $r_2~ b~ (f~ x)$ \\
			\> \>   \>	\> $(\isuspend$ \> $(\iList~ r_1~ a)~ (\iList~ r_2~ b)~ \bot$ \\
			\> \>	\> 	\> 		\> $\iMkPureBot$ \\
			\> \>	\>	\>		\> $(\ilazyMap'~ a~ b~ r_1~ r_2~ e_1~ w_1~ w_2~ w_3~ f)~ \ixs)$ 
\end{tabbing}
The masking is achieved with the $\kmask~ \delta~ \kin~ t$ expression, which contains a witness of purity $\delta$ and a body $t$. The type and value of this expression is the same as for $t$, but its effect is the effect of $t$ minus the terms which $\delta$ proves are pure. As $\ilazyMap'$ itself is now manifestly pure, we can use the $\iMkPureBot$ constructor to satisfy the purity constraint on $\isuspend$. 

% ----------------------------------------------------------------------------
\begin{flushleft}
\textbf{Design Decision: } Explicit witness construction.
\end{flushleft}
While constructing witnesses explicitly is admittedly verbose, it is no more verbose than the code that constructs type class dictionaries in a Haskell compiler such as GHC. Two of the reviewers of an earlier version of this paper asked why we do not remove witnesses from the core language entirely and have the type checker silently reconstruct them when needed. A partial answer to this is simply because witness construction looks so much like dictionary construction. Suppose we defined the following type class instance in Haskell:

\begin{tabbing}
~~ $\kinstance~ \iEq~ a \To \iEq~ (\iList~ a)~ \kwhere~ ...$
\end{tabbing}

This instance introduces a dictionary function in the core language that takes the dictionary providing the equality operators for type $a$ and converts it to a dictionary containing operators for $\iList~ a$. In the GHC core language, $\iEq$ is the type constructor for the record that holds the equality operators, hence our example dictionary function has the following type:

\begin{tabbing}
~~ $\iMkListEq :: \forall a.~ \iEq~ a \to \iEq~ (\iList~ a)$
\end{tabbing}

\begin{flushleft}
Suppose then we defined the following, for some class constructors $\iConst$, $\iPure$, and type constructor $\iRead$.  
\end{flushleft}

\begin{tabbing}
~~ $\kinstance~ \iConst~ r \To \iPure~ (\iRead~ r)~ \kwhere~ ...$
\end{tabbing}

\begin{flushleft}
This would introduce the following dictionary function into the core language:
\end{flushleft}

\begin{tabbing}
~~ $\iMkPurifyRead :: \forall r.~ \iConst~ r \to \iPure~ (\iRead~ r)$
\end{tabbing}

\begin{flushleft}
Here, $\iMkPurifyRead$ is a data constructor, $r$ is a type variable, $\forall$ takes types to types, and $\iConst$,~ $\iPure$,~ $\iRead$ and ($\to$) are all type constructors. 
\end{flushleft}

However, in our case, the $\iConst$ and $\iPure$ ``dictionaries'' are not computationally relevant, meaning that they do not contain any concrete values (like operators) that we need to evaluate the program. Rather, we are just using the dictionary passing mechanism to encode evidence that suspending a computation that reads from a constant region is safe. Because of this, we have chosen to lift the dictionary function one level up into types, to join all the other information that serves no purpose at runtime. The signature for this dictionary function is also lifted, what was once a type signature now becomes a kind signature:

\begin{tabbing}
~~ $\iMkPurifyRead ~::~ \Pi r.~ \iConst~ r \to \iPure~ (\iRead~ r)$
\end{tabbing}

Note that only the ``outer most'' structure is lifted, because the function is still polymorphic over the region variable $r$, which is a type. In this new signature: $\iMkPurifyRead$ is now a type constructor, $r$ remains a type variable, $\Pi$ takes types to kinds, $\iConst$ and $\iPure$ become kind constructors, while $\iRead$ remains a type constructor. 

Instead of lifting dictionary functions in this way, another design option would be to just leave $\iConst$ and $\iPure$ as type constructors, and treat the corresponding dictionaries as ``empty'' values which are implicitly erased at runtime. We have avoided this option for the following reason: as witness applications are erased during code generation, such applications can never cause an effect. All witness applications are manifestly ``pure'', which is a property shared with type applications, but not value applications. This makes witnesses more like types than values. 

As for why we don't have the type checker silently reconstruct witnesses when needed: we feel this wouldn't be helpful in a core language, for a variety of engineering reasons. Firstly, if we simply get tired of looking at witness constructions in our core programs, then they are easy enough to suppress. As we shall see in the next section, well formed witnesses always have the super-kind $\Diamond$, whereas ``regular'' type information has super-kind $\Box$. It would be easy enough to implement a flag in the compiler that causes it to omit type information with super-kind $\Diamond$ in debugging output. GHC has already has an equivalent flag \texttt{-dsuppress-coercions} that suppresses the System-Fc type coercions that arise from its encoding of GADTs \TODO{ref}. Finally, if we were to implement a system that silently reconstructs witnesses then it's highly likely we'd then need to debug it. Such a debugging effort would likely require us to insert tracing statements into the type checker code to understand how it justifies its ability to create each witness. Of course, when witnesses construction is explicit in the core program then this ``debugging'' output comes for free, with the advantage that said output also goes through the type checker!













