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.

I’m a postdoctoral researcher in the Functional Programming Lab at the University of Nottingham, working on ways to reason about the efficiency of programs in call-by-need (a.k.a. lazy) programming languages. I’m particularly interested in ways to unify the two concerns of correctness and efficiency.