Title: Witnessing Purity, Constancy and Mutability

Ben Lippmeier, ANU

Abstract:

Restricting destructive update to values of a distinguished reference
type prevents functions from being polymorphic in the mutability 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. I'll present a System-F
style core language that uses type class constraints and dependently
kinded proof witnesses to encode information about the mutability of
values, and the purity of computations. We support mixed strict and
lazy evaluation, and use our type system to ensure that only
computations without visible side effects are suspended.