Joachim Breitner's Homepage

I submitted a Functional Pearl to this year’s ICFP and it got accepted!

It is about the idea of using Haskell’s inherent ability to define recursive equations, and use them for more than just functions and lazy data structures. I blogged about this before (introducing the idea, behind the scenes, applications to program analysis, graph algorithms and minesweeper), but hopefully the paper brings out the idea even more clearly. The constructive feedback from a few friendly readers (Claudio, Sebastian, and also the anonymous reviewers) certainly improved the paper.

Abstract

Haskell’s laziness allows the programmer to solve some problems naturally and declaratively via recursive equations. Unfortunately, if the input is “too recursive”, these very elegant idioms can fall into the dreaded black hole, and the programmer has to resort to more pedestrian approaches.

It does not have to be that way: We built variants of common pure data structures (Booleans, sets) where recursive definitions are productive. Internally, the infamous unsafePerformIO is at work, but the user only sees a beautiful and pure API, and their pretty recursive idioms – magically – work again.

If you are curious, please have a look at the current version of the paper. Any feedback is welcome; even more if it comes before July 11, because then I can include it in the camera ready version.

There are still some open questions around this work. What bothers me maybe most is the lack of a denotational semantics that unifies the partial order underlying the Haskell fragment, and the partial order underlying the domain of the embedded equations.

The crux of the probem is maybe best captured by this question:

Imagine an untyped lambda calculus with constructors, lazy evaluation, and an operation rseq that recursively evaluates constructors, but terminates in the presence of cycles. So for example

rseq (let x    = 1 :: x    in x   ) ≡ ()
rseq (let x () = 1 :: x () in x ()) ≡ ⊥

In this language, knot tying is observable. What is the “nicest” denotational semantics.

Update: I made some progress via a discussion on the Haskell Discource and started some rough notes on a denotational semantics.