Haskell Equational Reasoning Assistant

(DRAFT; Work in Progress)

Functional programmers often appeal to equational reasoning to justify various decisions made in both design and implementation. This page introduces the Haskell Equational Reasoning Assistant (HERA), an architecture that provides both a GUI level and a batch level Haskell rewrite engine inside a single tool. The interactive interface is used to create and edit non-trivial translations that can be used to extend the batch level API; the batch level API can be used to implement powerful, context sensitive rewrites that can be provided to the interactive interface.

You can get the development version of HERA with the command: darcs get http://code.haskell.org/HERA

The Interactive Interface

Ajax applications use a web browser interface, and provide a dynamic interactive experience beyond traditional CGI scripts, with user interactions causing localized updates to the displayed web pages, rather than complete page reloads[2]. An Ajax engine implemented in Javascript turns user interactions into asynchronous HTTP requests, sending them to the Ajax-compliant web server. The engine then comprehends the responses to the asynchronous requests, and uses Javascript to redraw only the parts of the interface that need updating.

HERA is a classical Ajax application consisting of two components: a client-side Ajax engine running inside the browser customized for HERA; and a server-side Haskell application which provides the rewrite engine, and interacts with the Javascript Ajax engine via a simple web server, also written in Haskell.

There are three main panels in the interface:

The Code panel contains the pretty-printed selectable code fragment, and a list of individual rewrites that have recently been applied. The Ajax engine on the client side is configured to understand the nesting of Haskell expressions, allowing the user to select only valid candidate sub-expressions, using the algorithm described in a previous paper[4]. In the screenshot in Figure 1 above, the right hand side of a let expression has been selected; a case expression.

The Dictionary panel contains a comprehensive list of possible rewrites. When the user clicks on a rewrite name, the rewrite is applied to the currently selected sub-expression in the code window, or the whole code fragment, if no sub-expression is selected. The Ajax engine asks for a specific rewrite to be applied to a specific sub-expression, using a specific strategy. The server application honors the request, and the engine accepts the new rendition of the code panel after the rewrite has been applied.

The Oracle panel gives context sensitive suggestions of possible rewrites to apply. Any time the user selects a sub-expression, and before a possible rewrite has been chosen, the Ajax engine fires an asynchronous HTTP request to HERA server, explaining what selection is being considered. A Haskell thread inside the server is then tasked with attempting every reasonable candidate rewrite in the internal rewrite dictionary on the selected sub-expression, sending a list of matching rewrites back to Ajax engine to display in the Oracle panel.

In practice this background search takes a fraction of a second, and includes the rewrite the user actually wants to use almost every time. In our experience, only during the eureka steps of rewriting does the user actually need to hunt through the dictionary. In the screenshot in Figure 1, the Case of known constructor has been offered to the user as a possible candidate, and examination of the code reveals that the case selected is a case of known constructor candidate.

The interface also has a strategy pull down menu in the top bar, which allows the user to choose between a basic range of Stratego[1] like rewrite strategies, from highly focused rewriting through to applying a generic rewrite everywhere applicable using a depth-first strategy.

For more information, see the author's web page.