Deriving monadic quicksort (Declarative Pearl)

TL;DR

This paper demonstrates how to derive monadic quicksort algorithms from specifications, showcasing techniques for functional program derivation and reasoning about stateful computations.

Contribution

It introduces a method for deriving pure and stateful quicksort algorithms within a monadic framework, illustrating the process with detailed derivations.

Findings

Derived pure quicksort on lists

Derived state-monadic quicksort on arrays

Showcased derivation techniques for monadic programs

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.