
\section{Related Work}
The inspiration for our work has been to build on the monadic intermediate languages of \cite{tolmach:optimizing-ml}, \cite{benton:monads-effects-transformations} and \cite{peyton-jones:bridging-the-gulf}. Note that for our purposes, the difference between using effect and monadic typing is largely syntactic. We prefer effect typing because it mirrors our operational intuition more closely, but \cite{wadler:marriage-2003} gives a translation between the two.  Our system extends the previous with region, effect and mutability polymorphism, which improves the scope of the optimisations that can be performed. The work of  \cite{benton:relational-semantics-effect-transformations} and \cite{benton:semantics-effect-analysis}, presents monadic languages that include region and effect polymorphism, but does not consider mutability polymorphism or lazy evaluation. The roots of effect polymorphism lie in \cite{lucassen:polymorphic-effect-systems} which also uses a System-F based language. 

Our notion of a ``witness'' is derived from from a long line of work on typed intermediate languages \cite{tarditi:til}, typed assembly languages \cite{morrisett:system-f-to-typed-assembly-language} and \emph{proof carrying code} \cite{necula:proof-carrying-code}. However, in the last two of these systems the focus is guaranteeing the safety of programs that use low level operations such as strong update, that is, destructive update that changes the \emph{type} of a heap location as well as its value. In contrast, we do not support such an operation, and our focus is on justifying the transformation of specialised versions of a function. 

The Capability Calculus \cite{crary:capabilities} provides region based memory management, whereby a capability is associated with each region, and an expression can only access a region when it holds its capability. When the region is deallocated, its associated capability is revoked, ensuring soundness. The Vault language of \cite{deline:vault} is related. Although the capabilities of \cite{crary:capabilities} have similarities to the witnesses of our system, theirs are not reified in the term being evaluated, and we do not allow ours to be revoked.

An important consideration of our work is to keep the programs digestible by humans. As our system is used as the core language of a larger compiler we spend a substantial amount of time staring at programs written in it. The fact that information about mutability, purity and aliasing is reified and explicit in the core program helps us, as compiler developers, to reason about the compilation process. In this respect our approach is closer to \cite{terauchi:witnessing-side-effects}. This system also uses type level witnesses that are explicitly threaded through the program. They then provide a mechanism to check for \emph{witness race freedom}, meaning that a program using side effects has enough data dependencies to ensure that a parallel reduction of it has a deterministic result.

F{\sc able} \cite{swamy:fable} is a dependently typed extension of System-F that associates type level security labels with the data or actions they protect. These labels can be used to statically enforce security policies such as: search queries read from a network socket must be checked for malicious instructions before being passed onto a backend database. Although these labels could express the $Mutable$ and $Const$ constraints of our own system, they are treated more like data constructors than type class constraints. F{\sc able} contains a syntactically separated policy language that is used to explicitly add, remove and test for the labels attached to some object. However, their use of dependent types means that type checking is undecidable without the use of an auxiliary termination checker, whereas our language is less general but straightforward to check.

With respect to mutability polymorphism the stated goal of the BitC \cite{shapiro:bitc-language-specification} language is to permit any location, whether on the stack, heap or within data structures to be mutated. Its operational semantics includes an explicit stack as well as a heap, and function arguments are implicitly copied onto the stack during application. BitC includes mutability annotations, but does not use region or effect typing.  Finally, \cite{gupta:functional-encapsulation} presents an extension to the parallel language Id, which allows objects to be destructively initialised and then treated as constant from then on. As in our own system, Gupta uses region variables to track the mutability of objects. Instead of using region constraints, region variables are only attached to the types of mutable objects, leaving the types of constant objects annotated with the null region $\epsilon$.




