Hostname: page-component-6898cfcb55-zsp5v Total loading time: 0 Render date: 2026-11-11T04:11:36.441Z Has data issue: false hasContentIssue false
  • English
  • Français

Backtracking with cut via a distributive law and left-zero monoids*

Published online by Cambridge University Press:  13 July 2017

MACIEJ PIRÓG and
SAM STATON
MACIEJ PIRÓG
Affiliation:
University of Wrocław, Poland (e-mail: maciej.adam.pirog@gmail.com)
SAM STATON
Affiliation:
University of Oxford, UK
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We employ the framework of algebraic effects to augment the list monad with the pruning cut operator known from Prolog. We give two descriptions of the resulting monad: as the monad of free left-zero monoids, and as a composition via a distributive law of the list monad and the ‘unary idempotent operation’ monad. The scope delimiter of cut arises as a handler.

Information

Type
Theoretical Pearls
Information
Journal of Functional Programming , Volume 27 , 2017, e17
Copyright
Copyright © Cambridge University Press 2017 

Footnotes

*

Research supported by a Royal Society University Research Fellowship and EPSRC Grant EP/N007387/1

References

Baader, F. & Nipkow, T. (1998) Term Rewriting and All That. Cambridge University Press.Google Scholar
Barr, M. & Wells, C. (1985) Toposes, Triples and Theories. Springer-Verlag.Google Scholar
Beck, J. M. (1969) Distributive laws. In Seminar on Triples and Categorical Homology Theory, Lecture Notes in Mathematics, vol. 80. Berlin/Heidelberg: Springer, pp. 119–140.CrossRefGoogle Scholar
Billaud, M. (1990) Simple operational and denotational semantics for Prolog with cut. Theor. Comput. Sci. 71 (2), 193–208.Google Scholar
Bird, R. S. (2006) Functional pearl: A program to solve Sudoku. J. Funct. Progr. 16 (6), 671–679.CrossRefGoogle Scholar
Cheng, E. (2011) Distributive laws for Lawvere theories. Algebra Universalis. arXiv:1112.3076.Google Scholar
Hinze, R. (2000) Deriving backtracking monad transformers. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP '00), pp. 186–197.Google Scholar
Hinze, R. (2012) Kan extensions for program optimisation or: Art and Dan explain an old trick. In Proceedings of Mathematics of Program Construction—11th International Conference, MPC 2012, Lecture Notes in Computer Science, vol. 7342. Berlin/Heidelberg: Springer, pp. 324–362.CrossRefGoogle Scholar
Hyland, M. & Power, J. (2006) Discrete Lawvere theories and computational effects. Theor. Comput. Sci. 366 (1), 144–162.Google Scholar
Hyland, M., Plotkin, G. D. & Power, J. (2006) Combining effects: Sum and tensor. Theor. Comput. Sci. 357 (1–3), 70–99.CrossRefGoogle Scholar
Jaskelioff, M. & Moggi, E. (2010) Monad transformers as monoid transformers. Theor. Comput. Sci. 411 (51–52), 4441–4466.CrossRefGoogle Scholar
Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd ed. Springer.Google Scholar
Piróg, M. (2016) Eilenberg–Moore monoids and backtracking monad transformers. In Proceedings 6th Workshop on Mathematically Structured Functional Programming, Electronic Proceedings in Theoretical Computer Science, vol. 207, pp. 23–56.CrossRefGoogle Scholar
Plotkin, G. D. & Power, A. J. (2004) Computational effects and operations: An overview. Electron. Notes Theor. Comput. Sci. 73, 149–163.CrossRefGoogle Scholar
Plotkin, G. D. & Pretnar, M. (2013) Handling algebraic effects. Log. Methods Comput. Sci. 9 (4).Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.