《Programming with Refinement Types - An Introduction to LiquidHaskell》

【实例截图】

【核心代码】

Contents
1 Introduction 11
Well-Typed Programs Do Go Wrong 11
Refinement Types 13
Audience 13
Getting Started 13
Sample Code 14
2 Logic & SMT 15
Syntax 15
Semantics 16
Verification Conditions 18
Examples: Propositions 19
Examples: Arithmetic 20
Examples: Uninterpreted Function 22
Recap 23
4 ranjit jhala, eric seidel, niki vazou
3 Refinement Types 25
Defining Types 25
Errors 26
Subtyping 26
Writing Specifications 27
Refining Function Types: Pre-conditions 28
Refining Function Types: Post-conditions 29
Testing Values: Booleans and Propositions 29
Putting It All Together 31
Recap 31
4 Polymorphism 33
Specification: Vector Bounds 34
Verification: Vector Lookup 35
Inference: Our First Recursive Function 36
Higher-Order Functions: Bottling Recursion in a loop 37
Refinements and Polymorphism 39
Recap 40
5 Refined Datatypes 41
Sparse Vectors Revisited 41
Ordered Lists 44
Ordered Trees 46
Recap 49
programming with refinement types 5
Partial Functions 50
Lifting Functions to Measures 51
A Safe List API 53
Recap 56
6 Numeric Measures 57
Wholemeal Programming 57
Specifying List Dimensions 59
Lists: Size Preserving API 60
Lists: Size Reducing API 62
Dimension Safe Vector API 64
Dimension Safe Matrix API 66
Recap 69
7 Elemental Measures 71
Talking about Sets 71
Proving QuickCheck Style Properties 72
Content-Aware List API 74
Permutations 76
Uniqueness 78
Unique Zippers 80
Recap 82
Queues 83
Sized Lists 85
Queue Type 86
Queue Operations 87
Recap 89
6 ranjit jhala, eric seidel, niki vazou
8 Case Study: Associative Maps 91
Specifying Maps 91
Using Maps: Well Scoped Expressions 92
Implementing Maps: Binary Search Trees 96
Recap 100
HeartBleeds in Haskell 101
Low-level Pointer API 102
A Refined Pointer API 103
Assumptions vs Guarantees 106
ByteString API 107
Application API 111
Nested ByteStrings 112
Recap: Types Against Overflows 114
9 Case Study: AVL Trees 117
AVL Trees 117
Specifying AVL Trees 118
Smart Constructors 120
Inserting Elements 121
Rebalancing Trees 122
Refactoring Rebalance 127
Deleting Elements 129
Functional Correctness 130
List of Exercises
2.1 Exercise (Implications and Or) . . . . . . . . . . . . . . . 20
2.2 Exercise (DeMorgan’s Law) . . . . . . . . . . . . . . . . . 20
2.3 Exercise (Addition and Order) . . . . . . . . . . . . . . . 21
3.1 Exercise (List Average) . . . . . . . . . . . . . . . . . . . . 29
3.2 Exercise (Propositions) . . . . . . . . . . . . . . . . . . . . 30
3.3 Exercise (Assertions) . . . . . . . . . . . . . . . . . . . . . 30
4.1 Exercise (Vector Head) . . . . . . . . . . . . . . . . . . . . 36
4.2 Exercise (Unsafe Lookup) . . . . . . . . . . . . . . . . . . 36
4.3 Exercise (Safe Lookup) . . . . . . . . . . . . . . . . . . . . 36
4.4 Exercise (Guards) . . . . . . . . . . . . . . . . . . . . . . . 37
4.5 Exercise (Absolute Sum) . . . . . . . . . . . . . . . . . . . 37
4.6 Exercise (Off by one?) . . . . . . . . . . . . . . . . . . . . 37
4.7 Exercise (Using Higher-Order Loops) . . . . . . . . . . . 38
4.8 Exercise (Dot Product) . . . . . . . . . . . . . . . . . . . . 38
5.1 Exercise (Sanitization) . . . . . . . . . . . . . . . . . . . . 43
5.2 Exercise (Addition) . . . . . . . . . . . . . . . . . . . . . . 43
5.3 Exercise (Insertion Sort) . . . . . . . . . . . . . . . . . . . 45
5.4 Exercise (QuickSort) . . . . . . . . . . . . . . . . . . . . . 46
5.5 Exercise (Duplicates) . . . . . . . . . . . . . . . . . . . . . 48
5.6 Exercise (Delete) . . . . . . . . . . . . . . . . . . . . . . . . 49
5.7 Exercise (Safely Deleting Minimum) . . . . . . . . . . . . 49
5.8 Exercise (BST Sort) . . . . . . . . . . . . . . . . . . . . . . 49
8 ranjit jhala, eric seidel, niki vazou
5.9 Exercise (Average, Maybe) . . . . . . . . . . . . . . . . . . 52
5.10 Exercise (Debugging Specifications) . . . . . . . . . . . . 52
5.11 Exercise (Safe Head) . . . . . . . . . . . . . . . . . . . . . 53
5.12 Exercise (Weighted Average) . . . . . . . . . . . . . . . . 55
5.13 Exercise (Mitchell’s Risers) . . . . . . . . . . . . . . . . . . 55
6.1 Exercise (Map) . . . . . . . . . . . . . . . . . . . . . . . . . 60
6.2 Exercise (Reverse) . . . . . . . . . . . . . . . . . . . . . . . 60
6.3 Exercise (Zip Unless Empty) . . . . . . . . . . . . . . . . . 61
6.4 Exercise (Drop) . . . . . . . . . . . . . . . . . . . . . . . . 62
6.5 Exercise (Take it easy) . . . . . . . . . . . . . . . . . . . . 62
6.6 Exercise (QuickSort) . . . . . . . . . . . . . . . . . . . . . 63
6.7 Exercise (Vector Constructor) . . . . . . . . . . . . . . . . 65
6.8 Exercise (Flatten) . . . . . . . . . . . . . . . . . . . . . . . 65
6.9 Exercise (Legal Matrix) . . . . . . . . . . . . . . . . . . . . 67
6.10 Exercise (Matrix Constructor) . . . . . . . . . . . . . . . . 67
6.11 Exercise (Refined Matrix Constructor) . . . . . . . . . . . 67
6.12 Exercise (Matrix Transpose) . . . . . . . . . . . . . . . . . 68
7.1 Exercise (Bounded Addition) . . . . . . . . . . . . . . . . 73
7.2 Exercise (Set Difference) . . . . . . . . . . . . . . . . . . . 74
7.3 Exercise (Reverse) . . . . . . . . . . . . . . . . . . . . . . . 75
7.4 Exercise (Halve) . . . . . . . . . . . . . . . . . . . . . . . . 76
7.5 Exercise (Membership) . . . . . . . . . . . . . . . . . . . . 76
7.6 Exercise (Merge) . . . . . . . . . . . . . . . . . . . . . . . . 77
7.7 Exercise (Merge Sort) . . . . . . . . . . . . . . . . . . . . . 77
7.8 Exercise (Filter) . . . . . . . . . . . . . . . . . . . . . . . . 79
7.9 Exercise (Reverse) . . . . . . . . . . . . . . . . . . . . . . . 79
7.10 Exercise (Append) . . . . . . . . . . . . . . . . . . . . . . 80
7.11 Exercise (Range) . . . . . . . . . . . . . . . . . . . . . . . . 80
7.12 Exercise (Deconstructing Zippers) . . . . . . . . . . . . . 81
7.13 Exercise (Destructing Lists) . . . . . . . . . . . . . . . . . 86
programming with refinement types 9
7.14 Exercise (Whither pattern matching?) . . . . . . . . . . . 87
7.15 Exercise (Queue Sizes) . . . . . . . . . . . . . . . . . . . . 87
7.16 Exercise (Insert) . . . . . . . . . . . . . . . . . . . . . . . . 88
7.17 Exercise (Rotate) . . . . . . . . . . . . . . . . . . . . . . . . 88
7.18 Exercise (Transfer) . . . . . . . . . . . . . . . . . . . . . . 89
8.1 Exercise (Wellformedness Check) . . . . . . . . . . . . . . 95
8.2 Exercise (Closures) . . . . . . . . . . . . . . . . . . . . . . 95
8.3 Exercise (Empty Maps) . . . . . . . . . . . . . . . . . . . . 96
8.4 Exercise (Insert) . . . . . . . . . . . . . . . . . . . . . . . . 96
8.5 Exercise (Membership Test) . . . . . . . . . . . . . . . . . 99
8.6 Exercise (Fresh) . . . . . . . . . . . . . . . . . . . . . . . . 100
8.7 Exercise (Legal ByteStrings) . . . . . . . . . . . . . . . . . 109
8.8 Exercise (Create) . . . . . . . . . . . . . . . . . . . . . . . 109
8.9 Exercise (Pack) . . . . . . . . . . . . . . . . . . . . . . . . . 110
8.10 Exercise (Pack Invariant) . . . . . . . . . . . . . . . . . . . 110
8.11 Exercise (Unsafe Take and Drop) . . . . . . . . . . . . . . 110
8.12 Exercise (Unpack) . . . . . . . . . . . . . . . . . . . . . . . 111
8.13 Exercise (Checked Chop) . . . . . . . . . . . . . . . . . . . 112
9.1 Exercise (Singleton) . . . . . . . . . . . . . . . . . . . . . . 120
9.2 Exercise (Constructor) . . . . . . . . . . . . . . . . . . . . 120
9.3 Exercise (RightBig, NoHeavy) . . . . . . . . . . . . . . . . 125
9.4 Exercise (RightBig, RightHeavy) . . . . . . . . . . . . . . 126
9.5 Exercise (RightBig, LeftHeavy) . . . . . . . . . . . . . . . 126
9.6 Exercise (InsertRight) . . . . . . . . . . . . . . . . . . . . . 127
9.7 Exercise (Membership) . . . . . . . . . . . . . . . . . . . . 130
9.8 Exercise (Insertion) . . . . . . . . . . . . . . . . . . . . . . 131
9.9 Exercise (Insertion) . . . . . . . . . . . . . . . . . . . . . . 131