Haskell Types with Numeric Constraints

We are grateful to Microsoft Research for their sponsorship of this project, which includes an internship, and with it the chance to make a real difference to world of principled but practical programming.

The project investigates the practical and theoretical impact of extending Haskell's type system with numeric expressions (representing sizes, or ranges, or costs, for example) and constraints capturing richer safety properties than are currently managed by static typing. It has three strands: (1) to investigate type inference with numeric constraints, (2) to investigate new programming structures, patterns, and techniques which exploit numeric indexing, and (3) to study the performance benefits derivable from richer guarantees. A bright student could bring significant benefits to developers using Haskell, a language with increasing industrial traction — not least at Microsoft. Work on the Glasgow Haskell Compiler, at Strathclyde!

Reusability and Dependent Types

A new EPSRC-funded project on Reusability and Dependent Types has just started, as a collaboration between Nottingham (Thorsten Altenkirch), Oxford (Jeremy Gibbons), and Strathclyde (Neil Ghani and Conor McBride).

We are all familiar with Milner’s slogan that “well-typed programs cannot go wrong”. Types express properties of programs; more expressive type systems—such as dependent typing—can state properties more precisely, providing stronger guarantees of behaviour and additional guidance in development. However, this expressivity comes at a price: more specific typing can reduce opportunities for code reuse. The goal of this project is to investigate techniques for promoting reuse without sacrificing precision; in particular, how can we layer dependently typed programs, imposing stronger invariants onto more general library code?

Further Particulars

Conor McBride will be the primary supervisor for both of these projects. Funding covers stipend, and fees for home/EU students, but the position is open to all. For further information, please contact Conor (conor ? cis ? strath ? ac ? uk).