Jennifer L. P. Hackett

My Research

I'm a postdoctoral researcher in the Functional Programming Lab working on the Mind the Gap project funded by the EPSRC. This project aims to develop abstract ways of reasoning about program efficiency that are compatible with the current state-of-the-art techniques used to reason about correctness. Currently most program optimisations are justified using empirical techniques such as benchmarks; this project hopes to put the science of program efficiency on a more formal footing.

Recently, I have been looking into metric spaces as models for programming languages, and how this can be used to reason about efficiency.

I have a particular interest in evaluation strategies. My programming language of choice, Haskell, notably uses a "lazy" evaluation strategy which can make it difficult to reason about operational aspects of programs. It's my hope that by developing theories for reasoning about program efficiency, I can help to diminish this drawback and further encourage the adoption of lazy evaluation strategies. I am also interested in linear and affine lambda calculi for what they can tell us about lazy evaluation strategies.

Papers

Call-By-Need is Clairvoyant Call-By-Value
Jennifer Hackett, Graham Hutton
International Conference on Functional Programming, 2019
Erratum available
Call-by-need evaluation, also known as lazy evaluation, provides two key benefits: compositional programming and infinite data. The standard semantics for laziness is Launchbury's natural semantics, which uses a heap to memoise the results of delayed evaluations. However, the stateful nature of this heap greatly complicates reasoning about the operational behaviour of lazy programs. In this article, we propose an alternative semantics for laziness, clairvoyant evaluation, that replaces the state effect with nondeterminism, and prove this semantics equivalent in a strong sense to the standard semantics. We show how this new semantics greatly simplifies operational reasoning, admitting much simpler proofs of a number of results from the literature, and how it leads to the first denotational cost semantics for lazy evaluation.

Compositional Computational Constructive Critique
Or, How My Computer Learned to Appreciate Poetry
ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design, 2018
A well-typed work of art should not sound wrong:
we can use DSLs to get this boon.
Existing work has cover'd this for song,
at least so far as harmony and tune.
Well, verse contrains the author's pencil thus:
In English verse, the syllables adhere
to certain contours. Catenation plus
the empty form create a monoid here.
But not all poems stay within their meter;
some, like this, can be a little free
and so our monoid has to let us teeter
on the edge, as tunes oft do with key.
Our monoid must be fuzzy at its heart
to let us teach computers of this art.

Parametric Polymorphism and Operational Improvement
Jennifer Hackett, Graham Hutton
Proceedings of the ACM on Programming Languages, Volume 2, Issue ICFP, Article 68, September 2018.
Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as yet no comparable technique for reasoning about program improvement, that is, when one program uses fewer resources than another. Existing theories of parametricity cannot be used to address this problem as they are agnostic with regard to resource usage. This article addresses this problem by presenting a new operational theory of parametricity that is sensitive to time costs, which can be used to reason about time improvement properties. We demonstrate the applicability of our theory by showing how it can be used to prove that a number of well-known program fusion techniques are time improvements, including fixed point fusion, map fusion and short cut fusion.

Programs for Cheap!
Jennifer Hackett, Graham Hutton
Annual ACM/IEEE Symposium on Logic in Computer Science, 2015
Write down the definition of a recursion operator on a piece of paper. Tell me its type, but be careful not to let me see the operator's definition. I will tell you an optimization theorem that the operator satisfies. As an added bonus, I will also give you a proof of correctness for the optimisation, along with a formal guarantee about its effect on performance. The purpose of this paper is to explain these tricks.

Worker/Wrapper/Makes it/Faster
Jennifer Hackett, Graham Hutton
International Conference on Functional Programming, 2014
Much research in program optimisation has focused on formal approaches to correctness: proving that the meaning of programs is preserved. Paradoxically, there has been little work on formal approaches to efficiency: proving that the performance of optimised programs is actually improved. This paper addresses this problem for a general-purpose optimization technique, the worker/wrapper transformation. In particular, we use improvement theory to establish conditions under which the worker/wrapper transformation is formally guaranteed to improve the time performance of programs. These conditions are a natural refinement of those that guarantee the correctness of the transformation, and the resulting theory is simple to understand and apply.

The Underperforming Unfold: A New Approach to Optimising Recursive Programs
Jennifer Hackett, Graham Hutton, Mauro Jaskelioff
Symposium on Implementation and Application of Functional Languages, 2013
This paper presents a new approach to optimising corecursive programs by factorisation. In particular, we focus on programs written using the corecursion operator unfold. We use and expand upon the proof techniques of guarded coinduction and unfold fusion, capturing a pattern of generalising coinductive hypotheses by means of abstraction and representation functions. The pattern we observe is simple, has not been observed before, and is widely applicable. We develop a general program factorisation theorem from this pattern, demonstrating its utility with a range of practical examples.

Bio

I was born and grew up in Southampton, Hampshire, but went to Oxford to do my undergraduate degree in Computer Science. I achieved top first for my first three years and a first class degree overall, a fact of which I am eternally embarrassed. After completing my undergraduate degree, I went to the University of Nottingham to do a PhD under the supervision of Graham Hutton, and am now a postdoctoral researcher in the same group.

Outside of the world of computer science I have been involved in various forms of activism. I am involved in the charity organisation Action for Trans Health as well as other forms of LGBTQ+ campaigning. In particular, I was involved in a blockade of the Greater Manchester Police delegation to Manchester Pride 2016. I am also an active member of the Industrial Workers of the World.

I am into music, with my tastes ranging widely from anarcho-pop band Chumbawamba through 20th century classical composers such as Béla Bartók and avant-rockers Thinking Plague all the way to jazz-musician-cum-rapper Soweto Kinch. I also play with guitars and synthesizers and have mysterious and subtle links to a breakdancer named Ereshkigal.

I write fiction online at Thunder and Herbs.

Contact

School of Computer Science and Information Technology Home Page

The University of Nottingham Home Page