Purely Functional Lazy Non-deterministic Programming
📜 Abstract
Functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (non-strict evaluation with sharing of the results) with non-determinism. Yet these benefits are seldom enjoyed in functional programming, because the existing features for non-strictness, sharing, and non-determinism in functional languages are tricky to combine. We present a practical way to write purely functional lazy non-deterministic programs that are efficient and perspicuous. We achieve this goal by embedding the programs into existing languages (such as Haskell, SML, and OCaml) with high-quality implementations, by making choices lazily and representing data with non-deterministic components, by working with custom monadic data types and search strategies, and by providing equational laws for the programmer to reason about their code.
✨ Summary
The paper develops a purely functional implementation of lazy non-determinism with call-time choice. Its central mechanism is an explicit share combinator that preserves sharing of non-deterministic computations, including computations nested inside data structures. The authors specify equational laws for reasoning about such programs and implement the mechanism as a monad transformer that can be combined with different MonadPlus instances, allowing alternative search strategies such as depth-first, breadth-first, parallel, constrained, or weighted search. The implementation supports Haskell and OCaml-style embeddings and reports competitive performance against Curry implementations, including faster execution for the paper’s permutation-sort benchmark. (homes.luddy.indiana.edu)
Subsequent research used the approach as a foundation for systematically translating lazy functional-logic programs into pure Haskell with explicit sharing. That work made the generated programs parametric over the evaluation monad, enabling different search strategies while retaining the paper’s sharing model. (researchgate.net) The approach also continued to be used in later work on monadic implementations of functional-logic languages, where memoization of non-deterministic branches and performance relative to Curry compilers remain central concerns. (michaelhanus.de)
The implementation was released as the explicit-sharing Haskell package, whose documentation demonstrates its use for lazy functional-logic programming in pure Haskell. (sebfisch.github.io) The available evidence therefore indicates influence primarily on functional-logic programming, monadic search, explicit sharing, and embedded probabilistic-programming research; no specific broad industrial deployment is documented in the sources reviewed.