Deriving monad transformers
Ralf Thomas Walter Hinze · 1999
In a paper about pretty printing J. Hughes introduced two fundamental techniques for deriving programs from their specification, where a specification consists of a signature and properties that the operations of the signature are required to satisfy. Very briefly, the first technique, the term implementation, represents the operations by terms and works by defining a mapping from operations to observations --- this mapping can be seen as defining a simple interpreter. The second, the context-passing implementation, represents operations as functions from their calling context to observations. We apply both techniques to derive among others a backtracking monad transformer which adds backtracking to an arbitrary monad. In addition to the usual backtracking operations --- failure and nondeterministic choice --- the prolog cut and an operation for delimiting the effect of a cut are supported. 1 Introduction Why should one derive a program from its specification? Ideally, a derivation ex...