%!TEX root = ../../Main.tex

\pagebreak{}
\subsection{Types of Configurations and Frame Stacks}
\label{s:Configurations}

A configuration combines a frame stack $\mfs$ with some expression $x$ and is written $\mfs/x$. As discussed earlier, the frame stack describes the context in which the expression evaluates. The typing rules for configurations and frame stacks are given in Fig.~\ref{f:TypeC}. At the top of the figure, the judgment $\TypeC{\mke}{\mte}{\mse}{\msp}{\mfs}{x}{t}{e}$ reads: ``with kind environment $\mke$, type environment $\mte$, store environment $\mse$ and store properties $\msp$, frame stack $\mfs$ with expression $x$ has type $t$ and effect $e$''. The second judgment form checks the frame stack itself, where $\TypeF{\mke}{\mte}{\mse}{\msp}{\mfs}{t_1}{t_2}{e}$ reads ``... frame stack $\mfs$ takes an expression of type $t_1$ to a result of type $t_2$, causing effect $e$''. Here, the effect $e$ is the effect of evaluating all the suspended let-continuations contained on the stack.

In Fig.~\ref{f:TypeC}, rule (TcExp) checks the type of an entire configuration. As with the other rules in the same figure, (TcExp) is a ``dynamic typing'' rule that is only needed when checking the program during evaluation. Before a source program has commenced evaluation it has no associated frame stack, so the static typing rules of Fig.~\ref{f:TypeX} suffice to check it. The premise $\EquivT{\mke}{\msp}{e_1 + e_2}{e_3}{\kcEffect}$ is needed to normalize the syntactic form of the overall effect $e_3$. The premise allows us to treat an effect term such as ($e_1 + \bot$) as simply $e_1$, and use the usual commutativity and associativity properties of $+$. In hand written proofs these properties are typically used without mention, but in a mechanical proof we must be explicit. The equivalence judgment itself is defined in Fig.~\ref{f:EquivT} and discussed in the next section.

Rule (TcNil) shows that an empty frame stack takes an expression of type $t$ to another expression of type $t$ (itself), performing no effects. 

Rule (TfConsLet) gives the type of a frame stack where the top most frame is a let-continuation. Recall that a let-continuation holds the body of a let-expression while the binding is being evaluated. In the rule, the binding has type $t_1$ and the body $x_2$ has type~$t_2$. As per rule (SfLetPop) from Fig.~\ref{f:Step}, once the let-binding has reduced to a value it will be substituted into the body $x_2$ held in the let-continuation. Further evaluation of the body will then produce a value of type $t_2$ which will cause the next frame on the rest of the stack $\mfs$ to be popped, and so on. For this reason $\mfs$ has type $t_2 \multimap t_3$, where $t_3$ is the type of the overall value that the configuration produces. 

Rule (TfConsPriv) gives the type of a frame stack with a ~$\fprivd{p}$~ frame on top, for some region identifier $p$. Recall from the discussion of (SfPrivatePop) in \S\ref{s:Steps-Deallocation} that a frame ~$\fprivd{p}$~ indicates that when the expression being evaluated has reduced to a value then we should deallocate all store bindings in region $p$ and pop the frame. Unlike the previous case with (SfLetPop), in this case when we pop the frame we keep the original value, so the rest of the stack $\mfs$ must also accept this value --- hence we have $t_1 \multimap t_2$ in both the premise and conclusion. The premise ~$\trm{NoPrivFs}~ p~ \mfs$~ says that the region identifier $p$ cannot be mentioned in @priv@ frames in the rest of the stack $\mfs$, which inductively ensures that all region identifiers in @priv@ frames on the stack are distinct. Finally, the premise $\LiveS{\mfs}{e_2}$ ensures that the liveness of the overall stack ($\mfs,~ \fprivd{p})$ relative to $e_2$ will be preserved once we come to pop the $\fprivd{p}$ frame later in the evaluation.


% -----------------------------------------------
\input{figures/TypeC.tex}


Rule (TfConsExt) gives the type of a frame stack with a ~$\fprivm{p_1}{p_2}$~ frame on top, for outer and inner region identifiers $p_1$ and $p_2$. From the discussion of rule (SfExtendPop) from \S\ref{s:Steps-Deallocation}, recall that the frame $\fprivm{p_1}{p_2}$ indicates that when the expression being evaluated has reduced to a value, then we should merge region $p_2$ into region $p_1$ and pop the frame. The merging process rewrites $p_2$ into $p_1$ in both the value and in all store bindings, hence we must also rewrite the type of the value to match. The rest of the stack $\mfs$ thus has type $(\trm{mergeT}~ p_1~ p_2~ t_1) \multimap t_2$, as it expresses a continuation that takes the value after merging.

The premise ~$\trm{FreshFs}~ p_2~ \mfs$~ says that none of the frames in stack $\mfs$ may mention the region identifier $p_2$, which prevents it from appearing in let-continuation frames as well as @priv@ frames. This FreshFs predicate is stronger than the NoPrivFs predicate used in rule (TfConsPriv). We need the stronger version here because if an intermediate let-continution in $\mfs$ actually did mention $p_2$ then its type would also change during the merging process. However, at runtime such a let-continuation cannot be constructed, because from the form of the stack we know that $p_2$ will have been created after any let-continuations deeper in the stack were pushed. The premise ~$\trm{FreshSuppFs}~ p_2~ \mse~ \mfs$~ says that for all store locations mentioned in $\mfs$, their corresponding types from $\mse$ cannot mention region identifier $p_2$ (where ``Supp'' is short for ``Support''). This premise is needed for the same reason as the previous one: if $\mfs$ mentioned any locations that had types involving $p_2$ then these would change during merging, but such locations cannot exist because $p_2$ is guaranteed to be created after the locations. 

