
\section{Conclusions and Future Work}
\label{conclusion}
We have presented a System-F style intermediate language that supports mutability polymorphism as well as lazy evaluation. We have used dependently kinded witnesses to track the mutability, constancy and aliasing of regions, and the purity of effects. One of the current limitations of our system is that the results of all case alternatives must have the same type. This prevents us from choosing between, say, a mutable and a constant integer. In future work we plan to provide a new region constraint that represents the fact that an object could be in either a mutable or constant region. We would permit such objects to be read, but not updated, and computations that read them could not be suspended. Doing so would likely require introducing a notion of subtyping into the system, so the types of all alternatives could be coerced to a single upper bound. 

Another current limitation is that we have no way to destructively initialise an object, and then treat it as constant from that point onward. For example, in the $\ilength$ function from \S\ref{Witnesses-of-Constancy-and-Mutability} we copied the final counter value before returning it because we did not want a $\iMutable$ constraint in the overall type of $\ilength$. We are currently working on a system to provide a local witness of mutability to an expression that performs such initialisation. We must then ensure that this witness, and hence the capability to perform further updates, cannot be exported out of the context that performs the initialisation. 


\textbf{Acknowledgements}
Many thanks to Clem Baker-Finch and Simon Winwood for discussions on witnesses and aliasing. Thanks also to Erik de Castro Lopo, Ben Sinclair and others for test cases and patches to DDC. This work was supported in part by the School of Computer Science, Australian National University, and funded in part by the Australian Research Council under grant number LP0989507.
