Deriving monadic quicksort (Declarative Pearl)
Programming Languages
2021-01-28 v1 Data Structures and Algorithms
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.
Keywords
Cite
@article{arxiv.2101.11421,
title = {Deriving monadic quicksort (Declarative Pearl)},
author = {Shin-Cheng Mu and Tsung-Ju Chiang},
journal= {arXiv preprint arXiv:2101.11421},
year = {2021}
}