
% -----------------------------------------------------------------------------
\section{Overloading and Deep Mutability}
In addition to our @updateInt@ function from the previous section, suppose we wanted a function @updateListInt@ that read every element from a source list and used this to update elements in a destination. Eliding the closure information for now, here is one possible definition for @updateListInt@:

\begin{small}
\begin{code}
updateListInt 
 :: forall %r1 %r2 %r3 %r4 !e1 $c1. Mutable %r2
 => List %r1 (Int %r2) -> List %r3 (Int %r4) -(!e1 $c1)> ()
 :- !e1 :> !Read %r1 + !Write %r2 + !Read %r3 + !Read %r4
 ,  $c1 :> $Clo (List %r1 (Int %r2))

updateListInt [] _   = ()
updateListInt _  []  = ()
updateListInt (x : xs) (y : ys)
 = do  updateInt x y
       updateListInt xs ys
\end{code}
\end{small}

In the definition of @updateListInt@ our @do@ expression does not perform monadic desugaring as per Haskell, it simply executes the statements in its body one after the other. In the type signature, the fact that this function writes to the list elements is revealed in both the @!Write %r2@ effect and the @Mutable %r2@ constraint. Also, the body of the function refers to the outermost parameter (the first list), which introduces the closure term @$Clo (List %r1 (Int %r2)@.


% -----------------------------------------------------------------------------
\subsection{The Update Class}
Having both @updateInt@ and @updateListInt@ is all well and good, but as they perform a similar function we'd prefer abstract them into a more general operation. We'll use Haskell style type classes to define the class of types that can be updated. We use  @(:=)@ as the polymorphic update operator. The remaining decision is what to use for the type of @(:=)@. We'll start with the obvious, that @(:=)@ takes two values of the same type and produces @()@. This will turn out to be wrong, and we'll discuss why in a moment, but we'll press on for now.

\begin{code}
  class Update a where                (incomplete)
    (:=) :: forall a. a -> a -> ()
\end{code}
So far, this type contains just the \emph{shape} information, that is the structure of its value portion. We still need to attach mutability constraints, effects and closures. As the function writes to its first argument, we must add a constraint like @Mutable a@. However, @Mutable@ only works on single region variables, meaning its parameter must have kind @%@, and not @*@ as in this case. Instead, we use the constraint @DeepMutable@ which works on types of kind @*@, and indicates that every region variable in the given type must be mutable. Like @Mutable@, our @DeepMutable@ constraint is baked in to the language. Each data type definition in the source program automatically derives the appropriate instances that relate @Mutable@ and @DeepMutable@. For example, we have:

\begin{code}
  instance Mutable %r1 
        => DeepMutable (Int %r1)
	
  instance (Mutable %r1, DeepMutable a) 
        => DeepMutable (List %r1 a)
  ...
\end{code}
For effect types, we have the related constructors @!DeepRead@ and @!DeepWrite@ that indicate a read or write to every region in a type. These effects are reduced to a simpler form during type inference, for example @!DeepRead (List %r1 (Int %r2))@ is reduced to @!Read %r1 + !Read %r2@. However, if a data type contains functions then we do not need to produce effects for type variables that only appear attached to those functions. This is related to the concept of \emph{materiality} mentioned in \REF and is discussed further in \REF.

With our new constraints and effects, we can fill in more of the type of our polymorphic update operation:

\begin{code}
  class Update a where                (incomplete)
    (:=) :: forall a !e1 $c1. DeepMutable a
         => a -> a -(!e1 $c1)> ()
         :- !e1 :> !DeepRead a + !DeepWrite a
         ,  !c1 :> $Clo a
\end{code}

This is almost what we want, but is really too restrictive compared with the types of @updateInt@ and @updateListInt@.
Firstly, when we instantiate the type of @(:=)@ for @List %r1 (Int %r2)@, the resulting constraint @DeepMutable (List %r1 (Int %r2))@ will reduced to the components @Mutable %r1@ and @Mutable %r2@. However, our original type for @updateListInt@ reveals that only the \emph{elements} of the list were being updated (in @%r2@) and not the spine as well. We feel we must accept this behavior. The type of a method function is an upper bound of all possible instances, so without some way to represent ``spine'' vs ``elements'' at the type level we just define @(:=)@ as an operator that can potentially write to any component of its first argument.

A more serious problem is that the type of @(:=)@ indicates that both arguments are written to, whereas in practice an instance of this method should only ever write to the first one. Related to this is that the @DeepMutable@ constraint requires both arguments to be mutable, which prevents us from using the value of, say, a constant integer to overwrite the value of a mutable one. Our solution to this problem is to weaken the relationship between the types of the two arguments, using the @Shape@ constraint which we will discuss in the next section.


