
% -----------------------------------------------------------------------------
\section{Regions and Mutability Polymorphism}

Here is the standard list type, as defined in Haskell or O'Caml (we use Haskell synax).

\begin{code}
  data List a = Nil | Cons a (List a)
\end{code}

In Haskell and O'Caml, is not possible to destructively insert a new element into a list of this type. However, as any working programmer knows, sometimes for performance reasons lists (or their simulacrums) simply must be updated.

\pagebreak{}
Unfortunately, in most functional languages this requires that we define \emph{a whole new type of lists}. Here is one version in Haskell:

\begin{code}
  data MutableList a 
         = MNil 
         | MCons a (IORef (MutableList a))	
\end{code}

Defining a new data type to achieve destructive update is not a huge burden in itself, but the fact that we must also redefine standard functions such as @map@, @fold@ and @filter@ surely is. Worse is that the code for these new functions will be almost identical to their ``pure'' counterparts, with the possible inclusion of calls to @readIORef@, and the use of the @IO@ monad in the Haskell case. This highlights a lack of expressiveness in these languages, namely the lack of \emph{mutability polymorphism}. All data should have the capacity to be destructively updated, and the programmer should not need to write multiple nigh-identical versions of the same function when using it.

Of course there are good reasons for using constant data structures, ranging from the use of lazy evaluation to the ability to perform compile-time optimisations. What we want is \emph{polymorphism}, meaning that we can support both pure/constant and effectful/mutable styles of programming safely and coherently in the same language. 


% -----------------------------------------------------------------------------
\subsection{Region Variables}
To introduce mutability polymorphism, we need a place to attach information about whether an object is constant or mutable. We also desire that the types of constant and mutable objects with the same structure have the same \emph{shape}. For this reason we add an extra parameter to our data types, a region parameter, which represents the abstract region of the store where a value of this type may possibly lie. Here is the definition of our list in Disciple:
\begin{code}
    data List %r a  = Nil | Cons a (List %r a) 
\end{code}

The @%r@ is the region variable, with the @%@ being a namespace qualifier which keeps the space of region names distinct from others. We use this symbol @%@ because it is two circles separated by a line, a mneumonic for ``this or that''. Now, although @%r@ is a variable, in the source language there are no associated constructors, so region variables can only be instantiated by other region variables. We do not use regions for allocation as in Tofte and Talpin's MLKit \cite{tofte:mlkit-4.3.0}. Rather, we use region variables as a place to attach constraints, and to track aliasing relationships between values after Lucassen and Gifford's original work on effect typing \cite{lucassen:polymorphic-effect-systems}. 

Finally, note that we overload the @%@ symbol to refer to the kind of region types, as well as the namespace of region variables. For example, the type constructor @List@ takes a region variable, a value type, and produces a value type. It's kind is therefore @List :: % -> * -> *@.


% -----------------------------------------------------------------------------
\subsection{Constancy and Mutability}
Now that we have region variables, mutability polymorphism is introduced by constraining them to be either @Mutable@ or @Const@ as desired. For example, if we wanted to define a destructively updatable list of @Int@s then we could write:
\begin{code}
 members :: Mutable %r1 => List %r1 (Int %r2)
 members = [1, 2, 3]
\end{code}

The fact that the structure of the list is mutable gives us the ability to destructively insert new elements into the middle of it. We would write the insert function using a primitive update operator such as:
\begin{code}
 updateTail :: forall %r a. Mutable %r 
            => List %r a -> List %r a -> ()
\end{code}

Before we proceed, there are two things to note about about @updateTail@. Firstly, in our full Disciple language we have nicer syntax for this, so you don't actually have to write @updateTail@, but see \CITE for details. Secondly, in section \REF we will add effect and closure information as well, so this type is not the full story.

Returning to the type for @members@, note that @%r1@ refers to the \emph{spine} of the list, whereas the other region variable @%r2@ refers to the list elements, integers in this case. If we wanted to update the physical integer objects then we would use a different function, @updateInt@ that operates on the list elements directly. We would also require @%r2@ to be mutable. The @updateInt@ function has the following type:
\begin{code}
  updateInt :: forall %r1 %r2. Mutable %r1
            => Int %r1 -> Int %r2 -> ()
\end{code} 
This function reads its second parameter and uses its value to overwrite the value of the first. Note that the two parameters of @updateInt@ have different region variables. We don't require @%r2@ to be @Mutable@ as well, because it's not the one being updated.

Importantly, in the types for @updateInt@ and @updateTail@ not that we have quantified the region variables with a @forall@. This is because these functions accept data from \emph{any} region and can allocate their result into \emph{any} region. On the other hand, the two region variables in the type for @members@ are \emph{not} quantified. This is because the data for @members@ exists in some fixed place in the store, and not in ``any'' region. Because of this we say the region variables in the type of @members@ are \emph{material}, which we discuss further in \REF. During type inference our compiler examines the materiality of types and generalises them appropriately.

Instead of mutable lists, if we wanted a constant list, who's spine could not be updated, then we would constrain its region variable to be @Const@ as follows:
\begin{code}
 constMembers :: Const %r1 => List %r1 (Int %r2)
\end{code}

As @updateTail@ requires the spine of a list to support mutability, but there is no @Mutable@ context on @constMembers@, it cannot be updated. However suppose we wrote the following:
\begin{code}
 suspectMembers :: Const %r1 => Mutable %r1
                => List %r1 (Inst %r2)
\end{code}

This type is clearly suspect, and questionably valid. Constraining a region variable to be both @Const@ and @Mutable@ is like constraining a type variable to be both @Integral@ and @Fractional@ in Haskell. Although it would be safe from a theoretical point of view, it ensures that a ``value'' of this type cannot be used, as there is no type that is an instance of both @Integral@ and @Fractional@. Our type inferencer currently treats conflicting region constraints as an error, though we could perhaps reduce it to a warning. It the type system of our core language which prevents types constrained as both @Const@ and @Mutable@ from being used, but see \CITE for details.

Finally, note that in full Disciple the programmer can write data types and type signatures \emph{sans} region variables, and our compiler fills them in with some simple defaulting rules. Material values defined at top level also default to being constant. For example, if we wrote:
\begin{code}
  haskellishList :: List Int
\end{code}
The above signature would be \emph{elaborated} to:
\begin{code}
  haskellishList :: Const %r1 => Const %r2 
                 => List %r1 (Int %r2)
\end{code}

This means that many Haskell programs are also Disciple programs, as you only need to mention regions and mutability constraints when you are actually using them. The same goes for the effect and closure information which we will discuss the next section.
