Abstract
To demonstrate derivation of monadic programs, we present a specification of sorting using the non-determinism monad, and derive pure quicksort on lists and state-monadic quicksort on arrays. In the derivation one may switch between point-free and pointwise styles, and deploy techniques familiar to functional programmers such as pattern matching and induction on structures or on sizes. Derivation of stateful programs resembles reasoning backwards from the postcondition.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Unless we confine ourselves to stable sorting.
- 2.
This is standard in imperative program derivation—Dijkstra [6] argued that we should take non-determinism as default and determinism as a special case.
- 3.
- 4.
For example, we overlook that a \(\mathsf {Monad}\) must also be \(\mathsf {Applicative}\), \(\mathsf {MonadPlus}\) be \(\mathsf {Alternative}\), and that functional dependency is needed in a number of places.
- 5.
It might be worth noting that \( partl \) causes a space leak in Haskell, since the accumulators become thunks that increase in size as the input list is traversed. It does not matter here since \( partl \) merely serves as a specification of \( ipartl \).
- 6.
We will discover a stronger specification
, where
. We omit the details.
, where
. We omit the details.References
Backhouse, R.C., de Bruin, P.J., Malcolm, G., Voermans, E., van der Woude, J.: Relational catamorphisms. In: Möller, B. (ed.) Proceedings of the IFIP TC2/WG2.1 Working Conference on Constructing Programs, pp. 287–318. Elsevier Science Publishers (1991)
Bentley, J.L.: Programming Pearls, 2nd edn. Addison-Wesley, Boston (2000)
Bird, R.S.: Functional algorithm design. Sci. Comput. Program. 26, 15–31 (1996)
Bird, R.S., de Moor, O.: Algebra of programming. In: International Series in Computer Science. Prentice Hall (1997)
Bird, R., Rabe, F.: How to calculate with nondeterministic functions. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 138–154. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33636-3_6
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Upper Saddle River (1976)
Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: Danvy, O. (ed.) International Conference on Functional Programming, pp. 2–14. ACM Press (2011)
Gill, A., Kmett, E.: The monad transformer library (2014). https://hackage.haskell.org/package/mtl
Hoare, C.A.R.: Algorithm 63: partition. Commun. ACM 4(7), 321 (1961)
Kiselyov, O.: How to restrict a monad without breaking it: the winding road to the Set monad, July 2013. http://okmij.org/ftp/Haskell/set-monad.html
Kiselyov, O., Ishii, H.: Freer monads, more extensible effects. In: Reppy, J.H. (ed.) Symposium on Haskell, pp. 94–105. ACM Press (2015)
Moggi, E.: Computational lambda-calculus and monads. In: Parikh, R. (ed.) Logic in Computer Science, pp. 14–23. IEEE Computer Society Press (1989)
de Moor, O., Gibbons, J.: Pointwise relational programming. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 371–390. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-45499-3_27
Pauwels, K., Schrijvers, T., Mu, S.-C.: Handling local state with global state. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 18–44. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33636-3_2
Acknowledgements
The authors would like to thank Jeremy Gibbons for the valuable discussions during development of this work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Mu, SC., Chiang, TJ. (2020). Declarative Pearl: Deriving Monadic Quicksort. In: Nakano, K., Sagonas, K. (eds) Functional and Logic Programming. FLOPS 2020. Lecture Notes in Computer Science(), vol 12073. Springer, Cham. https://doi.org/10.1007/978-3-030-59025-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-59025-3_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-59024-6
Online ISBN: 978-3-030-59025-3
eBook Packages: Computer ScienceComputer Science (R0)