I’m a PhD student at the University of Birmingham, supervised by Paul Levy. I work on defined algebraic operations.
Many programs in CS are written by defining a domain-specific language (such as the state monad, or other monads) and writing an interpreter (such as runState). Abstract algebraic operations are a general framework for creating such a language:
- Start with a base functional language
- Add some algebraic operations, and
- Add some equations.
You can then easily give an interpreter by tree induction.
Defined algebraic operations are similar to handling, but operation definition (“handling”) binds operations to behaviour, ruling out “re-handling”. This unlocks many additional theorems which are false for handling, and in my opinion better reflects how people usually use handling.
Example. Our operation definition is spelled wherealg. Suppose that Dstate defines get and set operations suitably for global state. Then
(set 4; set 5) wherealg (get, set)=Dstate = (set 5) wherealg (get, set)=Dstate ,
just like with handling. But also for any term-with-hole M[—],
M[set 4; set 5] wherealg (get, set)=Dstate = M[set 5] wherealg (get, set)=Dstate .
(This is false in general for handling, because we don’t know if set will be handled by Dstate.)
Thus, (—) wherealg Dstate is truly a map from stateful programs to pure functions that respects the state equations. Or as I call it, an “interpreter”.
It is essential to set up the type system properly to get our desired reasoning principles. We found that the same principles apply for for-loops and this resulted in a paper: Iteration and labelled iteration with Paul. Summary: When you naively add iteration to lambda calculus, nested loops with control are very inconvenient in the resulting language. The inconvenience is rather like trying to program with De Bruijn indices. We give an alternative syntax using second-order labels.
» paper html / pdf
I am hoping to write up the results in a thesis soon.
I did my master’s thesis under Herman Geuvers in Eindhoven about a “continuation calculus” with a code=data feel, which yielded 2 papers: paper 1, paper 2.
Contact
You can reach me on myfirstname @ myfirstname . xyz