%!TEX root = ../Main.tex
\section{Introduction}

Suppose we want to multiply all the elements in an array by two, in Haskell --- a reasonable request.

\begin{code}
timesTwo :: Array Int -> Array Int
timesTwo arr
 = unsafePerformIO
 \$ do   marr :: MArray Int <- M.new (I.length arr) 
        loop (I.length arr) 
             (\ix -> do val <- I.read arr ix 
                        M.write marr ix (val * 2))
        M.unsafeFreezeMArr marr
\end{code}
%
What a disaster. The standard Haskell @Array@ type is immutable and does not support constant time update. For a reasonable implementation we need to create a @new@ mutable array (of type @MArray@), initialize it destructively, and then freeze (coerce) it into an immutable array. In the above example we have used the @M.*@ qualifier for operations that work on the mutable version and @I.*@ for operations that work on the immutable one. Because the @M.write@ function performs a side effect it is in the IO monad, and hence we must write monadic code and then use @unsafePerformIO@ to embed it into pure core. We also need @unsafeFreezeMArr@ to coerce the mutable array into an immutable one. These unsafe functions have the following types:

\begin{code}
 unsafePerformIO  :: IO a -> a
 unsafeFreezeMArr :: MArray a -> IO (Array a)
\end{code}
%
In this context, @unsafe@ means that the use of such a function can break the invariants the compiler depends on when compiling code. For example, we could write a program using @unsafeFreezeMArr@ functions that behaves differently depending on whether it is compiled with or without optimizations enabled. The @timesTwo@ function does not have this problem, but we offer no proof of this --- you just have to believe it. In larger programs the lack of a well defined meaning becomes more problematic.

We can certainly \emph{hide} unsafe functions behind an external API, perhaps with a suitable @map@ function on the @Array@ type, as provided by the well known @Data.Vector@ library~\cite{Coutts:stream-fusion}. There is not a way to manage this problem cleanly at the semantics level, though there are ways to make it more pleasant to hide~\cite{Terei:safe-haskell}.

The use of the @ST@ monad is a non-solution. Although we can encapsulate the \emph{effect} of destructive initialization as an @ST@ computation, there is no general way to coerce mutable data structures into immutable ones. 

We make the following contributions:

\begin{itemize}
\item   We present a new compiler intermediate language named System-F$^{rc}$, which is 1) call by value by default; 2) supports lazy evaluation via annotations; 3) directly manages the mutability of data structures at the type level. Our language is based on the region and effect system we formalized in prior work \CITE{Mechanized}, extended with a capability system. 

\item   We provide indexed computation types (like monads) that allow computational effects to be reasoned about in a more fine grained way than Haskell's monolithic IO monad.

\item   We use a version of Filinski's monadic reification and reflection operators, which allow the language to be presented with a single @let@-binding form that works for both pure and effectful expressions, easing compiler development. 

\item   Our language and its semantics are fully mechanized in Coq,\footnote{here} and we have a prototype interpreter.\footnote{here}
\end{itemize}
%
System-F$^{rc}$ directly builds on Nanevski's work on coeffects~\cite{Nanevski:modal-effects,Nanevski:modal-possiblity}, and is inspired by the lax-truth modality described by Pfenning and Davies \cite{Pfenning:judgmental-reconstruction} and others \cite{Benton:computational-types}. We cover the difference between effects and coeffects in the next section.
