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

共 14 条

[1] Backhouse R.C., 1991, P IFIP TC2 WG2 1 WOR, P287
[2] Bentley J.L., 2000, Programming Pearls, V2nd
[3] Bird R.S., 1997, International Series in Computer Science
[4] How to Calculate with Nondeterministic Functions
Bird, Richard
Rabe, Florian
[J]. MATHEMATICS OF PROGRAM CONSTRUCTION, 2019, 11825 : 138 - 154
[5] Functional algorithm design
Bird, RS
[J]. SCIENCE OF COMPUTER PROGRAMMING, 1996, 26 (1-3) : 15 - 31
[6] de Moor O, 2000, LECT NOTES COMPUT SC, V1816, P371
[7] Dijkstra, 1976, DISCIPLINE PROGRAMMI
[8] Just do It: Simple Monadic Equational Reasoning
Gibbons, Jeremy
Hinze, Ralf
[J]. ACM SIGPLAN NOTICES, 2011, 46 (09) : 2 - 14
[9] Gill A., 2014, The monad transformer library
[10] Hoare C.A.R., 1961, Commun. ACM, V4, P321, DOI DOI 10.1145/366622.366644

← 1 2 →