arxiv: 2604.27863 · v1 · submitted 2026-04-30 · 💻 cs.PL

Recognition: unknown

A Monadic Implementation of Functional Logic Programs

Finn Teegen, Kai-Oliver Prott, Michael Hanus

Pith reviewed 2026-05-07 05:52 UTC · model grok-4.3

classification 💻 cs.PL

keywords functional logic programmingmonadic implementationHaskellCurrymemoizationnon-determinismdemand-driven evaluationencapsulated search

0 comments

The pith

Functional logic programs can be translated into a monadic form in pure Haskell that supports memoization of non-deterministic choices and outperforms current Curry compilers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to represent functional logic programs using a monad in Haskell so that demand-driven non-deterministic evaluation can be performed with correct sharing of choices. This addresses the duplication of work that arises when unevaluated expressions are copied across branches. The monadic interface is implemented to allow memoization inside non-deterministic computations without leaving the pure functional setting. Advanced constructs such as functional patterns and encapsulated search are incorporated into the same framework. Static and dynamic optimizations focused on the purely functional parts then yield runtimes that exceed those of existing Curry compilers.

Core claim

Functional logic programs can be transformed into a monadic representation in Haskell whose interface supports memoization within non-deterministic branches while remaining entirely pure. This representation correctly amalgamates demand-driven evaluation with non-determinism and extends to functional patterns and encapsulated search. When the purely functional portions are further optimized by both static and dynamic techniques, the resulting implementation produces better performance than current compilers for the Curry language.

What carries the argument

The monadic interface that represents functional logic computations and enables memoization of non-deterministic choices while preserving purity in Haskell.

If this is right

Functional logic languages become implementable inside a purely functional host language with competitive efficiency.
Memoization of non-deterministic computations can be achieved without relying on imperative side effects.
Features such as functional patterns and encapsulated search integrate directly into the monadic framework.
Static and dynamic optimizations can be applied separately to the deterministic portions to improve overall speed.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Haskell libraries and type-level programming techniques could be reused directly inside functional logic applications.
The same monadic pattern might be applied to other hybrid declarative languages that combine determinism with search.
Type-system guarantees available in Haskell could be used to prove correctness properties of the translated programs.
Extending the approach to additional language features or different back ends would be a natural next measurement.

Load-bearing premise

The monadic transformation preserves the original semantics of functional logic programs and implements memoization of choices correctly without introducing side effects.

What would settle it

A program that produces different results or a different number of solutions when executed via the monadic Haskell translation compared with a standard Curry implementation, or independent benchmarks that show no consistent performance advantage.

Figures

Figures reproduced from arXiv: 2604.27863 by Finn Teegen, Kai-Oliver Prott, Michael Hanus.

**Figure 1.** Figure 1: Type transformation J◦K t Jdata D α1 ...αn = C1 | ... | Cn K d := data rename(D) α1 ...αn = JC1K c | ... | JCnK c (Data type) JC τ1 ... τnK c := rename(C) Jτ1K t ... JτnK t (Constructor) view at source ↗

**Figure 3.** Figure 3: Expression transformation J◦K e (where f , y, y1,..., yn are fresh variables) or constructor-based conditional term rewriting system can be transformed into this flat form. For instance, the operation insert defined in Section 2 is desugared into the following flat form. insert = λ x → λ xs → case xs of Curry [] → [ x ] y : ys → ( x : y : ys ) ? ( y : insert x ys ) view at source ↗

**Figure 4.** Figure 4: Improved alias rule let newParents = Set . insert b2 p2 put ( MemoState i newParents idSupply2 ) return res | otherwise → return res 5.4 Improving Performance of Sharing There is one major performance bottleneck with this implementation. The problem is that share enters its argument into the memoization heap, even when a previous share has done so already. Repeated sharing of a computation is unnecessary a… view at source ↗

**Figure 5.** Figure 5: Revised data type transformation J◦K d each argument of a deterministic function needs to be deterministic so that the optimized version is applicable. Due to these complications, a purely static approach would often use non-deterministic variants of functions where it is not necessary at run time. Without the ability to detect deterministic values at run time, once we enter the realm of non-determinism, t… view at source ↗

**Figure 6.** Figure 6: Revised transformation rule for branches of case expressions J◦K b One might notice that doubling the number of branches can lead to an exponential increase in the size of the generated code in case of deeply nested case expressions. Actually, this turned out to be practically relevant since there are programs where the flat form yields large case expressions (e.g., pattern matching on strings). This can b… view at source ↗

**Figure 7.** Figure 7: Timings (in seconds) of various programs evaluated with different compilers, green marks best time istic programs. The remaining two benchmarks test expensive non-deterministic computations. Times for our approach are both “Monadic MPT” columns, where the latter one integrates the optimization for fully deterministic sub-computations from Section 7. Both are performed with a depth-first search strategy, GH… view at source ↗

read the original abstract

Functional logic languages are a high-level approach to programming by combining the most important declarative features. They abstract from small-step operational details so that programmers can concentrate on the logical aspects of an application. This is supported by appropriate evaluation strategies. Demand-driven evaluation from functional programming is amalgamated with non-determinism from logic programming so that solutions or values are computed whenever they exist. This frees the programmer from considering the influence of an operational strategy on the success of a computation, but it is a challenge to the language implementer. A non-deterministic demand-driven strategy might duplicate unevaluated choices of an expression, which could duplicate the computational effort. In recent implementations, this problem has been tackled by adding a kind of memoization of non-deterministic choices to the expression under evaluation. Since this has been implemented in imperative target languages, it was unclear whether this could also be supported in a functional programming environment like Haskell. This paper presents a solution to this challenge by transforming functional logic programs into a monadic representation. Although this transformation is not new, we present an implementation of the monadic interface which supports memoization in non-deterministic branches. Additionally, we include more advanced features of functional logic languages, namely functional patterns and encapsulated search, in our approach. By optimizing our implementation for purely functional computations with both a static and dynamic approach, we are able to achieve a promising performance that outperforms current compilers for Curry.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a concrete monadic encoding in pure Haskell for functional logic programs that adds memoization for non-determinism plus functional patterns and encapsulated search, with static-dynamic optimizations that reportedly beat Curry compilers, but treats semantic preservation as an assumption rather than a proven property.

read the letter

The main thing to take away from this paper is that it describes a monadic transformation of functional logic programs into pure Haskell that supports memoization of non-deterministic choices, includes functional patterns and encapsulated search, and uses static and dynamic optimizations to achieve better performance than existing Curry compilers. They build on the idea that monadic representations can handle the combination of demand-driven evaluation and non-determinism. The new part is the specific interface for memoization in non-deterministic branches while staying pure, plus folding in those extra features. This is useful because it lets you implement these languages without going to imperative code, and the optimizations help with the pure functional computations that make up a lot of the work. The approach looks solid for practical purposes. If the benchmarks hold up, the performance edge is a real win for the field. Where it is softer is on the semantics side. The paper notes the transformation itself is not new, but does not provide a formal argument or proof that the monadic version preserves the behavior of the original programs, particularly with the memoization mechanism. The stress-test concern is fair here: without that, it's possible that some programs behave differently under nested non-determinism or search. The performance numbers would then need to be taken with that caveat. Overall, this is the kind of paper for people who implement or extend declarative languages. Someone working on Curry or similar systems, or on monads for non-determinism, would get concrete ideas from it. It is worth a serious referee because it delivers an implemented system with reported gains on a known hard problem. I would send it out for peer review. The implementation details and optimization strategies are the parts that matter most here, and they seem worth checking.

Referee Report

2 major / 2 minor

Summary. The paper presents a monadic transformation of functional logic programs (Curry-style) into pure Haskell. The monad supports demand-driven non-determinism together with memoization of choices to prevent duplication of work, plus functional patterns and encapsulated search. Static and dynamic optimizations targeted at purely functional sub-computations are claimed to yield performance that outperforms existing Curry compilers.

Significance. If the implementation is semantically faithful and the performance numbers are reproducible, the result would be significant: it demonstrates that the sharing required for efficient non-deterministic demand-driven evaluation can be realized entirely within a pure functional language, removing the previous necessity for imperative target-language features. This could simplify future FLP implementations and improve their portability and maintainability.

major comments (2)

[§3] §3 (Monadic Interface and Memoization): the central claim that the new monadic interface correctly implements memoization of non-deterministic choices in pure Haskell is load-bearing, yet the paper supplies neither a formal semantics for the source language nor a bisimulation or equivalence proof relating it to the target monad. Without such a relation it is impossible to verify that the memoization mechanism preserves the set of solutions and the observable behavior of encapsulated search.
[§6] §6 (Performance Evaluation): the claim that the implementation 'outperforms current compilers for Curry' is central to the contribution, but the section provides insufficient detail on benchmark selection, measurement methodology, the concrete static and dynamic optimizations applied, and any statistical analysis of the results. This makes it impossible to assess whether the reported gains are attributable to the monadic techniques rather than implementation artifacts or benchmark choice.

minor comments (2)

[Abstract] The abstract uses the vague qualifier 'promising performance'; quantitative statements (speed-up factors, absolute run-times, or comparison tables) would improve precision.
[§3] Notation for the monad operations and the memoization primitives should be introduced with a small example that shows both the source Curry expression and the generated monadic code side-by-side.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the thoughtful and constructive comments on our manuscript. We address each major comment below, indicating the revisions we intend to make.

read point-by-point responses

Referee: [§3] §3 (Monadic Interface and Memoization): the central claim that the new monadic interface correctly implements memoization of non-deterministic choices in pure Haskell is load-bearing, yet the paper supplies neither a formal semantics for the source language nor a bisimulation or equivalence proof relating it to the target monad. Without such a relation it is impossible to verify that the memoization mechanism preserves the set of solutions and the observable behavior of encapsulated search.

Authors: We agree that a formal proof would provide stronger assurance of correctness. Our paper presents a practical implementation rather than a theoretical development, and the monadic design is based on established operational semantics for functional logic programming with sharing. To address this, we will revise Section 3 to include a more detailed informal argument explaining how the memoization in the monad preserves the set of solutions and the behavior of encapsulated search, supported by additional examples. A full formal semantics and bisimulation proof is outside the scope of this work but represents a valuable direction for future research. revision: partial
Referee: [§6] §6 (Performance Evaluation): the claim that the implementation 'outperforms current compilers for Curry' is central to the contribution, but the section provides insufficient detail on benchmark selection, measurement methodology, the concrete static and dynamic optimizations applied, and any statistical analysis of the results. This makes it impossible to assess whether the reported gains are attributable to the monadic techniques rather than implementation artifacts or benchmark choice.

Authors: We acknowledge the need for greater transparency in the performance evaluation. In the revised version, we will expand Section 6 with: (1) a clear description of the benchmark programs, their origins, and selection rationale; (2) detailed measurement methodology, including the hardware platform, number of repetitions, and averaging method; (3) explicit listing of the static and dynamic optimizations applied; and (4) statistical measures such as standard deviation across runs. This will enable better assessment of the results and their attribution to the monadic approach. revision: yes

standing simulated objections not resolved

A complete formal semantics for the source language and a bisimulation proof relating it to the monadic implementation, as developing this would constitute a separate theoretical contribution beyond the implementation focus of the current paper.

Circularity Check

0 steps flagged

No circularity in monadic implementation or performance claims

full rationale

The paper describes a concrete Haskell implementation that transforms functional logic programs into a monadic form supporting memoization, functional patterns, and encapsulated search. It explicitly notes that the core transformation is not new and focuses on a new monadic interface plus optimizations (static and dynamic) for pure computations. Performance results are obtained by running benchmarks against existing Curry compilers rather than by deriving predictions from fitted parameters or self-referential equations. No load-bearing self-citations, uniqueness theorems, ansatzes smuggled via prior work, or renamings of known results appear in the derivation chain. The implementation is presented as an engineering artifact whose correctness and efficiency are evaluated empirically, making the paper self-contained against external benchmarks with no reduction of outputs to inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that the monadic encoding correctly captures the operational semantics of functional logic languages and that memoization can be added without violating purity. No free parameters, new axioms beyond standard Haskell monads and language semantics, or invented entities are described in the abstract.

axioms (1)

standard math Standard semantics of functional logic languages (Curry) and monadic programming in Haskell
The implementation builds directly on these established concepts without introducing new unproven foundations.

pith-pipeline@v0.9.0 · 5550 in / 1247 out tokens · 33169 ms · 2026-05-07T05:52:37.291118+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

21 extracted references

[1]

Verifying Haskell programs using constructive type theory

ABEL, A., BENKE, M., BOVE, A., HUGHES, J.,ANDNORELL, U. Verifying Haskell programs using constructive type theory. InProceedings of the 2005 ACM SIGPLAN Workshop on Haskell2005, pp. 62–73, New York, NY , USA. ACM Press. ALBERT, E., HANUS, M., HUCH, F., OLIVER, J.,ANDVIDAL, G

2005
[2]

ALQADDOUMI, A., ANTOY, S., FISCHER, S.,ANDRECK, F

Operational semantics for declarative multi-paradigm languages.Journal of Symbolic Computation,40, 1, 795–829. ALQADDOUMI, A., ANTOY, S., FISCHER, S.,ANDRECK, F. The pull-tab transformation. InProc. of the Third International Workshop on Graph Computation Models2010, pp. 127–132, Enschede, The Netherlands. Published Online. Available at http://gcm2010.ima...

1997
[3]

Constructor-based conditional narrowing

ANTOY, S. Constructor-based conditional narrowing. InProc. of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001)2001, pp. 199–206, New York, NY , USA. ACM Press. ANTOY, S

2001
[4]

ANTOY, S.ANDBRASSEL, B

On the correctness of pull-tabbing.Theory and Practice of Logic Programming,11, 4-5, 713–730. ANTOY, S.ANDBRASSEL, B. Computing with subspaces. InProceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’07)2007, pp. 121–130. ACM Press. ANTOY, S., ECHAHED, R.,ANDHANUS, M

2007
[5]

ANTOY, S.ANDHANUS, M

A needed narrowing strategy.Journal of the ACM,47, 4, 776–822. ANTOY, S.ANDHANUS, M. Compiling multi-paradigm declarative programs into Prolog. InProc. In- 34Michael Hanus, Kai-Oliver Prott, Finn Teegen ternational Workshop on Frontiers of Combining Systems (FroCoS’2000)2000, pp. 171–185, Berlin, Heidelberg. Springer LNCS

2000
[6]

Functional logic design patterns

ANTOY, S.ANDHANUS, M. Functional logic design patterns. InProc. of the 6th International Symposium on Functional and Logic Programming (FLOPS 2002)2002, pp. 67–87. Springer LNCS

2002
[7]

Declarative programming with function patterns

ANTOY, S.ANDHANUS, M. Declarative programming with function patterns. InProceedings of the International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR’05)2005, pp. 6–22, Berlin, Heidelberg. Springer LNCS

2005
[8]

Overlapping rules and logic variables in functional logic programs

ANTOY, S.ANDHANUS, M. Overlapping rules and logic variables in functional logic programs. In Proceedings of the 22nd International Conference on Logic Programming (ICLP 2006)2006, pp. 87–101, Berlin, Heidelberg. Springer LNCS

2006
[9]

Set functions for functional logic programming

ANTOY, S.ANDHANUS, M. Set functions for functional logic programming. InProceedings of the 11th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’09) 2009, pp. 73–82, New York, NY , USA. ACM Press. ANTOY, S.ANDHANUS, M

2009
[10]

ANTOY, S., HANUS, M., JOST, A.,ANDLIBBY, S

Functional logic programming.Communications of the ACM,53, 4, 74–85. ANTOY, S., HANUS, M., JOST, A.,ANDLIBBY, S. ICurry. InDeclarative Programming and Knowledge Management - Conference on Declarative Programming (DECLARE 2019)2020, pp. 286–307, Berlin, Heidelberg. Springer LNCS 12057. ANTOY, S.ANDJOST, A. A new functional-logic compiler for Curry: Sprite....

2019
[11]

Encapsulating non-determinism in functional logic computations.Journal of Functional and Logic Programming,2004,

2004
[12]

KiCS2: A new compiler from Curry to Haskell

BRASSEL, B., HANUS, M., PEEM ¨OLLER, B.,ANDRECK, F. KiCS2: A new compiler from Curry to Haskell. InProc. of the 20th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2011)2011, pp. 1–18, Berlin, Heidelberg. Springer LNCS

2011
[13]

A semantics for weakly encapsulated search in functional logic programs

CHRISTIANSEN, J., HANUS, M., RECK, F.,ANDSEIDEL, D. A semantics for weakly encapsulated search in functional logic programs. InProc. of the 15th International Symposium on Principle and Practice of Declarative Programming (PPDP’13)2013, pp. 49–60, New York, NY , USA. ACM Press. DEMOURA, L.ANDBJØRNER, N. Z3: An efficient SMT solver. InProc. of the 14th Int...

2013
[14]

Improving logic programs by adding functions

HANUS, M. Improving logic programs by adding functions. InProceedings of the 34th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2024)2024, pp. 27–44. Springer LNCS 14919. HANUS, M., ANTOY, S., BRASSEL, B., ENGELKE, M., H ¨OPPNER, K., KOJ, J., NIEDERAU, P., SADRE, R., STEINER, F.,ANDTEEGEN, F

2024
[15]

Available at https://www.curry-lang.org/pakcs/

PAKCS: The Portland Aachen Kiel Curry System. Available at https://www.curry-lang.org/pakcs/. HANUS, M., PEEM ¨OLLER, B.,ANDRECK, F. Search strategies for functional logic programming. InProc. of the 5th Working Conference on Programming Languages (ATPS’12)2012, pp. 61–74, Bonn. Springer LNI

2012
[16]

A monadic implementation of functional logic programs

HANUS, M., PROTT, K.-O.,ANDTEEGEN, F. A monadic implementation of functional logic programs. InProc. of the 24th International Symposium on Principles and Practice of Declarative Programming (PPDP 2022)2022, pp. 1:1–1:15. ACM Press. HANUS, M.ANDSKRLAC, F. A modular and generic analysis server system for functional logic programs. In Proc. of the ACM SIGPL...

2022
[17]

ACM Program

Efficient compilation of algebraic effect handlers.Proc. ACM Program. Lang.,5, OOPSLA. LLOYD, J. 1987.Foundations of Logic Programming. Springer, second, extended edition, Berlin, Heidelberg. L ´OPEZ-FRAGUAS, F.ANDS ´ANCHEZ-HERN ´ANDEZ, J. TOY: A multiparadigm declarative system. InProc. of RTA’991999, pp. 244–247, Berlin, Heidelberg. Springer LNCS

1987
[18]

2005.The Implementation of Practical Functional Programming Languages

PERRY, N. 2005.The Implementation of Practical Functional Programming Languages. PhD thesis, Univer- sity of London. PETRICEK, T

2005
[19]

PEYTONJONES, S., editor 2003.Haskell 98 Language and Libraries—The Revised Report

Evaluation strategies for monadic computations.Electronic Proceedings in Theoretical Computer Science,76, 68–89. PEYTONJONES, S., editor 2003.Haskell 98 Language and Libraries—The Revised Report. Cambridge University Press, Cambridge, UK. 36Michael Hanus, Kai-Oliver Prott, Finn Teegen PEYTONJONES, S., GORDON, A.,ANDFINNE, S. Concurrent Haskell. InProc. 23...

2003
[20]

Journal of the ACM,21, 4, 622–642

Automated theorem-proving for theories with simplifiers, commutativity, and associativity. Journal of the ACM,21, 4, 622–642. TEEGEN, F., PROTT, K.-O.,ANDBUNKENBURG, N. Haskell −1: Automatic function inversion in Haskell. InProceedings of the 14th ACM SIGPLAN International Symposium on Haskell2021, Haskell 2021, pp. 41–55, New York, NY , USA. Association ...

2021
[21]

Comprehending monads

WADLER, P. Comprehending monads. InProc. 1990 ACM Conference on LISP and Functional Programming 1990, pp. 61–78, New York, NY , USA. ACM. WADLER, P

1990