Type-driven development with Idris

SummaryType-Driven Development with Idris, written by the creator of Idris, teaches you how to improve the performance and accuracy of your programs by taking advantage of a state-of-the-art type system. This book teaches you with Idris, a language designed to support type-driven development.Purchase of the print book includes a free eBook in PDF, Kindle, and ePub formats from Manning Publications.About the TechnologyStop fighting type errors! Type-driven development is an approach to coding that embraces types as the foundation of your code - essentially as built-in documentation your compiler can use to check data relationships and other assumptions. With this approach, you can define specifications early in development and write code that's easy to maintain, test, and extend. Idris is a Haskell-like language with first-class, dependent types that's perfect for learning type-driven programming techniques you can apply in any codebase.About the BookType-Driven Development with Idris teaches you how to improve the performance and accuracy of your code by taking advantage of a state-of-the-art type system. In this book, you'll learn type-driven development of real-world software, as well as how to handle side effects, interaction, state, and concurrency. By the end, you'll be able to develop robust and verified software in Idris and apply type-driven development methods to other languages.What's InsideUnderstanding dependent typesTypes as first-class language constructsTypes as a guide to program constructionExpressing relationships between dataAbout the ReaderWritten for programmers with knowledge of functional programming concepts.About the AuthorEdwin Brady leads the design and implementation of the Idris language.Table of ContentsPART 1 - INTRODUCTIONOverviewGetting started with IdrisPART 2 - CORE IDRISInteractive development with typesUser-defined data typesInteractive programs: input and output processingProgramming with first-class typesInterfaces: using constrained generic typesEquality: expressing relationships between dataPredicates: expressing assumptions and contracts in typesViews: extending pattern matchingPART 3 - IDRIS AND THE REAL WORLDStreams and processes: working with infinite dataWriting programs with stateState machines: verifying protocols in typesDependent state machines: handling feedback and errorsType-safe concurrent programming 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 Types are often seen as a tool for checking errors, with the programmer writing a complete program first and using the type checker to detect errors. And while tests are used to show presence of errors, they can only find errors that you explicitly test for. In type-driven development, types become your tools for constructing programs and, used appropriately, can show the absence of errors. And you can express precise relationships between data, your assumptions are explicit and checkable, and you can precisely state and verify properties. Type-driven development lets users write extensible code, create simple specifications very early in development, and easily create mock implementation for testing. This book, written by the creator of Idris, teaches programmers how to improve the performance and accuracy of programs by taking advantage of a state-of-the-art type system Type-Driven Development with Idris, written by the creator of Idris, teaches you how to improve the performance and accuracy of your programs by taking advantage of a state-of-the-art type system. This book teaches you with Idris, a language designed from the very beginning to support type-driven development. In this book, youll learn how to manipulate types just like any other construct (numbers, strings, lists, etc.). Youll see how to use type-driven development to build real-world software, as well as how to handle side-effects, state and concurrency, and interoperating with existing systems. By the end of this book, you will be able to develop robust and verified software in Idris and apply type-driven development methods to programming in other languages.