
% -- Intro --------------------------------------------------------------------
\section{Introduction}
\label{Introduction}

Suppose we are writing a library that provides a useful data structure such as linked lists. A Haskell-style definition for the list type would be:
\code{
	\kdata~ List~ a~ =~ Nil~ |~ Cons~ (List~ a)
}
The core language of compilers such as GHC is based around System-F \cite{sulzmann:system-Fc}. Here is the translation of the standard $map$ function to this representation, complete with type abstractions and applications:
\code{
	map	&::	& \mc{3}{\forall a~b.~(a \to b) \to List~a \to List~b} \\
	map	&=	& \mc{3}{\Lambda a.~\Lambda b.~ \lambda (f : a \to b).~\lambda (list : List~a).} \\
		&	& \mc{3}{\kcase~list~\kof} \\
		&	&	& Nil 		& \to~Nil~b \\
		& 	&	& Cons~x~xs 	& \to~Cons~b~(f~x)~(map~a~b~f~xs) \\
}

Say we went on to define some other useful list functions, and then decided that we need one to destructively insert a new element into the middle of a list. In Haskell, side effects are carefully controlled and we would need to introduce a monad such as $ST$ or $IO$ \cite{launchbury:lazy-functional-state-threads} to encapsulate the effects due to the update. Destructive update is also limited to distinguished types such as $\iSTRef$ and $\iIORef$.  We cannot use our previous list type, so will instead change it to use an $\iIORef$.
\code{
	\kdata~ List~ a~ = Nil~ |~ Cons~ (IORef~ (List~ a))
}
Unfortunately, changing the structure of our original data type means that we can no longer use the previous definition of $\imap$, or any other list functions defined earlier. We must go back and refactor each of these definitions to use the new type. We must insert calls to $\ireadIORef$ and use monadic sequencing combinators instead of vanilla $\klet$ and $\kwhere$-expressions. However, doing so introduces explicit data dependencies into the program. This in turn reduces the compiler's ability to perform optimisations such as deforestation and the full laziness transform \cite{santos:compilation}, which require functions to be written in the ``pure'', non-monadic style. It appears that we need \emph{two} versions of our list type and its associated functions, an immutable version that can be optimised, and a mutable one that can be updated. 

Variations of this problem are also present in ML and O'Caml. In ML, mutability is restricted to $\iref$ and $\iarray$ types \cite{macqueen:sml}. In O'Caml, record types can have mutable fields, but variant types cannot \cite{leroy:ocaml-3.11}. Similarly to Haskell, in these languages we are forced to insert explicit reference types into the definitions of mutable data structures, which makes them incompatible with the standard immutable ones. 

Value, effect, and mutability are three separate concepts, yet in both Haskell and O'Caml they are conflated. While we agree that expressing information about effects and mutability in types is good and useful for all the standard reasons, as this information is essentially orthogonal we argue that it should also appear that way in the types. We developing a new language, Disciple, that takes this idea as its central principle. 

\subsection{Disciple vs DDC Core}

Although Disciple is a source language intended for direct use by the programmer, in this paper we focus instead on the \emph{core intermediate language} for our compiler: the \emph{Disciplined Disciple Compiler (DDC)}. We refer to this language as DDC Core. The source and core languages are strongly related, the latter being essentially a desugared version of the first, with the addition of System-F style type abstractions and applications. We also use the same type structure for both, so when discussing our core language we are also implicitly discussing the source. Although Disciple supports full Haskell-style type inference up to the usual ambiguities with type classes (such as with the read/show problem), this aspect of our system is at an earlier stage of development. Although we will mention type inference in passing, reader is advised to see \cite{lippmeier:impure-world} for further information.  

DDC Core is modelled after the core language used in GHC, albeit with the addition of region and effect typing, and support for mutability polymorphism. GHC Core is currently based on System-Fc, which extends System-F with support for non-syntactic type equality. This feature is used to support advanced type system features such as Associated Types \TODO{ref} and GADTs \TODO{ref}. In contrast, we are working from a similar base, but in a different direction. The application areas we have in our sites are primarily concerned with systems programming, where both runtime performance and space usage make a difference, and working with mutable data structures is commonplace.

As DDC Core is part of a larger compiler, this paper is as much about compiler development as it is about types. DDC Core has several features specifically geared towards making the compiler easier to write and debug, which would appear superfluous if this work was just an exercise in meta-theory. We will discuss these features along the way. 

\pagebreak{}
In summary, we make the following contributions:

\begin{itemize}
\item	We present a System-F style core language that uses region variables and region class constraints to encode mutability polymorphism. This allows arbitrary data to be mutable without changing the structure of their value types. \medskip

\item	We use call-by-value evaluation as default, but support lazy evaluation via a primitive $\isuspend$ operator. We use purity constraints on effect variables to represent the fact that only pure function applications should be suspended.\medskip

\item	We use dependently kinded witnesses to encode information about mutability and purity in the core language, and show how they can be used to reason about the correctness of program optimisations in the presence of destructive update.\medskip

\item	As a natural extension to the above system, we discuss witnesses of no-aliasing (distinctness), and show how they can be used to improve the scope of the previous optimisations.
\end{itemize}

As the name may suggest, Disciple draws inspiration from much existing work, including the Type and Effect Discipline of \cite{talpin:type-and-effect-discipline},~ The Capability Calculus \cite{crary:capabilities} and System-Fc \cite{sulzmann:system-Fc}. We also build on ideas from 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. DDC can be obtained from \verb|http://disciple.ouroborus.net|.




