

% -------------------------------------------------------------------------------------------------
\section{Material Regions and Sharing}
As Disciple supports destructive update of arbitrary objects, the way in which objects are shared between computations matters more than in a purely functional language such as Haskell. Note that we use the word ``object'' to refer to physical objects in the store, and that two distinct objects can have the same ``value''. In Disciple it is possible to distinguish between functions that freshly allocate their returned objects, from functions that return a shared object from their environment. This is a simple matter of updating the returned object, calling the function again, and comparing the result. Because sharing is directly observable, we track it in our type system.

As mentioned in \REF, we track sharing with an extension of Leroy's \emph{closure typing} \CITE. Although closure typing was originally used to mitigate the potential unsoundness of the ML type system that arises with mutable references, its utility extends beyond this. As we have seen, closure typing models the sharing of data due to free variables in the bodies of functions. In \CITE this is used to determine the set of \emph{dangerous variables} in a type, which are the ones that cannot be generalised because they classify polymorphic objects reachable by shared mutable references.

As discussed in \CITE we also use closure typing to restrict the generalisation of dangerous variables. However, our support for mutability is greater than in ML, as we do not require all updates to be performed on objects of a distinguished reference type. In Disciple objects of \emph{all} types have the potential to be destructively updated, and we use region variables to support mutability polymorphism. These features require us to introduce the notion of \emph{materiality}, to help decide which type variables in a type actually correspond to shared data.


% -----------------------------------------------------------------------------
\subsection{Material, Strongly Material and Immaterial Variables}
As mentioned in \REF, we name the type variables associated with physical data \emph{material} variables. Type variables associated with data that we can ``get at'' directly are \emph{strongly material} and all others are \emph{immaterial}. For example, consider the following type:
\begin{code}
  five :: Int r1
  five = 5
\end{code}

Here, @r1@ is strongly material because @five@ is bound to a real data object in the store. We can happily read/copy this object, and write to it too provided we include the appropriate mutability constraint. In contrast, consider:
\begin{code}
  succ :: forall r2 r3
       .  Int r2 -(e1)> Int r3
       :- e1 :> Read r2
\end{code}

In this case @r2@ and @r3@ are immaterial, as they represent the locations of objects passed to, and returned from a function. There are no actual integer objects associated with @succ@, and the region variables in its type do not correspond to data that is shared between uses of this function. However, consider:
\begin{code}
  sameFive :: () -(c1)> Int r1
           :- c1 :> Clo (Int r1)
  sameFive () = five
\end{code}

Here, @sameFive@ is a function that returns the same object from its environment each time it is called. The closure constraint in its type reveals the sharing. In this case @r1@ is material, but not strongly material. This is because the only thing we can do with @sameFive@ is apply it, which yields the same `5' object each time. It is not possible to ``copy'' @sameFive@ in such a way that the copy yields a \emph{different} `5' object on further application.

The fact that we are unable to copy functions as described above is a limitation of our language implementation, but it is a standard one. In most implementations of functional languages, function objects are atomic. They can be applied to an argument, yielding a return value, but do not support any other operations such as copying, update, equality, ordering, pretty printing and so on. If we had an implementation that \emph{could} copy function closures then perhaps we would want to treat such closures as strongly material as well, but we have not considered this further.

% -----------------------------------------------------------------------------
\subsection{The variables that cannot be generalised}
Note that during type inference, material variables are \emph{not} generalised. In our @succ@ example from the previous section we have added @forall@ quantifiers to indicate that this function accepts its pararameter from any region, and can produce its result into any region. However, the @r1@ variable in the type of @five@ and @sameFive@ refers to a shared, statically allocated region. As discussed in \CITE the following classes of variables are not generalised: 

\begin{enumerate}
\item 	Variables free in the type environment. 
\item	Dangerous variables.
\item	Material variables.
\end{enumerate}

The first of these is standard from Hindley-Milner style type inference. As mentioned earlier, we use mutability constraints to indicate which types correspond to to mutable objects. This is different from \CITE where the types of mutable objects contain @ref@ constructors that indicate mutability. This implies that we compute the set of dangerous variables differently, though the principle remains the same. Computation of the dangerous and material variables in a type is discussed formally in \REF.


% -----------------------------------------------------------------------------
\subsection{Shape Constraints and Values Containing Functions}
In this section we discuss how materiality interacts with our @Shape@ constraint from \REF. Consider the following data type declaration, which has had its namespace qualifiers elided for space reasons. We write @r1..r4@ as a contraction of @r1 r2 r3 r4@.
\mcode{
	\mc{4}{\kdata~ \iIntFun~ r_{1..4}~ e_1~ c_1} \\[0.5ex]
	 & =  & SInt~ & (\iInt~ r_2) \\
	 & ~| & SFun~ & (\iInt~ r_3 \ttoa{e_1 c_1} \iInt~ r_4)
}

Using the class instantiation process from \REF, the type of a @copy@ instance function must be at least as polymorphic, and no more effectful, closureful or otherwise constrained than the following. We have written @Read r1..r4@ as a contraction of the four atomic effects. 
\mcode{
	\icopy[\iIntFun]
		& :: 	& \forall~ r_{1..8}~ e_{1..3}~ c_{1..2} \\
		& .  	& IntFun~ r_{1..4}~ e_1~ c_1 \ttoa{e_3} IntFun~ r_{5..8}~ e_2~ c_2 \\
		& \rhd 	& e_3 \tme Read~ r_{1..4} \\
}

Unfortunately, we have no way of writing a copy function that actually has this type. The trouble is with the function object embedded in the @SFun@ constructor. For example, we could try something like:
\mcode{
	\ibadCopy \ixx \\
	\quad = \kcase~ \ixx~ \kof \\
	\qq \qq \iSInt~ i  & \to~ \iSInt~ (\icopyInt~ i) \\
	\qq \qq \iSFun~ f  & \to~ \iSFun~ f \\
}

For the @SInt@ alternative we have just used @copyInt@ to copy the contained integer. However, as we have have no way of copying a function value, we have simply reused the variable @f@ on the right of the second alternative. Unfortunately, this gives our function the following type:
\mcode{
	badCopy & ::   & \forall   r_{1..6}~ e_1~ c_1 \\
   		& .    & \iIntFun~ r_{1..4}~ e_1~ c_1 \ttoa{e_1} IntFun~ r_{5..6}~ r_{3..4}~ e_1~ c_1 \\
   		& \rhd & e2 \tme \iRead~ r_{1..2}
}

Note that in the return type of this function, @r5@ and @r6@ are fresh but @r3@ and @r4@ are not. The effect and closure variables @e1@ and @c1@ also appear on both sides. The first two region parameters @IntFun@ correspond to actual objects in the store that can be copied, but the rest do not. For the @SFun@ alternative, the best we can do is to pass @f@ through as the return value, but doing so does not freshen all the variables in its type.

Our solution to this problem is to define the @Shape@ constraint such that only strongly material variables must be fresh. For @IntFun@ variables @r1@ and @r2@ are strongly material, and the rest are immaterial. The materiality of each variable in a data type declaration is computed during the desugaring stage of our compiler, and the appropriate @Shape@ instances are generated accordingly. For @IntFun@ this gives us:
\mcode{
	\kinstance \iShape 
		& \hspace{-0.5em} (\iIntFun~ r_1~ r_2~ r_3~ r_4~ e_1~ c_1~) \\
                & \hspace{-0.5em} (\iIntFun~ r_1~ r_2~ r_5~ r_6~ e_1~ c_1~)
}

Although there may be a use for a @Shape@ style constraint without this added restriction concerning materiality, we have not yet thought of one. As for why its need arises in our system: we feel it is a natural result of including value, region, effect and closure typing in the same framework. In many cases these types can be treated similarly, such as by using the same syntax for quantification, and keeping the constructors at the same syntactic level. However, values, regions, effects and closures, are really different sorts of things, and sometimes that shows. Conceptually, the @Shape@ constraint requires the physical structure of two objects to be identical, while requiring other information to vary. Strongly material region variables classify this physical structure, but immaterial variables do not. Weakly material variables also classify physical structure, but this is structure that we cannot access directly. As with immaterial variables, the @Shape@ constraint passes weakly material ones through unharmed.


% ------------------------------------------------------------------------------------------------
\subsection{Computing the sets of variables}
Dangerous variables were discussed in \REF. To compute the dangerous variables of a type we use a domain @D@ where a member of this domain can be either a pair consisting of a set of constraints and a type expression, or a dotted variable @a@$^\bullet$.
$$
      D = \{Constraint\} \times Type + DotVar
$$

To compute the dangerous variables in a particular type @t@, we start with the set $\emptyset$


\TODO{Describe operation of this, and operation of ctorTypes, args}


% -- Dangerous Variables --------------------------------------------------------------------------
\begin{figure}
\mcode{
		\idv : \setof{D} \to \setof{D}
\\[0.5ex]
		\idv(\mu) 
			& = \mu~ \cup~ \bigcup \setof{ \idv'(x) ~|~ x \in \mu }
\\[2ex]
		\idv' : D \to \{D\}
\\[0.5ex]
		\idv' ( a^\bullet )
			& = \setof{ a^\bullet }
\\[0.5ex]
		\idv' ( \apair{\Omega,~ a} )
			& = \emptyset
\\[0.5ex]
		\idv' ( \apair{\Omega,~ \varphi \rhd \Omega'} )
			& = \setof{ \apair{\Omega \cup \Omega',~ \varphi} }
\\[0.5ex]
		\idv' ( \apair{\Omega,~ \varphi \lor \varphi'} )
			& = \setof{
			 	\apair{\Omega,~ \varphi},~ 
				\apair{\Omega,~ \varphi'} }
\\[0.5ex]
		\idv' ( \apair{\Omega,~ \bot} )
			& = \emptyset
\\[0.5ex]
		\idv' (\apair{\Omega,~ \tau \longtoa{\sigma~ c} \tau'})
			& = \setof{ \apair{\Omega,~ \varphi} }~ \kwhere~ (c \tme \varphi) \in \Omega
\\[0.5ex]
		\idv' (\apair{\Omega,~ T_{\kappa}~ r~ \ov{\varphi}})  
\\[0.2ex]
		\quad |~ \iMutable~ r \in \Omega
			& \hspace{-1em} = \setof{ a^\bullet ~|~ a \in \ifv(\ov{\varphi}) }   \\
		\quad |~ \iotherwise
			& \hspace{-1em} = \setof{ \apair{\Omega, \tau[r~ \ov{\varphi} / \ov{a}]}
				~|~ \forall \ov{a}.~ \tau \in \iargs(\ictorTypes(T)) }
\\[0.5ex]
		\idv' (\apair{\Omega, \iClo~ \varphi})
			& = \setof{ \apair{\Omega, \varphi }}
\\[0.5ex]
		\idv' (\apair{\Omega, \varphi_1~ \varphi_2}
			& = \emptyset
}
\label{fig:DangrousVariables}
\caption{Dangerous Variables}
\end{figure}


% -- Material Variables ---------------------------------------------------------------------------
\begin{figure}
\mcode{
		\imv : \{ D \} \to \{D\}
\\[0.5ex]
		\imv(\mu) 
			& = \mu~ \cup~ \bigcup \setof{ \imv'(x) ~|~ x \in \mu }
\\[2ex]
		\imv' : D \to \{D\}
\\[0.8ex]
		\imv' ( a_\kappa^\bullet )
			& = \setof{ a_\kappa^\bullet }
\\[0.8ex]
		\imv' ( \apair{\Omega, \ a_\kappa} )
\\[0.2ex]
		\quad |~ \kappa \in \{ \%, \ * \}
			& = \{ a_\kappa^\bullet \} 
\\
		\quad |~ \iotherwise
			& = \emptyset
\\[0.8ex]
		\imv' (\apair{\Omega, \ T_{\kappa}~ r~ \ov{\varphi}})  \\
		\mc{2}	{\quad 
			   = 	\setof{ r^\bullet }
			   \cup	\setof{	\apair{\Omega, \tau[r~ \ov{\varphi} / \ov{a}]}  
					|~ \forall \ov{a}.~ \tau \in \iargs(\ictorTypes(T)) }
			}
\\[0.8ex]
		\imv' (\apair{\Omega, \iClo~ \varphi})
			& = \setof{ \apair{\Omega, \varphi }}
\\[0.8ex]		
		\mc{2}{\trm{... other cases as per $\idv'$}}
}
\label{fig:MaterialVariables}
\caption{Material Variables}
\end{figure}


% -- Immaterial Variables -------------------------------------------------------------------------
\begin{figure}
\mcode{
		\iiv : \setof{ D } \to \setof{ D }
\\[0.5ex]
		\iiv(\mu) 
			& = \mu ~\cup~ \bigcup \setof{ \iiv'(x) ~|~ x \in \mu }
\\[2ex]
		\iiv' : D \to \setof{ D }
\\[0.8ex]		
		\iiv' ( a_\kappa^\bullet )
			& = \setof{ a_\kappa^\bullet }
\\[0.8ex]
		\iiv' ( \apair{\Omega,~ a_\kappa} )
\\[0.2ex]
		\quad |~ \kappa \in \setof{ \%,~ * }
			& = \emptyset		
\\
		\quad |~ \iotherwise
			& = \setof{ a_\kappa^\bullet }
\\[0.8ex]
		\iiv' (\apair{\Omega,~ \tau \ttoa{e~ c} \tau'})
\\
		\mc{3}	{\quad
			  = \setof{ a^\bullet 
				~|~	a \in \ifv(\tau) 
					\cup  \ifv(\tau') 
					\cup  \ifv(\varphi) 
					\cup  \setof{ e,~ c }
				  }
			 \cup	\setof{ \apair{\Omega,~ \varphi'} }
			}
\\
		\mc{3}{\quad \kwhere\quad
				(e \tme \varphi)  \in \Omega,~ 
				(c \tme \varphi') \in \Omega}
\\[0.8ex]
		\iiv' (\apair{\Omega,~ T_{\kappa}~ r~ \ov{\varphi}})
			& = \setof{ \apair{\Omega, \tau[r~ \ov{\varphi} / \ov{a}]} \ 
					|~ \forall \ov{a}.~ \tau \in \iargs(\ictorTypes(T)) }
\\[0.8ex]
		\iiv' (\apair{\Omega, \iClo~ \varphi})
			& = \setof{ \apair{\Omega, \varphi }}
\\[0.8ex]
		\mc{2}{\trm{... other cases as per $\idv'$}}
}


\label{fig:ImmaterialVaraibles}
\caption{Immaterial Variables}
\end{figure}

