Prolog's Control Constructs in a Functional Setting — Axioms and Implementation

Abstract

The purpose of this article is twofold. First, we show that Prolog's control constructs can be smoothly integrated into a functional language like Haskell. The resulting `language', termed embedded Prolog, incorporates many of the features prescribed by the Prolog ISO standard: control constructs including the cut, all solution collecting functions, and error handling facilities. Embedded Prolog lacks some concepts such as logical variables but it inherits all of Haskell's strengths, eg static polymorphic typing, higher order functions etc. Technically, the integration is achieved using monads and monad transformers. One of the main innovations is the definition of a backtracking monad transformer, which allows us to combine backtracking with exception handling and interaction. Second, we work towards an axiomatization of the operations, through which the computational features are accessed. Equations are used to lay down the meaning of the various operations and their interrelations enabling the programmer to reason about programs in a simple calculational style. The axiomatization is applied to show that each finite computation has a simple canonical form.