Declarative Pearl: Deriving Monadic Quicksort

被引：2

作者：

Mu, Shin-Cheng ^{[1
]}

Chiang, Tsung-Ju ^{[2
]}

机构：

[1] Acad Sinica, Taipei, Taiwan

[2] Natl Taiwan Univ, Taipei, Taiwan

来源：

FUNCTIONAL AND LOGIC PROGRAMMING, FLOPS 2020 | 2020年 / 12073卷

关键词：

Monads; Program derivation; Equational reasoning; Nondeterminism; State; Quicksort;

D O I：

10.1007/978-3-030-59025-3_8

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：124 / 138

页数：15