%!TEX root = ../Main.tex
\clearpage{}
\section{Related}
\subsection{Disciple Core v0.3}
The Disciple Core v0.3 intermediate language is a version of System-F with region and effect typing, used in the DDC research compiler. Values such as arrays can be mutable or immutable, and the choice is tracked as a constraint at the type level. For example, we write @(Mutable r => Array r Int)@ for the type of a mutable array of integers and @(Const r => Array r Int)@ for the type of a constant (immutable) array of integers. The 'r' is a region variable, and @(Mutable r => ...)@ and @(Const r => ...)@ are type class constraints on that region variable. Now, although the use of type class constraints allows us to write code that is polymorphic over mutability, there is no safe way to destructively initialize a mutable array and then treat it as immutable from then on. 

Although the use of mutability constraints makes it easy to abstract over the mutability of some data type, the evidence-based encoding of type class constraints makes them impossible to revoke. In the operational semantics, to satisfy a constraint like @(Mutable r => ...)@ we pass a ``proof witness'' of type @(Mutable r)@. However, a ``proof witness'' is typically understood to be to true forever -- not just true while we initialize our array, then false afterwards. Without some notion of linearity, once we've passed a proof witness to a function, we can't be sure to get it back.


\subsection{ST Monads}
We could implement a primitive such as:

\begin{code}
 runSTArray 
  :: (forall s. ST s (STArray s a)) -> Array a
\end{code}

However, @runSTArray@ only works for computations that return a single array at a time. If our @ST@ computation needs to return, say, three arrays at once then we need a @runSTArray3@ function as well. This approach also does not scale to more complex data types -- suppose we wanted to destructively initialize two mutable graphs and three arrays in the same @ST@ computation.
