
% -- Language -----------------------------------------------------------------
\section{Language}
\label{Language}

We are now in a position to formally define our core language and its typing rules. The structure of the language is given in Fig. \ref{fig:core-language}. Most has been described previously, so we only discuss the aspects not covered so far. Starting at the top of the strata we use super-kinds to classify witness kind constructors, and to ensure they are applied to the right kind of type. For our three baked-in constructors we have the following super-kinds:

\code{
	\iConst		& :: & \% \to \Diamond \\
	\iMutable	& :: & \% \to \Diamond \\
	\iPure		& :: & \ !\  \to \Diamond
}

The first signature says that $\iConst$ may only be applied to a region type, such as with $\iConst \ r_1$. The result of a witness kind constructor is always $\Diamond$, pronounced ``prop". A signature such as $\iConst :: \% \to \Diamond$ is read ``a witness classified by $\iConst$ guarantees a property of a region''. We use $\Box$, pronounced ``box'' as the super-kind for kinds that do not encode such a property, such as $\%$ and $* \to *$.

We use use $\tau_i$ as binders for value types, $\sigma_i$ as binders for effect types, and $\delta_i$ as binders for type expressions that construct witness types. $\Delta_i$ refers to a normal form witness such as $\un{\rho}$, \ $\un{\rconst \ \rho}$, \ $\un{\rmutable \ \rho}$ or $\un{\rpure \ \sigma}$. We use $\varphi_i$ to refer to an arbitrary type expression. 

The values in our term language are identified with $v$. Weak values, $v^\circ$, consist of the values as well as suspended function applications $\isuspend \ \ov{\varphi} \ v_1^\circ \ v_2^\circ$. A suspension is only forced when its (strong) value is demanded by using it as the function in an application, the discriminant of a case expression, or as an argument to a primitive operator such as $\iupdate$. Store locations $l_i$ are discussed in \S\ref{Language:DynamicSemantics}. We require the alternatives of a case-expression to be exhaustive, and data constructors, $suspend$ and $update$ to be fully applied. The other aspects of our term language are standard. Recursion can be introduced via \textbf{fix} in the usual way, but we omit it to save space. 

\medskip
\begin{flushleft}
% -----------------------------------------------------------------------------
\textbf{Design Decision: } Super-kinds
\end{flushleft}
Besides the ability to easily suppress the witness constructions discussed \S\TODO{ref}, we use super-kinds because they are more flexible than simply encoding the predicates $\iConst$,~ $\iMutable$ and $\iPure$ syntactically. Note especially the $\iPure$ constructor, who's argument can be a general effect term rather than a simple variable. Without a syntactically separate effect language (which also do not have), in the absence of super-kinds we would need to introduce a specific rule to check that the application of $\iPure$ to its argument was well formed. For example:
\[	\infer	[\trm{(ValidPure)}]
		{ \Gamma \vdash \iPure~ \sigma ~~\trm{\tbf{valid}}}
		{ \Gamma \vdash \sigma : ~! }
\]
Note that this rule contains exactly the same information that is present in its super-kind above, namely that for the application of $\iPure$ to be valid it must be applied to a well formed effect. As discussed in \TODO{cite} our practical implementation uses more witness kind constructors than the three outlined above, namely $\iLazy$ and $\iDirect$. In \TODO{ref} we will also introduce a sixth, $\iDistinct$. The use of super-kinds gives us the ability to add new witness constructors as needed without requiring new typing rules to be added to our checker. In our implementation we tag each witness kind constructor with its super-kind, so in effect it carries the rule for checking its own validity. A uniform treatment of witness kind constructors also avoids the need new code for parsing, pretty printing, checking for free variables etc each time a new one is added. 

\input{04-Language/Core}

% -----------------------------------------------------------------------------
\subsection{Typing Rules}
\label{Language:TypingRules}

\input{04-Language/SupersOfKinds}
\input{04-Language/KindsOfTypes}

In Fig. \ref{fig:supers-of-kinds} the judgement form $\ksJudgeGS{\kappa}{\omega}$ reads: with type environment $\Gamma$ and store typing $\Sigma$, kind $\kappa$ has super-kind $\omega$. The store typing is an abstract model of the current state of the store, and is discussed further in \S\ref{Language:StoreTypings}. KsAbs is the rule for dependent kind abstraction. Note that a kind signature such as $\% \to *$ is desugared to this form, resulting in $\kiPi{\_}{\%}{*}$.

In Fig. \ref{fig:kinds-of-types} the judgement form $\kiJudgeGS{\varphi}{\kappa}$ reads: with type environment $\Gamma$ and store typing $\Sigma$, type $\varphi$ has kind $\kappa$. Rules KiApp, KiVar and KiAll are standard. Note that KiJoin and KiBot are defined on effect types only. The remainder of the rules give kinds for our ``baked-in'' constructors. We have included $\iList$ and $\iInt$ as representative data type constructors, though in a full language the programmer would be able to define their own. The function type constructor $(\to)$ and the unit type constructor $()$ are special because they are referred to directly in the typing rules of Fig. \ref{fig:TypesOfTerms}. We discuss the kinds of witness types in \S\ref{Language:StoreTypings}.

\input{04-Language/SubsOfEffects}
\input{04-Language/TypesOfTerms}
\input{04-Language/TypesOfAlternatives}

In Fig. \ref{fig:TypesOfTerms} the judgement form $\tyJudgeGS{t}{\tau}{\sigma}$ reads: with type environment $\Gamma$ and store typing $\Sigma$, term $t$ has type $\tau$ and effect $\sigma$. Rules TyVar through TyApp are standard. In TyLetRegion the premise ``$\ov{\delta_i}$ well formed" refers to the syntactic restrictions on the introduced witnesses that were discussed in \S\ref{Witnesses-of-Constancy-and-Mutability}.

Note the premise $r \notin \ifv(\tau)$, also in TyLetRegion. In an entirely strict language this premise would allow us to allocate storage for the region $r$ in a stack-like manner, freeing it once the body of the $\kletregion$ had finished evaluating \cite{tofte:mlkit-4.3.0}. This would be possible because when the variable $r$ does not appear in the type of the result (or in the type environment), objects in this region are not reachable from the calling context. This is not true in a language that supports laziness, such as ours. In our case a ``value'' with a type such as $\iInt~ r_1$ may be represented as a suspended function application, and the suspension may contain references to objects in regions besides $r_1$. This is discussed further in \S\ref{Language:NoStacks}

\TODO{Discuss TyWithRegion, TyAlloc}
The meta-function $\trm{ctorTypes}(T)$ returns a set containing the types of all data constructors associated with a type constructor $T$.

In TyCase, the act of inspecting the discriminant causes the effect $\iRead \ \varphi$, where $\varphi$ corresponds to the data type's first (primary) region variable. The primary variable corresponds to the region containing the outer constructor of the object, which was discussed in \S\ref{Update:SeveralRegionVariables}. The rule for checking the alternatives of a case expression is given in \TODO{ref}. 

In TyUpdate, we must pass the $\iupdate$ operator a witness $\delta$ of kind $\iMutable \ \varphi$. This witness proves that the region holding the constructor to be updated is indeed mutable. Performing the update causes a write effect on this same region. Note that we use the symbol $\varphi$ to represent the region as it can be instantiated by both region variables $r$ and handles $\un{\rho}$. 

In TySuspend, we must pass the $\isuspend$ operator a witness $\delta$ of kind $\iPure \ \sigma$. This proves that the application to be suspended is pure. Note that although the application itself must be pure, the expressions that compute the function and argument need not be, hence the effect term $\sigma_1 \lor \sigma_2$.

TyMaskPure allows us to explicitly mask an effect, provided we can produce a witness of its purity. This was discussed in \S\ref{Explicit-Effect-Masking}.


\input{04-Language/DynamicObjects}

% -----------------------------------------------------------------------------
\subsection{Dynamic Semantics}
\label{Language:DynamicSemantics}
During evaluation, all updatable data is held in the store (also known as the heap), which is defined in Fig. \ref{fig:dynamic-objects}. The store contains bindings that map abstract store locations to store objects. Each store object consists of a constructor tag $C_K$ and a list of weak values $\ov{v^\circ}$. Each binding is annotated with a region label $\rho$ that specifies the region it belongs to. 

The store also contains \emph{properties} that specify how bindings in the various regions may be used. Properties are named after our witnesses from Fig. \ref{fig:core-language}, and are $\rho$, $(\rconst \ \rho)$ and $(\rmutable \ \rho)$. When used as a property, a region handle $\rho$ indicates that the corresponding region has been created and is ready to have bindings allocated into it. The last two indicate whether a binding in a region may be treated as constant, or updated.  

\begin{flushleft}
\textbf{Reminder: } Properties, Witnesses, Witness Constructors and Witness Kind Constructors
As we have now introduced \emph{four} different things named after some version of ``mutable'', this is an opportune time to remind ourselves what they all do. Starting from the bottom:
\end{flushleft}

\begin{itemize}
\item	$\rmutable~ \rho$ -- Store property. We imagine this to be like a `read/write' descriptor in a hardware page table, signalling that bindings in the given region may be mutated. In our semantics this exists in the store, but it is not needed in the physical implementation. 
\item	$\un{\rmutable~ \rho}$ -- Witness. The fact that such a witness occurs in the term guarantees that the associated property exists in the store. This is enforced by the rules in Fig. \ref{fig:KindsOfWitnesses} by also requiring the witness to be in the store typing. Witnesses exist in the term being evaluated, but not in the initial program. The initial program does not contain witnesses because at startup no regions have yet been created. Witnesses are always written with an underline. 
\item	$\iMkMutable$ -- Witness constructor. Constructs a witness that a particular region is mutable. As shown in the next section, our language design ensures that these cannot be reduced to real witnesses unless the associated property actually exists in the store. This is enforced by the rules in Fig. \ref{fig:WitnessConstruction}. Witness constructors (other than $\lor$) always start with ``Mk''. 
\item	$\iMutable$~~ -- Witness Kind Constructor. A witness of kind $\iMutable~ r$ encodes a proof that the region $r$ is indeed mutable. Witness kinds classify witnesses as well as unevaluated witness applications, so we have both $\un{\rmutable~ \rho} :: \iMutable~ \un{\rho}$ and $\iMkMutable~ r :: \iMutable~ r$. 
\end{itemize}
Note the difference between witnesses and properties. Although the two are written similarly, witnesses occur in the term being reduced, whereas properties occur in the store. In our notation, witnesses are always written with an underline, while properties are not.

None of properties, witnesses, witness constructors or witness kind constructors exist in the physical store during evaluation. Only witness constructors and witness kind constructors are used in our practical compiler implementation, while the manifest witnesses and properties are part of the semantics only. 


% -----------------------------------------------------------------------------
\subsection{Witness Construction}
\input{04-Language/PureEffects}
\input{04-Language/KindsOfWitnesses}
\input{04-Language/EvalWitness}
\input{04-Language/EvalOperational}

Fig. \ref{fig:WitnessConstruction} gives the relationship between properties, witnesses and witness constructors. The judgement form $H; \delta \leadsto \delta'$ reads: with store $H$, witness $\delta$ produces witness $\delta'$. As mentioned earlier, properties can be imagined as hardware protection flags on regions of the store --- much like the read, write and execute bits in a hardware page table. The witness constructors $\iMkConst$ and $\iMkMutable$ test for these properties, producing a type-level artefact showing that the property was set. If we try to evaluate either constructor when the associated property is \emph{not} set, then the evaluation becomes stuck. Note that although we use this notion of type-level ``evaluation'' in our semantics, it is not needed at runtime. In our compiler, witnesses are erased during code generation along with all other type information.

The axiom EwPureBot produces a witness that $\bot$ is a pure effect. The remaining rules construct a new witness from existing ones. EwPurifyRead takes a witness that $\rho$ is constant, and produces a witness that a read from this region is pure, likewise for EwPurifyAlloc. The last two are used to take witnesses that two separate effects are pure, and produce a witness that their sum is pure. Note that from Fig. \ref{fig:KindsOfWitnesses}, witness kinds are essentially a singleton kinds after $\TODO{cite: Hayashi, Singleton}$. Given a normal form witness type of kind $\iPure~ \sigma$, the only possible form this can have is $\un{\rpure~ \sigma}$. From the rules in \mbox{Fig. \ref{fig:WitnessConstruction}} we also see that the $\sigma$ can only contain read and allocation effects on regions that are guaranteed to be constant.

% -----------------------------------------------------------------------------
\subsection{Term Evaluation}
In Fig. \ref{fig:TermEvaluation} the judgement form $\evJudgeHH{t}{t'}$ reads: in heap $H$ term $t$ reduces to a new heap $H'$ and term $t'$. In EvLetRegion the propOf meta-function maps a witness to its associated store property. Also, note that the second premise of EvLetRegion is always true, and is used to convert the given witness expressions $\ov{\delta_i}$ to their associated witnesses $\ov{\Delta_i}$. EvAlloc allocates a new binding into the store, which is tagged with the region label applied to its constructor. EvUpdateBind says that to update the value of a binding in region $\rho$ we must pass an appropriate witness $\un{\rmutable~ \rho}$, and the corresponding property $(\rmutable~ \rho)$ must be present in the store. In our soundness theorem discussed in \S\ref{Language:Soundness}, the fact that an update expression of this form can always progress ensures that the binding is indeed mutable. Similarly, in EvSuspendApp we must supply a witness $\un{\rpure~ \sigma}$ that the application to be suspended is pure. EvUpdateFail handles the case where we try to update a binding using an update operator for the wrong data constructor. As different constructors can have a different number of parameters, of different types, we halt the program with the special value ``fail''. EvMask shows that a $\kmask$ expression has no operational effect, besides requiring an appropriate witness of purity.


% -----------------------------------------------------------------------------
\subsection{Store typings}
\label{Language:StoreTypings}
The store typing $\Sigma$ models the state of the heap as the program progresses, and was defined in Fig. \ref{fig:core-language}. The store typing contains the type of each store location, along with witnesses to the current set of store properties. We say that the store typing \emph{models} the store, and write $\Sigma \models H$, when all members of the store typing correspond to members of the store. Conversely, we say the store is \emph{well typed}, and write $\Sigma \vdash H$ when it contains all the bindings and properties predicted by the store typing. These are defined formally below. Both the store and store typing grow as the program evaluates, and neither bindings, properties or witnesses are removed once added. 

\pagebreak{}
% -------------------------------------------------------------------------------------------------
\begin{definition}[Store Model ~ $\Sigma \models H$]
Given a store typing $\Sigma$ and a store $H$, the store typing \emph{models} the store, written $\Sigma \models H$ when all elements of the store typing correspond to elements of the store.

\medskip
\begin{tabular}{llll}
	for all 	&~ $l :: T~ \un{\rho}~ \ov{\varphi} \in \Sigma$ 
	&~ we have	&~ $l \mtoa{\rho} C_K~ \ov{v^\circ} \in H$ 
\\
	for all		&~ $\un{\rho} \in \Sigma$ 
	&~ we have	&~ $\un{\rho} \in H$
\\
	for all		&~ $\un{\rmutable~ \rho} \in \Sigma$ 
	&~ we have	&~ $\rmutable~ \rho \in H$
\\
	for all		&~ $\un{\rconst~ \rho} \in \Sigma$ 
	&~ we have	&~ $\rconst~ \rho \in H$
\end{tabular}
\end{definition}

% -------------------------------------------------------------------------------------------------
\begin{definition}[Well Typed Stores~ $\Sigma \vdash H$]
	
Given a store typing $\Sigma$ and a store $H$, the store is \emph{well typed} relative to the store typing, written $\Sigma \vdash H$ when all elements of the store correspond to elements in the store typing.

\medskip
\statement{
	for all 	&~ $l \mtoa{\rho} C_K~ \ov{v^\circ} \in H$ \\
	~ we have	&~ $l :: T~ \un{\rho}~ \ov{\varphi} \in \Sigma$ \\
	~ and		&~ $K :: \forall(r : \%)(\ov{a : \kappa}). \ov{\tau} \to T~ r~ \ov{a} \in \trm{ctorTypes}(T)$ 
\\
	~ and 		&~ $\ov{\tyJudgeES
				{v^\circ_i}
				{\tau_i[\un{\rho}/r~ \ov{\varphi/a}]}
				{\bot}}^{~ i}$
}

\hspace{-2em}
\begin{tabular}{llll}
	for all		&~ $\rho \in H$
	&~ we have	&~ $\un{\rho} \in \Sigma$ 
\\
	for all		&~ $\rmutable~ \rho \in H$
	&~ we have	&~ $\un{\rmutable~ \rho} \in \Sigma$ 
\\
	for all		&~ $\rconst~ \rho \in H$
	&~ we have	&~ $\un{\rconst~ \rho} \in \Sigma$
\end{tabular}
\end{definition}

\bigskip

Although most of the typing rules from Figs \ref{fig:supers-of-kinds}, \ref{fig:kinds-of-types} and \ref{fig:TypesOfTerms} simply pass the store typing through unchanged, it is used in TyLoc from Fig. \ref{fig:TypesOfTerms} to determine type of a store location $l$. However, as kind expressions can contain types, and hence store locations as well, the store typing must be a part of all judgement forms.

Store typings are also used in Fig. \ref{fig:KindsOfWitnesses}, which gives kinds to witnesses. The judgement form $\kiJudgeGS{\Delta}{\kappa}$ reads: with type environment $\Gamma$ and store typing $\Sigma$, witness $\Delta$ has kind $\kappa$. This is similar to the one in Fig. \ref{fig:kinds-of-types}. Importantly, in the first four rules in Fig. \ref{fig:KindsOfWitnesses}, when we give a kind to a witness we \emph{require} that witness to also be in the store typing. Provided the store typing models the store, this also means that the corresponding property is in the store. 


% -------------------------------------------------------------------------------------------------
\begin{lemma}[Forms of Purity]
In latter proofs we will need to reason directly about forms of witnesses that \emph{cannot} be well kinded. To support this reasoning we introduce three simple lemmas about the form of the Pure Effects judgement in Fig. \ref{fig:PureEffects}. 

\medskip
\begin{tabular}{ll}
	If~	& $\un{\rmutable~ \rho} \in \Sigma$	then $\neg(\pureJudgeS{\iRead~ \un{\rho}})$ 
\\[1ex]
	If~ 	& $\un{\rmutable~ \rho} \in \Sigma$	then $\neg(\pureJudgeS{\iAlloc~ \un{\rho}})$ 
\\[1ex]
	\mc{2}{$\neg(\pureJudgeS{\iWrite~ \un{\rho}})$}
\end{tabular}
\end{lemma}

\medskip
We use $\neg S$ to mean statement S is neither an axiom of our system, or can be derived via inference rules. Each of the above lemmas can be verified directly from Fig. \ref{fig:PureEffects}, and recalling from \TODO{ref} that the definition of the Store Typing ensures that if the witness $\un{\rmutable~ \rho}$ is present then there is not also a witness $\un{\rconst~ \rho}$.


\clearpage{}
% -------------------------------------------------------------------------------------------------
\begin{lemma}[No Purification of Impurity]
If $\sigma$ is a read, write or allocation effect on a mutable region, and $\sigma'$ is an effect at least as big as $\sigma$, then we cannot infer that $\sigma'$ is pure. 

\medskip
\begin{tabular}{ll}
	If~	& (\un{1})~ 	$\suJudgeGS{\sigma}{\sigma'}$ ~~for $\sigma$ ~one of~
				$\iRead~ \un{\rho}$,~ $\iWrite~ \un{\rho}$,~ $\iAlloc~ \un{\rho}$ 
\\
	~and~	& (\un{2})~	$\un{\rmutable~ \rho} \in \Sigma$ 
\\[0.5ex]
	then~~	& $\neg(\suJudgeGS{\sigma'}{\bot})$
\end{tabular}
\end{lemma}

This lemma guarantees that our system cannot wrongly infer that impure effects are actually pure. This is the key soundness property for the rules of Figs. \ref{fig:PureEffects}, \ref{fig:KindsOfWitnesses} and \ref{fig:SubsumptionOfEffects}. We will use it in the proofs of Visible and Invisible effects in the next section.
 

\begin{proof}
By induction over the derivation of $\suJudgeGS{\sigma}{\sigma'}$

\tabbedstmts{
~~	(IH)	\> No Purification... holds for all subderivations of $\suJudgeGS{\sigma}{\sigma'}$.
\\
	\> Assume (\un{1}) (\un{2}). 
\\
~~	(\un{3}) \> Suppose we had a derivation of $\suJudgeGS{\sigma'}{\bot}$
\\
~~	(4)	\> ~~ Case: $\sigma' = \bot$
\\
~~	(5)	\> ~~~~~ $\suJudgeGS{\sigma}{\bot}$
		\> (4 1)
\\
~~	(6)	\> ~~~~~ Case: $\sigma = \iRead~ \un{\rho}$
\\
~~	(7)	\> ~~~~~~~~ $\suJudgeGS{\iRead~ \un{\rho}}{\bot}$
		\> (5 6)
\\
~~	(8)	\> ~~~~~~~~ $\kiJudgeGS{\un{\rpure~ (\iRead~ \rho)}}{\iPure~ (\iRead~ \un{\rho})}$
		\> (Inv. SubPure 7)
\\	
~~	(9)	\> ~~~~~~~~ $\pureJudgeS{\iRead~ \un{\rho}}$
		\> (Inv. KiPure 8)
\\
~~	(10)	\> ~~~~~~~~ $\neg(\pureJudgeS{\iRead~ \un{\rho}})$
		\> (Forms of Purity 2)
\\
~~	(11)	\> ~~~~~~~~ Contradiction
		\> (9 10)
\\
		\> ~~~~~ Cases for $\sigma$ one of $\iWrite~ \un{\rho},~ \iAlloc~ \un{\rho}$ similarly.
\\
~~	(12)	\> ~~ Case: $\sigma' \ne \bot$
\\
~~	(13)	\> ~~~~~ $\suJudgeGS{\sigma'}{\bot}$
		\> (Restate 3)
\\
~~	(14)	\> ~~~~~ Case: $\sigma'$ one of $\iRead~ \un{\rho}$,~ $\iWrite~ \un{\rho}$,~ $\iAlloc~ \un{\rho}$
\\		
~~	(15)	\> ~~~~~~~ Contradiction
		\> (As per 5-11)
\\
~~	(16)	\> ~~~~~ Case: $\sigma' = \sigma_1 \lor \sigma_2$
\\
~~	(17)	\> ~~~~~~~~ $\suJudgeGS{\sigma}{\sigma_1 \lor \sigma_2}$
		\> (1 16)
\\
~~	(18 19) \> ~~~~~~~~ $\suJudgeGS{\sigma}{\sigma_1}$ ~~~~~~~~or~~~~ $\suJudgeGS{\sigma}{\sigma_2}$
		 \> (Inv. 17)
\\
~~	(20 21)	\> ~~~~~~~~ $\neg(\suJudgeGS{\sigma_1}{\bot})$ ~~or~~~~  $\neg(\suJudgeGS{\sigma_2}{\bot})$
		\> (IH 18 19 2)
\\
~~	(22)	\> ~~~~~~~~ $\suJudgeGS{\sigma_1 \lor \sigma_2}{\bot}$
		\> (13 16)
\\
~~	(23 24)	\> ~~~~~~~~ $\suJudgeGS{\sigma_1}{\bot}$,~~~~~~~~~~~~~~~ $\suJudgeGS{\sigma_2}{\bot}$
		\> (Inv. 22)
\\
~~	(25)	\> ~~~~~~~~ Contradiction
		\> (20 21 23 24)
\\
~~	(26)	\> $\neg(\suJudgeGS{\sigma'}{\bot})$
		\> (Neg. Intro. 3-25)
}
\end{proof}

\pagebreak{}
% -----------------------------------------------------------------------------
\subsection{Soundness}
\label{Language:Soundness}
Our proof of soundness is split into Progress and Preservation (subject reduction) theorems in the usual way. The proof is fairly routine, and is given in the Appendix.
\smallskip

\begin{theorem}[Progress]
\begin{tabbing}
MM \= MMx \= MMMMMMMMMMMM \kill
\>	If~ 	\> $\tyJudge{\emptyset}{\Sigma}{t}{\tau}{\sigma}$ 
			~and~ $\Sigma \models H$ 
			~and~ $\Sigma \vdash H$ 
			~and~ $\trm{nofab}(t)$  \\
\>	then~~	\> $t \in \trm{Value}$  \\
\>	~or~~	\> for some $H', t'$ we have ($H ; t \eto H' ; t'$ and $\trm{nofab}(t')$ or $H ; t \eto H' ; \trm{fail}$)
\end{tabbing}
\end{theorem}


\begin{theorem}[Preservation]
\begin{tabbing}
MM \= MMx \= MMMMMMMMMMMM \kill
\>	If~	\> $\tyJudgeGS{t}{\tau}{\sigma}$ 
			and $\Sigma \models H$ 
			and $\Sigma \vdash H$ \\
\>	and~~	\> $H ; t \eto H' ; t'$ \\
\>	then 	\> for some $\Sigma', \sigma'$ we have  \\
\>		\> ~~$\tyJudge{\Gamma}{\Sigma'}{t'}{\tau}{\sigma'}$ \\
\>		\> ~~and $\Sigma' \supseteq \Sigma$ and $\Sigma' \models H'$ and $\Sigma' \vdash H'$ and $\sigma' \tle \sigma$.
\end{tabbing}
\end{theorem}

\medskip

In the Progress Theorem, ``nofab'' is short for ``no fabricated region witnesses'', and refers to the syntactic constraint discussed in \S\ref{Witnesses-of-Constancy-and-Mutability} that $\iMkConst$ and $\iMkMutable$ may only appear in the witness binding of a $\kletregion$, and not elsewhere in the program.

In the Preservation Theorem, note that the latent effect of the term reduces as the program progresses. The $\sqsubseteq$ relationship on effects is defined in Fig. \ref{fig:SubsumptionOfEffects}. Most of this relationship is standard, apart from the TyMaskPure rule. This rule says that if we can construct a witness that a particular effect is pure, then we can treat it as such. This allows us to erase read effects on constant regions during the proof of Preservation. It is needed to show that forcing a suspension does not have a visible effect, and that we can disregard explicitly masked effect terms when entering into the body of a $\kmask$-expression.

As mentioned in the previous section, our typing rules ensure that if a witness occurs in the term being reduced, then it also occurs in the store typing. Provided the store typing models the store, this also means that the corresponding property is present in the store. From the evaluation rules of Fig. \ref{fig:TermEvaluation}, the only term that adds properties to the store is $\kletregion$, and when it does, it also introduces the corresponding witnesses into its body. The well-formedness restriction on $\kletregion$ guarantees that a witness of mutability and constancy for the same region cannot be created. This ensures that if we have, say, the witness $\un{\rconst~ \rho}$ in the term, then there is \emph{not} a $(\rmutable~ \rho)$ property in the store. This means that bindings in those regions can never be updated, and it is safe to suspend function applications that read them. \TODO{ref to proof of this property}. 

As a final point, note that although we support destructive update of arbitrary data, we do not suffer the potential unsoundness commonly associated with ML-style mutable references \cite{garrigue:relaxing}. Although our Progress and Preservation theorems ensure that our core language by itself is sound, for a compiler using a System-F core language, problems can arise when erasing type abstractions during code generation. The issue is that erasing type abstractions converts what where once type functions into values, which introduces sharing that was not present in the original program \cite{leroy:polymorphism-by-name}. However, in our system, by the TyAbsT rule from Fig. \ref{fig:TypesOfTerms} the body of a type abstraction cannot have a visible effect. This means that it cannot (visibly) allocate mutable data, and erasing type abstractions during code generation does not cause a problem. Of course, we can still write polymorphic functions that allocate \emph{constant} data simply by masking the allocation effect using the appropriate witness of constancy. In DDC itself, when performing type inference for the source language we use closure typing \TODO{cite} to ensure that offending types are not generalised, though one has to be careful about the order in which the constraints are processed \TODO{cite}. Restricting generalisation during type inference then ensures that erroneous expressions are not produced when translating the source language to core. 


% -------------------------------------------------------------------------------------------------
\subsection{Allocation, Suspension and Region Phase Changes}
\label{Language:NoStacks}
The design of our type and evaluation rules for $\kletregion$ has been through several revisions. Along the way we have learned quite a bit about the design of a formal semantics, from reviewers of previous versions of this paper, and from the simple act of trying something seemingly reasonable and then finding out days later that it was never going to work in the first place. In this section we present several of our initial attempts, which illustrate why our final system separates uses both $\kletregion$ and $\kwithregion$ to manage regions. The operation of these two forms was first discussed in \TODO{ref}. 


% -------------------------------------
\begin{flushleft}
\textbf{Unhygenic letregion}
\end{flushleft}
Our original attempt was as follows. The ``UH'' in the rule names stands for ``un-hygenic" which we will discuss in a moment. 

\smallskip
\[	\infer	[\trm{(TyLetR-UH)}]
		{ \tyJudgeGS
			{\teLetR
				{r}
				{\ov{w_i = \delta_i}}
				{t}
			}
			{\tau}
			{\sigma}
		}
		{ \begin{array}{lll}
		     \ov{\delta_i}~ \trm{well formed} 
		     & 
		     \ov{\kiJudgeGS{\delta_i}{\kappa_i}}^{~i}
		     &
	  	     \tyJudge
			{\Gamma,~ r : \%,~ \ov{w_i : \kappa_i}}
			{\Sigma}
			{t}
			{\tau}
			{\sigma}
		  \end{array}
		}
\]

\[	\infer	[\trm{(EvLetR-UH)}]
		{ \evJudge
			{H}	{\teLetR{r}{\ov{w_i = \delta_i}}{t}}
			{H'}	{t[\un{\rho}/r~ \ov{\Delta_i/w_i}]}
		}
		{ \rho~ \trm{fresh}
		  \qq
		  H' = H,~ \rho,~ \ov{\rpropOf(\delta_i[\rho/r])}
		  \qq
		  \ov{\Delta_i} = \ov{\rwitOf(\delta_i[\rho/r])}
		}
\]

Note that we have not included the $r \notin \ifv(\tau)$ premise in TyLetR-UH. This premise is standard from the MLKit system \cite{tofte:mlkit-4.3.0} which uses regions to allocate and deallocate storage in a stack like manner. However, we did not include the premise because, as mentioned in \TODO{ref}, we are using regions for alias control only and not allocation. In a strict language such as MLKit, the premise $r \notin \ifv(\tau)$ ensures that the result of the expression in the body of a $\kletregion$ cannot reference the new region, and hence the region can be deallocated after the reduction is complete. However, this trick doesn't work for a typical lazy language because ``value'' of a type like $\iInt~ r_1$ may actually be a thunk which is referencing data in regions other than $r_1$. Hence, until the thunk is completely evaluated, the referenced regions cannot be deallocated. As our language supports laziness, and were not using regions for allocation, we opted to omit the $r \notin \ifv(\tau)$ premise from TyLetR-UH. Although this is fine with respect to the practical compiler implementation, it creates problems in the semantics for a variety of reasons. 

The first problem is that the evaluation of a $\kletregion$ expression doesn't preserve its typing in the usual manner. For example, consider the following reduction, where we have elided the set of witness bindings because they are not needed in this instance.
\code{
	\evJudge
		{\emptyset}
		{\teLetRE{r}{\iTrue~ r~ ()}~~}
		{~~\rho}
		{\iTrue~ \un{\rho}~ ()}
}
Although the term on the left has type $\iBool~ r$, the term on the right has type $\iBool~ \un{\rho}$. We initially thought this was a feature. The first type says that the term is an unevaluated expression that will produce a boolean object into a region that has not yet been created, while the second reveals that it will produce one into an existing region named $\rho$. The problem is that to prove a Preservation theorem we must keep track of the mapping between region variables and their associated region handles, to justify why $\iBool~ r$ and $\iBool~ \un{\rho}$ are equivalent. It is quite possible to do this, but plumbing the mapping around the proof and typing rules complicates them significantly. A related problem is that the result type $\iBool~ \un{\rho}$ cannot be kind checked in the initial environments $\Gamma$ and $\Sigma$, which is a difference from every other evaluation rule. To say this another way, the new region handle $\rho$ ``leaks'' out of the typing rule, making it un-hygenic. 

In our original formulation we also presented effect masking in a separate rule, similarly to the system of \TODO{ref}, instead of folding it into (TyLetR-UH). The masking rule implements the \emph{observation criteria}, which says that if the reduction of some expression has an effect, but that effect is not visible to the calling context, then we can safely ignore it. 

\[	\frac
	{ \tyJudgeGS
		{t}
		{\tau}
		{\sigma}
	 \quad
	 r \notin fv_T(\Gamma)
	 \quad
	 r \notin fv(\tau)
	}
	{ \tyJudgeGS
		{t}
		{\tau}
		{\sigma \setminus (\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)}
	}
	\qq \trm{(TyObs-UH)}
\]

In the above rule, the premise $r \notin fv_T(\Gamma)$ refers to free variables in type bindings only. For example, we allow a plain $r : \%$ to appear in the environment provided $r$ it is not also free in the $\tau'$ of any $x : \tau'$. The reasoning why TyObs is valid is standard and fashioned after \cite{talpin:type-and-effect-discipline}. As $r$ does not appear in any type binding in the environment, the term $t$ cannot hold a direct reference to pre-existing objects in this region. It may hold an indirect reference via a suspended function application, but as suspended applications must be pure their final values cannot be affected once the suspension is created. As $r$ does not appear in the return type, we cannot hold a direct reference to any object in $r$
after the term has finished evaluating. 

The problem with presenting such a rule separately is that, once again, it complicates the proof of Preservation. This rule is not syntax directed, meaning that it could be invoked at at any point in the typing derivation. This presents no problems for the compiler implementation, but it does for the proof, as we must factor it in to each of our inversion lemmas \TODO{cite}. Another option would be to prove Preservation separately from TyObs-UH, and then try to argue that adding it does not affect the original result. However, this spoils the simple ``proof by induction over the structure of the typing derivation'' reasoning common to many such proofs. 

% -------------------------------------
\begin{flushleft}
\textbf{Combined letregion}
\end{flushleft}
Faced with the problems of unhygienic typing rules, our next attempt was to simply add back the $r \in \ifv(\tau)$ premise to TyLetR-UH and fold the effect masking into the same rule. This leaves us with TyLetR-C below, where ``C'' is short for ``Combined''. 


\[	\infer	[\trm{(TyLetR-C)}]
		{ \tyJudgeGS
			{\teLetR
				{r}
				{\ov{w_i = \delta_i}}
				{t}
			}
			{\tau}
			{\sigma \setminus (\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)}
		}
		{ \begin{array}{lll}
		     & 
		     &
		     \ov{\kiJudgeGS{\delta_i}{\kappa_i}}^{~i}
		     \\ 
		     \ov{\delta_i}~ \trm{well formed} 
		     &
		     r \notin \ifv(\tau)
		     &
    	  	     \tyJudge
			{\Gamma,~ r : \%,~ \ov{w_i : \kappa_i}}
			{\Sigma}
			{t}
			{\tau}
			{\sigma} 
		  \end{array}
		}
\]

Sadly, this approach still doesn't work with the Preservation theorem. The trouble is that the region phase change also alters the effect of a term as well as its type. For example, consider the following reduction:

\[	\begin{array}{lll}
		& \emptyset & ;~~~~ \kletregion~ r~ \kin~ \klet~ \_ = \iTrue~ r~ ()~ \kin~ () \\
	\longto & \rho 	    & ;~~~~ \klet~ \_ = \iTrue~ \un{\rho}~ ()~ \kin~ ()
	\end{array}
\]

Whereas the initial expression has effect $\iAlloc~ r$, the result has effect $\iAlloc~ \un{\rho}$. Note that we really do want to incorporate the phase change somehow, because if we had not substituted $\un{\rho}$ for $r$ in the result then $r$ would now be free. 

% -------------------------------------
\begin{flushleft}
\textbf{Hermetic letregion}
\end{flushleft}
As our immediate problem stems from region handles leaking into the type and effect of the body of the $\kletregion$, one might wonder if we could add a $r \notin \ifv(\sigma)$ premise to seal the effect of the term in the same way that $r \notin \ifv(\tau)$ seals its type. This leads us to TyLetR-H below, where ``H'' is short for ``Hermetic'' (meaning air-tight). 

\[	\infer	[\trm{(TyLetR-H)}]
		{ \tyJudgeGS
			{\teLetR
				{r}
				{\ov{w_i = \delta_i}}
				{t}
			}
			{\tau}
			{\sigma}
		}
		{ \begin{array}{lll}
		     & 
		     r \notin \ifv(\tau)
		     &
		     \ov{\kiJudgeGS{\delta_i}{\kappa_i}}^{~i}
		     \\ 
		     \ov{\delta_i}~ \trm{well formed} 
		     &
		     r \notin \ifv(\sigma)
		     &
    	  	     \tyJudge
			{\Gamma,~ r : \%,~ \ov{w_i : \kappa_i}}
			{\Sigma}
			{t}
			{\tau}
			{\sigma} 
		  \end{array}
		}
\]

Adding the $r \notin \ifv(\sigma)$ solves the problem with the region phase change, or rather, it pushes it into another part of the system. Note that now $\sigma$ cannot mention \emph{any} effect involving $r$. Without an additional masking rule such as TyObs-UH, we cannot actually make use of the new region. We are now faced with either a degenerate system, or the same lack of syntax-directedness discussed earlier. 

% -------------------------------------
\begin{flushleft}
\textbf{Split letregion / withregion}	
\end{flushleft}
Our solution, of course, is to split the problem into two. We use $\kletregion$ to create the region handle as before, and $\kwithregion$ to hold this handle while the body evaluates. Only $\kletregion$ is required in the initial program, whereas $\kwithregion$ models ``the stack frame'' during evaluation. Here are the final rules, repeated from Fig. \ref{fig:TypesOfTerms} and Fig. \ref{fig:TermEvaluation}.


\medskip
\[	\ruleIL	{TyLetR}
		{ \begin{array}{lll}
		  &&
			\ov{\kiJudgeGS
				{\delta_i}
				{\kappa_i}}^{\ i}
		  \\
			\ov{\delta_i} \ \trm{well formed}
		  & 
			{r \notin \ifv(\tau)}
		  & 
		        \tyJudge	
				{\Gamma, \ r : \%, \ \ov{w_i : \kappa_i}}
				{\Sigma}
				{t}
				{\tau}
				{\sigma} 
		  \end{array}
		}
		{ \tyJudgeGS
			{\teLetR{r}{\ov{w_i = \delta_i}}{t}} 
			{\tau} 
			{\sigma \setminus {(\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)}}
		}
\]

\[	\ruleIL	{TyWithR}
		{ \un{\rho},~ \ov{\Delta_i} \in \Sigma
		  \qq 
		  \tyJudgeGS
			{t}
			{\tau}
			{\sigma}
		}
		{ \tyJudgeGS
			{\teWithR{\un{\rho}}{\ov{\Delta_i}}{t}}
			{\tau}
			{\sigma \setminus {(\iRead~ \un{\rho} \lor \iWrite~ \un{\rho} \lor \iAlloc~ \un{\rho})}}
		}
\]

\bigskip

\[	\ruleIL	{EvCreateR}
		{ \rho~ \trm{fresh}
		  \quad
		  \ov{\Delta_i = \rwitOf(\delta_i[\un{\rho}/r])}^{~ i}
		  \quad
		  \ov{\pi_i    = \rpropOf(\delta_i[\un{\rho}/r])}^{~ i}
		  \quad
		  H' = H,~ \rho,~ \ov{\pi_i}
		}
		{ \evJudge
			{H}
			{\kletregion \ r \ \kwith \ \{ \ov{w_i = \delta_i} \} \ \kin \ t}
			{H'}
			{ \teWithR
				{\un{\rho}}
				{\ov{\Delta_i}}
				{t[\un{\rho}/r~ \ov{\Delta_i/w_i}]}
			}
		}
\]
\[	\ruleAL	{EvEjectR}
		{ \evJudge
		  	{H}	{\teWithR
					{\un{\rho}}
					{\ov{\Delta_i}}
					{v^\circ}}
		  	{H}	{v^\circ}
		}
\]
\smallskip

\TODO{No more EvWithR. Say that we could dealloc the region if we could guarantee there were no suspensions being referenced by the returned value}.

The TyWithR rule now provides a place in the semantics to mask effect terms which have undergone the phase change. The EvCreateR rule creates the new region handle, substitutes the new region and witnesses into the term, then wraps both in a $\kwithregion$. EvWithR then takes over and continues evaluating the term until it has reached a (weak) value, after which it is ejected from the $\kwithregion$ construct by EvEjectR. The type and effect of the term is preserved at all times. 

Note that in EvEjectR we must return the region handle $\rho$ as well as its corresponding properties in the resulting heap. This is because we allow the resulting term to be a \emph{weak} value, $v^\circ$, which includes suspensions. As stated earlier, a suspension may refer to heap locations in regions that are not visible in its type. This means that we cannot deallocate whole regions for risk of breaking these references. 

Of course, the fact that we cannot deallocate regions in our formal semantics does not mean we cannot deallocate memory in our practical implementation. For the DDC runtime we use garbage collection for storage management, though admittedly it would be nice if we could perform some region based memory management as well. A related issue is whether it is sound to deallocate regions that are referenced by a suspension but never actually used. For example, the expression $\isuspend~ (\lambda. ())~ l$ has type $()$ and effect $\bot$, yet references at least one region via the location $l$. If we take locations as corresponding to pointers in the practical implementation, then deallocating the region associated with $l$ invalidates the associated pointer. We leave this as a topic for future work. \TODO{cite paper mixing regions with garbage collection}. 





