Olaf's Research Project Proposals

Static Contracts for Communicating Erlang Processes

Erlang is a concurrent functional programming language designed by Ericsson with dynamic process creation and asynchronous message passing. Type systems have been defined on top of the dynamically typed Erlang language, but these concentrate on the traditional, non-concurrent aspects of the language. The aim of the project is first to define a language for expressing properties (i.e. contracts) of process creation and communication, for example communication protocols. These contracts shall prevent many concurrency-related runtime errors but still allow common Erlang programming patterns. The second challenge is to devise algorithms for statically checking these contracts. The project will build on a wide area of previous research on type systems, dynamic and static contracts for functional languages and session types.

Tracing Functional Programs with Hat

Hat is a sophisticated tool for locating faults in Haskell programs. Hat consists of a trace generation system plus various tools for viewing a trace. The aim of the research project is to improve Hat by both extending it and easing its application in practise: (1) Integrate the trace generator of Hat into the byte code interpreter of the Glasgow Haskell system (GHC). (2) Enable traced code to call and be called from unmodified non-tracing code, such that Hat can use pre-compiled libraries of GHC. (3) Apply several theoretical results of a recent EPSRC project on tracing in Hat (e.g. algorithmic debugging with functions as finite maps). (4) Develop and implement new ways of displaying computations of common programming patterns, for example for the IO monad and monads in general.

Understanding Type Errors

The type systems of functional languages such as Haskell, ML and Clean have the advantages that they are flexible by allowing polymorphism, are unobtrusive by not requiring type annotations, and are very expressive. Practical experience shows that the type checker catches many errors, from trivial oversights to sometimes even deep logical errors. Well-typed programs seldomly go wrong at runtime.

However, experience also shows that from a type error message it is often hard to deduce the actual cause of the error and understand it. Novice programmers are often baffled by the type error messages. Even experienced programmers can take ages to locate the cause of some nasty type errors. This problem exists mainly because type errors are often raised far from the part of the program that causes them. The error messages give little additional information for tracking the cause.

Many proposals for improving the situation have been made, but few of them made it into practice. This is mainly because implementing many proposals would require a substantial amount of work which seems to be greater than their potential benefit. Hence the aim of this project would be to analyse existing proposals, relate them (many use different methods but provide similar results) and design and implement a simplified system that can be incorporated into an existing Haskell compiler.