Computer Laboratory

Part II Projects Suggestions

Handling Transparent Code Migration

(Based on Eijiro Sumii’s An Implementation of Transparent Migration on Standard Scheme.)

Mobile computation is an efficient and effective approach to distributed programming where a program works by migrating from one host to another. The migration is called transparent if the execution state of the program is preserved before and after the migration. Transparent migration is preferable to non-transparent, because it is easier to use for application programmers. At the same time, however, it is harder to implement for language developers: all existing implementations of transparent migration need either a custom runtime system or global source code transformation.

Concretely, we have a “go” statement that lets us switch to a different machine and continue execution there. For example:

for host in network
  go host

That is, each iteration is executed on a different machine.

This challenging project involves using effect handlers to serialise code so that it can migrate to another host. After implementing the code migration library, this project can include a use-case implementing distributed programs such as routing maintenance operations using the code migration library.

For a successful project, the student would have used Haskell and its class system, and obtain familiarity with monads and algebraic effects as used to structure typed functional programs.

Graphical and Polynomial Combinations of Algebraic Theories for Semantics

(Based on pages 34-38 of Hyland, Plotkin and Power’s Combining Effects: Sum and Tensor.)

Defining the meaning of programming languages using denotational semantics is particularly useful for optimising compiler design. When constructing denotational semantics for languages with computational effects (such as state, exceptions, I/O, and non-determinism) two algebraic operations emerge as useful: the sum of two theories and their tensor. These operators lead to a description of algebraic semantics as polynomials in theories. However, choosing the exact order in which to perform these two operations on the theories at hand is non-trivial. Arranging the data as a graph leads to a more intuitive description: each semantic theory corresponds to a vertex, and two vertices are connected iff the corresponding theories should commute. The graphical notation is strictly more expressive than the polynomial notation. Linear polynomials enable an extraction of the monadic semantics using monad transformers, which are already usable by functional programmers.

The goal of this challenging project is to provide tools for investigating algebraic semantics. In particular, studying and implementing Hyland et al.’s various algorithms:

  • deciding whether a given graph description has a corresponding polynomial description and extracting this polynomial; and
  • deciding whether a polynomial is linear and extracting the monad transformer stack corresponding to a linear polynomial.

For a successful project, the student would need to understand the algebraic properties of these polynomials, their connection with the graphical notation, and the various algorithms involved. The student would also need to implement graph algorithms and data structures for syntax.

(8 October 2013: Check this page later for additional project suggestions…)