Witnessing Purity, Constancy and Mutability

Abstract. Restricting destructive update to values of a distinguished reference type prevents functions from being polymorphic in the muta-bility of their arguments. This restriction makes it easier to reason about program behaviour during transformation, but the lack of polymorphism reduces the expressiveness of the language. We present a System-F style core language that uses dependently kinded proof witnesses to encode information about the mutability of values and the purity of computa-tions. We support mixed strict and lazy evaluation, and use our type system to ensure that only computations without visible side effects are suspended.