Type-Driven Development with Idris

by Edwin Brady

Overview

Summary

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 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 Technology

Stop 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 Book

Type-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 Inside

• Understanding dependent types
• Types as first-class language constructs
• Types as a guide to program construction
• Expressing relationships between data

About the Reader

Written for programmers with knowledge of functional programming concepts.

About the Author

Edwin Brady leads the design and implementation of the Idris language.

Table of Contents

PART 1 - INTRODUCTION
1. Overview
2. Getting started with IdrisPART 2 - CORE IDRIS
3. Interactive development with types
4. User-defined data types
5. Interactive programs: input and output processing
6. Programming with first-class types
7. Interfaces: using constrained generic types
8. Equality: expressing relationships between data
9. Predicates: expressing assumptions and contracts in types
10. Views: extending pattern matching
PART 3 - IDRIS AND THE REAL WORLD
11. Streams and processes: working with infinite data
12. Writing programs with state
13. State machines: verifying protocols in types
14. Dependent state machines: handling feedback and errors
15. Type-safe concurrent programming

Product Details

ISBN-13:	9781617293023
Publisher:	Manning
Publication date:	04/07/2017
Edition description:	1st Edition
Pages:	480
Product dimensions:	7.30(w) x 8.70(h) x 1.20(d)

About the Author

Edwin Brady leads the design and implementation of the Idris language. He is a Lecturer in Computer Science and regularly speaks at conferences.

Table of Contents

Preface xv

Acknowledgments xvii

About this book xix

About the author xxiii

About the cover illustration xxiv

Part I

1 Overview 3

1.1 What is a type? 4

1.2 Introducing type-driven development 5

Matrix arithmetic 6

An automated teller machine 7

Concurrent programming 9

Type, define, refine: the process of type-driven development 10

Dependent types 11

1.3 Pure functional programming 13

Purity and referential transparency 13

Side-effecting programs 14

Partial and total function 16

1.4 A quick tour of Idris 17

The interactive environment 17

Checking types 18

Compiling and running Idris programs 19

Incomplete definitions: working with holes 20

First-class types 22

1.5 Summary 24

2 Getting started with Idris 25

2.1 Basic types 26

Numeric types and values 27

Type conversions using cast 28

Characters and strings 29

Booleans 30

2.2 Functions: the building blocks of Idris programs 30

Function types and definitions 31

Partially applying functions 33

Writing generic functions: variables in types 33

Writing generic functions with constrained types 35

Higher-order function types 36

Anonymous functions 38

Local definitions: let and where 39

2.3 Composite types 40

Tuples 40

Lists 41

Functions with lists 43

2.4 A complete Idris program 46

Whitespace significance: the layout rule 46

Documentation comments 47

Interactive programs 48

2.5 Summary 52

Par 2 Core Idris 53

3 Interactive development with types 55

3.1 Interactive editing in Atom 56

Interactive command summary 57

Defining function by pattern matching 57

Data types and patterns 61

3.2 Adding precision to types: working with vectors 64

Refining the type of allLengths 65

Type-directed search: automatic refining 69

Type, define, refine: sorting a vector 70

3.3 Example: type-driven development of matrix functions 75

Matrix operations and their types 76

Transposing a matrix 77

3.4 Implicit arguments: type-level variables 82

The need for implicit arguments 82

Bound and unbound implicits 83

Using implicit arguments in functions 84

3.5 Summary 86

4 User-defined data types 87

4.1 Defining data types 88

Enumerations 89

Union types 90

Recursive types 92

Generic data types 95

4.2 Defining dependent data types 102

A first example: classifying vehicles by power source 102

Defining vectors 104

Indexing vectors with bounded numbers using Fin 107

4.3 Type-driven implementation of an interactive data store 110

Representing the store 112

Interactively maintaining state in main 113

Commands: parsing user input 115

Processing commands 118

4.4 Summary 122

5 Interactive programs: input and output processing 123

5.1 Interactive programming with IO 124

Evaluating and executing interactive programs 125

Actions and sequencing: the >>= operator 127

Syntactic sugar for sequencing with do notation 129

5.2 Interactive programs and control flow 132

Producing pure values in interactive definitions 132

Pattern-matching bindings 134

Writing interactive definitions with loops 136

5.3 Reading and validating dependent types 138

Reading a Vect from the console 139

Reading a Vect of unknown length 140

Dependent pairs 141

Validating Vect lengths 143

5.4 Summary 146

6 Programming with first-class types 147

6.1 Type-level functions: calculating types 148

Type synonyms: giving informative names to complex types 149

Type-level functions with pattern matching 150

Using ease expressions in types 153

6.2 Defining functions with variable numbers of arguments 155

An addition function 155

Formatted output: a type-safe print function 157

6.3 Enhancing the interactive data store with schemas 161

Refining the DataStore type 162

Using a record for the DataStore 164

Correcting compilation errors using holes 165

Displaying entries in the store 170

Timing entries according to the schema 171

Updating the schema 175

Sequencing expressions with Maybe using do notation 177

6.4 Summary 181

7 Interfaces: using constrained generic types 182

7.1 Generic comparisons with Eq and Ord 183

Testing for equality with Eq 183

Defining the Eq constraint using interfaces and implementations 185

Default method definitions 189

Constrained implementations 189

Constrained interfaces: defining orderings with Ord 191

7.2 Interfaces defined in the Prelude 194

Converting to String with Show 194

Defining numeric types 195

Converting between types with Cast 198

7.3 Interfaces parameterized by Type -> Type 199

Applying a junction across a structure with Functor 200

Reducing a structure using Foldable 201

Generic do notation using Monad and Applicative 205

7.4 Summary 207

8 Equality: expressing relationships between data 208

8.1 Guaranteeing equivalence of data with equality types 209

Implementing exactLength, first attempt 210

Expressing equality of Nats as a type 211

Testing for equality of Nats 212

Functions as proofs: manipulating equalities 215

Implementing exactLength, second attempt 216

Equality in general: the = type 218

8.2 Equality in practice: types and reasoning 220

Reversing a vector 220

Type checking and evaluation 221

The rewrite construct: rewriting a type using equality 223

Delegating proofs and rewriting to holes 224

Appending vectors, revisited 225

8.3 The empty type and decidability 227

Void: a type with no values 228

Decidability: checking properties with precision 229

DecEq: an interface, for decidable equality 233

8.4 Summary 234

9 Predicates: expressing assumptions and contracts in types 236

9.1 Membership tests: the Elem predicate 237

Removing an element from a Vect 238

The Elem type: guaranteeing a value is in a vector 239

Removing an element from a Vect: types as contracts 241

Auto-implicit argument: automatically constructing proofs 244

Decidable predicates: deciding membership of a vector 245

9.2 Expressing program state in types: a guessing game 250

Representing the game's state 250

A top-level game function 251

A predicate, for validating user input: ValidInput 251

Processing a guess 253

Deciding input validity: checking ValidInput 255

Completing the top-level game implementation 255

9.3 Summary 257

10 Views: extending pattern matching 258

10.1 Defining and using views 259

Matching the last item in a list 260

Building views: covering functions 262

With blocks: syntax fin extended pattern matching 262

Example: reversing a list using a view 264

Example: merge sort 266

10.2 Recursive views: termination and efficiency 271

"Snoc" lists: traversing a list in reverse 271

Recursive views and the with construct 274

Traversing multiple arguments: nested with blocks 275

More, traversals: Data.List.Views 277

10.3 Data abstraction: hiding the structure of data using views 280

Digression: modules in Idris 280

The data since, revisited 282

Traversing the store's contents with a view 284

10.4 Summary 288

Part 3 Idris and the real world 289

11 Streams and processes: working with infinite data 291

11.1 Streams: generating and processing infinite lists 292

Labeling elements in a List 293

Producing an infinite list of numbers 295

Digression: what does it mean for a function to be total? 296

Processing infinite lists 297

The Stream data type 299

An arithmetic quiz using streams of random numbers 301

11.2 Infinite processes: writing interactive total programs 305

Describing infinite processes 306

Executing infinite processes 307

Executing infinite processes as total functions 308

Generating infinite structures using Lazy types 309

Extending do notation for InfIO 311

A total arithmetic quiz 311

11.3 Interactive programs with termination 314

Refining InfIO: introducing termination 314

Domain-specific commands 317

Sequencing Commands with do notation 320

11.4 Summary 323

12 Writing programs with state 324

12.1 Working with mutable state 325

The tree-traversal example 326

Representing mutable state using a pair 328

State, a type for describing stateful operations 329

Tree traversal with State 331

12.2 A custom implementation of State 333

Defining State and runState 333

Defining Functor, Applicative, and Monad implementations for State 335

12.3 A complete program with state: working with records 340

Interactive programs with state: the arithmetic quiz revisited 340

Complex state: defining nested records 343

Updating record field values 344

Updating record fields applying functions 346

Implementing the quiz 346

Running interactive and stateful programs: executing the quiz 348

12.4 Summary 351

13 State machines: verifying protocols in types 352

13.1 State machines: tracking state in types 353

Finite state machines: modeling a door as a type 354

Interactive development of sequences of door operations 356

Infinite states: modeling a vending machine 358

A verified vending machine description 360

13.2 Dependent types in state: implementing a stack 363

Representing stack operations in a state machine 364

Implementing the stack using Vect 366

Using a stack interactively: a stack-based calculator 367

13.3 Summary 371

14 Dependent state machines: handling feedback and errors 373

14.1 Dealing with errors in state transitions 374

Refining the door model representing failure 375

A verified, error-checking, door-protocol description 378

14.2 Security properties in types: modeling an ATM 382

Defining slates for the ATM 383

Defining a type for the ATM 384

Simulating an ATM at the console: executing ATMCmd 387

Refining preconditions using auto-implicits 388

14.3 A verified guessing game: describing rules in types 390

Defining an abstract game state and operation 391

Defining a type for the game state 392

Implementing the game 395

Defining a concrete game stale 397

Running the game: executing GameLoop 399

14.4 Summary 402

15 Type-safe concurrent programming 403

15.1 Primitives for concurrent programming in Idris 404

Defining concurrent processes 406

The Channels library: primitive message passing 407

Problems with channels: type errors and blocking 410

15.2 Defining a type for safe message passing 411

Describing message-pressing processes in a type 412

Making processes total using Inf 415

Guaranteeing responses using a state machine and Inf 418

Generic message-passing processes 422

Defining a module for Process 426

Example 1 List processing 427

Example 2 A word-counting process 429

15.3 Sum man 433

Appendix A Installing Idris and editor modes 435

Appendix B Interactive editing commands 438

Appendix C REPL commands 439

Appendix D Further rending 441

Index 445