Type-driven Development with Idris

Type-Driven Development with Idris......Page 1
brief contents......Page 7
contents......Page 9
preface......Page 17
acknowledgments......Page 19
 Roadmap......Page 21
 Author Online......Page 23
 Other online resources......Page 24
about the author......Page 25
about the cover illustration......Page 26
Part 1 Introduction......Page 27
 1 Overview......Page 29
  1.1 What is a type?......Page 30
  1.2 Introducing type-driven development......Page 31
   1.2.1 Matrix arithmetic......Page 32
   1.2.2 An automated teller machine......Page 33
   1.2.3 Concurrent programming......Page 35
   1.2.4 Type, define, refine: the process of type-driven development......Page 36
   1.2.5 Dependent types......Page 37
   1.3.1 Purity and referential transparency......Page 39
   1.3.2 Side-effecting programs......Page 40
   1.3.3 Partial and total functions......Page 42
   1.4.1 The interactive environment......Page 43
   1.4.2 Checking types......Page 44
   1.4.3 Compiling and running Idris programs......Page 45
   1.4.4 Incomplete definitions: working with holes......Page 46
   1.4.5 First-class types......Page 48
  1.5 Summary......Page 50
 2 Getting started with Idris......Page 51
  2.1 Basic types......Page 52
   2.1.1 Numeric types and values......Page 53
   2.1.2 Type conversions using cast......Page 54
   2.1.3 Characters and strings......Page 55
  2.2 Functions: the building blocks of Idris programs......Page 56
   2.2.1 Function types and definitions......Page 57
   2.2.3 Writing generic functions: variables in types......Page 59
   2.2.4 Writing generic functions with constrained types......Page 61
   2.2.5 Higher-order function types......Page 62
   2.2.6 Anonymous functions......Page 64
   2.2.7 Local definitions: let and where......Page 65
   2.3.1 Tuples......Page 66
   2.3.2 Lists......Page 67
   2.3.3 Functions with lists......Page 69
   2.4.1 Whitespace significance: the layout rule......Page 72
   2.4.2 Documentation comments......Page 73
   2.4.3 Interactive programs......Page 74
  2.5 Summary......Page 78
Part 2 Core Idris......Page 79
 3 Interactive development with types......Page 81
  3.1 Interactive editing in Atom......Page 82
   3.1.2 Defining functions by pattern matching......Page 83
   3.1.3 Data types and patterns......Page 87
  3.2 Adding precision to types: working with vectors......Page 90
   3.2.1 Refining the type of allLengths......Page 91
   3.2.2 Type-directed search: automatic refining......Page 95
   3.2.3 Type, define, refine: sorting a vector......Page 96
  3.3 Example: type-driven development of matrix functions......Page 101
   3.3.1 Matrix operations and their types......Page 102
   3.3.2 Transposing a matrix......Page 103
   3.4.1 The need for implicit arguments......Page 108
   3.4.2 Bound and unbound implicits......Page 109
   3.4.3 Using implicit arguments in functions......Page 110
  3.5 Summary......Page 112
 4 User-defined data types......Page 113
  4.1 Defining data types......Page 114
   4.1.1 Enumerations......Page 115
   4.1.2 Union types......Page 116
   4.1.3 Recursive types......Page 118
   4.1.4 Generic data types......Page 121
   4.2.1 A first example: classifying vehicles by power source......Page 128
   4.2.2 Defining vectors......Page 130
   4.2.3 Indexing vectors with bounded numbers using Fin......Page 133
  4.3 Type-driven implementation of an interactive data store......Page 136
   4.3.1 Representing the store......Page 138
   4.3.2 Interactively maintaining state in main......Page 139
   4.3.3 Commands: parsing user input......Page 141
   4.3.4 Processing commands......Page 144
  4.4 Summary......Page 148
 5 Interactive programs: input and output processing......Page 149
  5.1 Interactive programming with IO......Page 150
   5.1.1 Evaluating and executing interactive programs......Page 151
   5.1.2 Actions and sequencing: the >>= operator......Page 153
   5.1.3 Syntactic sugar for sequencing with do notation......Page 155
   5.2.1 Producing pure values in interactive definitions......Page 158
   5.2.2 Pattern-matching bindings......Page 160
   5.2.3 Writing interactive definitions with loops......Page 162
  5.3 Reading and validating dependent types......Page 164
   5.3.1 Reading a Vect from the console......Page 165
   5.3.2 Reading a Vect of unknown length......Page 166
   5.3.3 Dependent pairs......Page 167
   5.3.4 Validating Vect lengths......Page 169
  5.4 Summary......Page 172
 6 Programming with first-class types......Page 173
  6.1 Type-level functions: calculating types......Page 174
   6.1.1 Type synonyms: giving informative names to complex types......Page 175
   6.1.2 Type-level functions with pattern matching......Page 176
   6.1.3 Using case expressions in types......Page 179
   6.2.1 An addition function......Page 181
   6.2.2 Formatted output: a type-safe printf function......Page 183
  6.3 Enhancing the interactive data store with schemas......Page 187
   6.3.1 Refining the DataStore type......Page 188
   6.3.2 Using a record for the DataStore......Page 190
   6.3.3 Correcting compilation errors using holes......Page 191
   6.3.4 Displaying entries in the store......Page 196
   6.3.5 Parsing entries according to the schema......Page 197
   6.3.6 Updating the schema......Page 201
   6.3.7 Sequencing expressions with Maybe using do notation......Page 203
  6.4 Summary......Page 207
 7 Interfaces: using constrained generic types......Page 208
   7.1.1 Testing for equality with Eq......Page 209
   7.1.2 Defining the Eq constraint using interfaces and implementations......Page 211
   7.1.4 Constrained implementations......Page 215
   7.1.5 Constrained interfaces: defining orderings with Ord......Page 217
   7.2.1 Converting to String with Show......Page 220
   7.2.2 Defining numeric types......Page 221
   7.2.3 Converting between types with Cast......Page 224
  7.3 Interfaces parameterized by Type -> Type......Page 225
   7.3.1 Applying a function across a structure with Functor......Page 226
   7.3.2 Reducing a structure using Foldable......Page 227
   7.3.3 Generic do notation using Monad and Applicative......Page 231
  7.4 Summary......Page 233
 8 Equality: expressing relationships between data......Page 234
  8.1 Guaranteeing equivalence of data with equality types......Page 235
   8.1.1 Implementing exactLength, first attempt......Page 236
   8.1.2 Expressing equality of Nats as a type......Page 237
   8.1.3 Testing for equality of Nats......Page 238
   8.1.4 Functions as proofs: manipulating equalities......Page 241
   8.1.5 Implementing exactLength, second attempt......Page 242
   8.1.6 Equality in general: the = type......Page 244
   8.2.1 Reversing a vector......Page 246
   8.2.2 Type checking and evaluation......Page 247
   8.2.3 The rewrite construct: rewriting a type using equality......Page 249
   8.2.4 Delegating proofs and rewriting to holes......Page 250
   8.2.5 Appending vectors, revisited......Page 251
  8.3 The empty type and decidability......Page 253
   8.3.1 Void: a type with no values......Page 254
   8.3.2 Decidability: checking properties with precision......Page 255
   8.3.3 DecEq: an interface for decidable equality......Page 259
  8.4 Summary......Page 260
 9 Predicates: expressing assumptions and contracts in types......Page 262
  9.1 Membership tests: the Elem predicate......Page 263
   9.1.1 Removing an element from a Vect......Page 264
   9.1.2 The Elem type: guaranteeing a value is in a vector......Page 265
   9.1.3 Removing an element from a Vect: types as contracts......Page 267
   9.1.4 auto-implicit arguments: automatically constructing proofs......Page 270
   9.1.5 Decidable predicates: deciding membership of a vector......Page 271
   9.2.1 Representing the game?s state......Page 276
   9.2.3 A predicate for validating user input: ValidInput......Page 277
   9.2.4 Processing a guess......Page 279
   9.2.6 Completing the top-level game implementation......Page 281
  9.3 Summary......Page 283
 10 Views: extending pattern matching......Page 284
  10.1 Defining and using views......Page 285
   10.1.1 Matching the last item in a list......Page 286
   10.1.3 with blocks: syntax for extended pattern matching......Page 288
   10.1.4 Example: reversing a list using a view......Page 290
   10.1.5 Example: merge sort......Page 292
   10.2.1 ?Snoc? lists: traversing a list in reverse......Page 297
   10.2.2 Recursive views and the with construct......Page 300
   10.2.3 Traversing multiple arguments: nested with blocks......Page 301
   10.2.4 More traversals: Data.List.Views......Page 303
   10.3.1 Digression: modules in Idris......Page 306
   10.3.2 The data store, revisited......Page 308
   10.3.3 Traversing the store?s contents with a view......Page 310
  10.4 Summary......Page 314
Part 3 Idris and the real world......Page 315
 11 Streams and processes: working with infinite data......Page 317
  11.1 Streams: generating and processing infinite lists......Page 318
   11.1.1 Labeling elements in a List......Page 319
   11.1.2 Producing an infinite list of numbers......Page 321
   11.1.3 Digression: what does it mean for a function to be total?......Page 322
   11.1.4 Processing infinite lists......Page 323
   11.1.5 The Stream data type......Page 325
   11.1.6 An arithmetic quiz using streams of random numbers......Page 327
  11.2 Infinite processes: writing interactive total programs......Page 331
   11.2.1 Describing infinite processes......Page 332
   11.2.2 Executing infinite processes......Page 333
   11.2.3 Executing infinite processes as total functions......Page 334
   11.2.4 Generating infinite structures using Lazy types......Page 335
   11.2.6 A total arithmetic quiz......Page 337
   11.3.1 Refining InfIO: introducing termination......Page 340
   11.3.2 Domain-specific commands......Page 343
   11.3.3 Sequencing Commands with do notation......Page 346
  11.4 Summary......Page 349
 12 Writing programs with state......Page 350
  12.1 Working with mutable state......Page 351
   12.1.1 The tree-traversal example......Page 352
   12.1.2 Representing mutable state using a pair......Page 354
   12.1.3 State, a type for describing stateful operations......Page 355
   12.1.4 Tree traversal with State......Page 357
   12.2.1 Defining State and runState......Page 359
   12.2.2 Defining Functor, Applicative, and Monad implementations for State......Page 361
   12.3.1 Interactive programs with state: the arithmetic quiz revisited......Page 366
   12.3.2 Complex state: defining nested records......Page 369
   12.3.3 Updating record field values......Page 370
   12.3.5 Implementing the quiz......Page 372
   12.3.6 Running interactive and stateful programs: executing the quiz......Page 374
  12.4 Summary......Page 377
 13 State machines: verifying protocols in types......Page 378
  13.1 State machines: tracking state in types......Page 379
   13.1.1 Finite state machines: modeling a door as a type......Page 380
   13.1.2 Interactive development of sequences of door operations......Page 382
   13.1.3 Infinite states: modeling a vending machine......Page 384
   13.1.4 A verified vending machine description......Page 386
  13.2 Dependent types in state: implementing a stack......Page 389
   13.2.1 Representing stack operations in a state machine......Page 390
   13.2.2 Implementing the stack using Vect......Page 392
   13.2.3 Using a stack interactively: a stack-based calculator......Page 393
  13.3 Summary......Page 397
 14 Dependent state machines: handling feedback and errors......Page 399
  14.1 Dealing with errors in state transitions......Page 400
   14.1.1 Refining the door model: representing failure......Page 401
   14.1.2 A verified, error-checking, door-protocol description......Page 404
  14.2 Security properties in types: modeling an ATM......Page 408
   14.2.1 Defining states for the ATM......Page 409
   14.2.2 Defining a type for the ATM......Page 410
   14.2.3 Simulating an ATM at the console: executing ATMCmd......Page 413
   14.2.4 Refining preconditions using auto-implicits......Page 414
  14.3 A verified guessing game: describing rules in types......Page 416
   14.3.1 Defining an abstract game state and operations......Page 417
   14.3.2 Defining a type for the game state......Page 418
   14.3.3 Implementing the game......Page 421
   14.3.4 Defining a concrete game state......Page 423
   14.3.5 Running the game: executing GameLoop......Page 425
  14.4 Summary......Page 428
 15 Type-safe concurrent programming......Page 429
  15.1 Primitives for concurrent programming in Idris......Page 430
   15.1.1 Defining concurrent processes......Page 432
   15.1.2 The Channels library: primitive message passing......Page 433
   15.1.3 Problems with channels: type errors and blocking......Page 436
  15.2 Defining a type for safe message passing......Page 437
   15.2.1 Describing message-passing processes in a type......Page 438
   15.2.2 Making processes total using Inf......Page 441
   15.2.3 Guaranteeing responses using a state machine and Inf......Page 444
   15.2.4 Generic message-passing processes......Page 448
   15.2.5 Defining a module for Process......Page 452
   15.2.6 Example 1: List processing......Page 453
   15.2.7 Example 2: A word-counting process......Page 455
  15.3 Summary......Page 459
  Mac OS......Page 461
  Atom......Page 462
  Other editors......Page 463
appendix B  Interactive editing commands......Page 464
appendix C  REPL commands......Page 465
 Other languages and tools with expressive type systems......Page 467
 Total functional programming......Page 468
 Types for concurrency......Page 469
 C......Page 471
 E......Page 472
 G......Page 473
 I......Page 474
 P......Page 475
 S......Page 476
 T......Page 477
 V......Page 478
 Z......Page 479