Effect Parametricity in Dependently-Typed Languages (FWOTM978)

In imperative programming languages (e.g. Java), a function can cause side-effects such as displaying output on the screen or throwing an exception. A function in a purely functional programming language (e.g. Haskell) on the other hand, cannot perform side- effects unless this is explicitly mentioned in its output type. For instance, a function that takes an integer as argument and returns an integer or throws an exception, would have the type int -> Excep(int). Here Excep(int) is the type of computations that have an integer as result but which may cause a side-effect, viz. throwing an exception. Just as integers, these computations can be provided as arguments of another function or collected into a list. We can also construct other types (e.g. File(int)) to encode other kinds of effects (e.g. reading from a file). Effect polymorphic functions are functions that can work with any computation, irrespective of the kind of effect it may cause. Haskell for example provides a function 'sequence' taking a list of computations and performing them sequentially. Effect parametricity is a mechanism to reason and derive properties about effect polymorphic functions. Dependently-typed programming languages have a very powerful type system, allowing a programmer to simultaneously write programs and prove properties of these programs in the same language. The idea of this project is to use recently developed support for parametricity in these languages to study effect parametricity.

Keywords:Programming languages, formal verification, side-effects

Disciplines:Language design, constructs and features, Language processors, Programming languages and technologies