Haskell Equational Reasoning Assistant
The 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.
The Interactive Interface
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. 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 like rewrite strategies, from highly focused rewriting through to applying a generic rewrite everywhere applicable using a depth-first strategy.