第1页 / 共543页
第2页 / 共543页
第3页 / 共543页
第4页 / 共543页
第5页 / 共543页
第6页 / 共543页
第7页 / 共543页
第8页 / 共543页
Type-Driven_Development_with_Idris_v13_MEAP.pdf
Type-Driven Development with Idris MEAP V13
Copyright
Welcome
Brief contents
Chapter 1: Overview
1.1 What is a Type?
1.2 Introducing Type-driven Development
1.2.1 Matrix Arithmetic
1.2.2 An Automated Teller Machine
1.2.3 Concurrent Programming
1.2.4 Type, Define, Refine: The Process of Type-Driven Development
1.2.5 Dependent Types
1.2.6 Introductory Exercises
1.3 Pure Functional Programming
1.3.1 Purity and Referential Transparency
1.3.2 Side Effecting Programs
1.3.3 Partial and Total Functions
1.4 A quick tour of Idris
1.4.1 The interactive environment
1.4.2 Checking Types
1.4.3 Compiling and Running Idris Programs
1.4.4 Incomplete Definitions: Working with Holes
1.4.5 Types as a First-class Construct
1.5 Summary
Chapter 2: Getting started with Idris
2.1 Basic types
2.1.1 Numeric types and values
2.1.2 Type conversions using cast
2.1.3 Characters and strings
2.1.4 Booleans
2.2 Functions: the building blocks of Idris programs
2.2.1 Function types and definitions
2.2.2 Partially applying functions
2.2.3 Writing generic functions: variables in types
2.2.4 Writing generic functions with constrained types
2.2.5 Higher-order function types
2.2.6 Anonymous functions
2.2.7 Local definitions: let and where
2.3 Composite types
2.3.1 Tuples
2.3.2 Lists
2.3.3 Functions with lists
2.4 A complete Idris program
2.4.1 Whitespace significance: the layout rule
2.4.2 Documentation comments
2.4.3 Interactive programs
2.5 Exercises
2.6 Summary
Chapter 3: Interactive development with types
3.1 Interactive editing in Atom
3.1.1 Interactive command summary
3.1.2 Defining functions by pattern matching
3.1.3 Data types and patterns
3.2 Adding precision to types: working with vectors
3.2.1 Refining the type of allLengths
3.2.2 Type-directed search: automatic refining
3.2.3 Type, define, refine: sorting a vector
3.2.4 Exercises
3.3 Example: type-driven development of matrix functions
3.3.1 Matrix operations and their types
3.3.2 Transposing a matrix
3.3.3 Exercises
3.4 Implicit arguments: type-level variables
3.4.1 The need for implicit arguments
3.4.2 Bound and unbound implicits
3.4.3 Using implicit arguments in functions
3.5 Summary
Chapter 4: User-defined data types
4.1 Defining data types
4.1.1 Enumerations
4.1.2 Union types
4.1.3 Recursive types
4.1.4 Generic data types
4.1.5 Exercises
4.2 Defining dependent data types
4.2.1 A first example: classifying vehicles by power source
4.2.2 Defining vectors
4.2.3 Indexing vectors with bounded numbers using Fin
4.2.4 Exercises
4.3 Type-driven implementation of an interactive data store
4.3.1 Representing the store
4.3.2 Interactively maintaining state in main
4.3.3 Commands: parsing user input
4.3.4 Processing commands
4.3.5 Exercises
4.4 Summary
Chapter 5: Interactive programs: input and output processing
5.1 Interactive programming with IO
5.1.1 Evaluating and executing interactive programs
5.1.2 Actions and sequencing: the >>= operator
5.1.3 Syntactic sugar for sequencing with do notation
5.1.4 Exercises
5.2 Interactive programs and control flow
5.2.1 Producing pure values in interactive definitions
5.2.2 Pattern-matching bindings
5.2.3 Writing interactive definitions with loops
5.2.4 Exercises
5.3 Reading and validating dependent types
5.3.1 Reading a Vect from the console
5.3.2 Reading a Vect of unknown length
5.3.3 Dependent pairs
5.3.4 Validating Vect lengths
5.3.5 Exercises
5.4 Summary
Chapter 6: Programming with first-class types
6.1 Type-level functions: calculating types
6.1.1 Type synonyms: giving informative names to complex types
6.1.2 Type-level functions with pattern matching
6.1.3 Using case expressions in types
6.2 Defining functions with variable numbers of arguments
6.2.1 An addition function
6.2.2 Formatted output: a type-safe printf function
6.2.3 Exercises
6.3 Enhancing the interactive data store with schemas
6.3.1 Refining the DataStore type
6.3.2 Using a record for the DataStore
6.3.3 Correcting compilation errors using holes
6.3.4 Displaying entries in the store
6.3.5 Parsing entries according to the schema
6.3.6 Updating the schema
6.3.7 Sequencing expressions with Maybe using do notation
6.3.8 Exercises
6.4 Summary
Chapter 7: Interfaces: using constrained generic types
7.1 Generic comparisons with Eq and Ord
7.1.1 Testing for equality with Eq
7.1.2 Defining the Eq constraint using interfaces and implementations
7.1.3 Default method definitions
7.1.4 Constrained implementations
7.1.5 Constrained interfaces: defining orderings with Ord
7.1.6 Exercises
7.2 Interfaces defined in the Prelude
7.2.1 Converting to String with Show
7.2.2 Defining numeric types
7.2.3 Converting between types with Cast
7.2.4 Exercises
7.3 Interfaces parameterized by Type -> Type
7.3.1 Applying a function across a structure with Functor
7.3.2 Reducing a structure using Foldable
7.3.3 Generic do notation using Monad and Applicative
7.3.4 Exercises
7.4 Summary
Chapter 8: Equality: expressing relationships between data
8.1 Guaranteeing equivalence of data with equality types
8.1.1 Implementing exactLength, first attempt
8.1.2 Expressing equality of Nats as a type
8.1.3 Testing for equality of Nats
8.1.4 Functions as proofs: manipulating equalities
8.1.5 Implementing exactLength, second attempt
8.1.6 Equality in general: the = type
8.1.7 Exercises
8.2 Equality in practice: types and reasoning
8.2.1 Reversing a vector, first attempt
8.2.2 Type checking and evaluation
8.2.3 The rewrite construct: rewriting a type using equality
8.2.4 Delegating proofs and rewriting to holes
8.2.5 Appending vectors, revisited
8.2.6 Exercises
8.3 The empty type and decidability
8.3.1 Void: a type with no values
8.3.2 Decidability: checking properties with precision
8.3.3 DecEq: an interface for decidable equality
8.3.4 Exercises
8.4 Summary
Chapter 9: Predicates: expressing assumptions and contracts in types
9.1 Membership tests: the Elem predicate
9.1.1 Removing an element from a Vect, first attempt
9.1.2 The Elem type: guaranteeing a value is in a vector
9.1.3 Removing an element from a Vect: types as contracts
9.1.4 Auto-implicit arguments: automatically constructing proofs
9.1.5 Decidable predicates: deciding membership of a vector
9.1.6 Exercises
9.2 Expressing program state in types: a guessing game
9.2.1 Representing the game’s state
9.2.2 A top-level game function
9.2.3 A predicate for validating user input: ValidInput
9.2.4 Processing a guess
9.2.5 Deciding input validity: checking ValidInput
9.2.6 Completing the top-level game implementation
9.3 Summary
Chapter 10: Views: Extending Pattern Matching
10.1 Defining and Using Views
10.1.1 Matching the Last Item in a List
10.1.2 Building Views: Covering Functions
10.1.3 with blocks: Syntax for Extended Pattern Matching
10.1.4 Example: Reversing a List using a View
10.1.5 Example: Merge Sort
10.1.6 Exercises
10.2 Recursive Views: Termination and Efficiency
10.2.1 "Snoc" Lists: Traversing a List in Reverse
10.2.2 Recursive Views and the with Construct
10.2.3 Traversing Multiple Arguments: Nested with Blocks
10.2.4 More Traversals: Data.List.Views
10.2.5 Exercises
10.3 Data Abstraction: Hiding the Structure of Data Using Views
10.3.1 Digression: Modules in Idris
10.3.2 The Data Store, Revisited
10.3.3 Traversing the Store's Contents with a View
10.3.4 Exercises
10.4 Summary
Chapter 11: Streams and Processes: Working with Infinite Data
11.1 Streams: Generating and Processing Infinite Lists
11.1.1 First Example: Labelling Elements in a List
11.1.2 Producing an Infinite List of Numbers
11.1.3 Digression: What Does it Mean for a Function to be Total?
11.1.4 Processing Infinite Lists
11.1.5 The Stream data type
11.1.6 An Arithmetic Quiz Using Streams of Random Numbers
11.1.7 Exercises
11.2 Infinite Processes: Writing Interactive Total Programs
11.2.1 Describing Infinite Processes
11.2.2 Executing Infinite Processes
11.2.3 Executing Infinite Processes as Total Functions
11.2.4 Generating Infinite Structures using Lazy Types
11.2.5 Extending do-notation for InfIO
11.2.6 A Total Arithmetic Quiz
11.2.7 Exercise
11.3 Interactive Programs with Termination
11.3.1 Refining InfIO: Introducing Termination
11.3.2 Domain Specific Commands
11.3.3 Sequencing Commands with do-notation
11.3.4 Exercises
11.4 Summary
Chapter 12: Writing Programs with State
12.1 Working with Mutable State
12.1.1 Running Example: Tree Traversal
12.1.2 Representing Mutable State using a Pair
12.1.3 State, a Type for Describing Stateful Operations
12.1.4 Tree Traversal with State
12.1.5 Exercises
12.2 A Custom Implementation of State
12.2.1 Defining State and runState
12.2.2 Defining Functor, Applicative
and Monad Implementations for State
12.3 A Complete Program with State: Working with Records
12.3.1 Interactive Programs with State: The Arithmetic Quiz Revisited
12.3.2 Complex State: Defining Nested Records
12.3.3 Updating Record Field Values
12.3.4 Updating Record Fields by Applying Functions
12.3.5 Implementing the Quiz
12.3.6 Running Interactive and Stateful Programs: Executing the Quiz
12.3.7 Exercises
12.4 Summary
Chapter 13: State Machines: Verifying Protocols in Types
13.1 State Machines: Tracking State in Types
13.1.1 Finite State Machines: Modelling a Door
as a Type
13.1.2 Interactive Development of Sequences of Door Operations
13.1.3 Infinite States: Modelling a Vending Machine
13.1.4 A Verified Vending Machine Description
13.1.5 Exercises
13.2 Dependent Types in State: Implementing a Stack
13.2.1 Representing Stack Operations in a State Machine
13.2.2 Implementing the Stack using Vect
13.2.3 Using a Stack Interactively: A Stack-based Calculator
13.2.4 Exercises
13.3 Summary
Chapter 14: Dependent State Machines: Handling Feedback and Errors
14.1 Dealing with Errors in State Transitions
14.1.1 Refining the Door Model: Representing Failure
14.1.2 A Verified, Error Checking, Door Protocol Description
14.2 Security Properties in Types: Modelling an ATM
14.2.1 Defining States for the ATM
14.2.2 Defining a Type for the ATM
14.2.3 Simulating an ATM at the Console: Executing ATMCmd
14.2.4 Refining Preconditions using auto-implicits
14.2.5 Exercises
14.3 A Verified Guessing Game: Describing Rules in Types
14.3.1 Defining an Abstract Game State and Operations
14.3.2 Defining a Type for the Game State
14.3.3 Implementing the Game
14.3.4 Defining a Concrete Game State
14.3.5 Running the Game: Executing GameLoop
14.4 Summary
Chapter 15: Type-safe Concurrent Programming
15.1 Primitives for Concurrent Programming in Idris
15.1.1 Defining Concurrent Processes
15.1.2 The Channels Library: Primitive Message Passing
15.1.3 Problems with Channels: Type Errors and Blocking
15.2 Defining a Type for Safe Message Passing
15.2.1 Describing Message Passing Processes in a Type
15.2.2 Making Processes Total using Inf
15.2.3 Guaranteeing Responses using a State Machine and Inf
15.2.4 Generic Message Passing Processes
15.2.5 Defining a module for Process
15.2.6 Example 1: List Processing
15.2.7 Example 2: A Word Counting Process
15.3 Summary
Appendix A: Installing Idris and Editor Modes
A.1 The Idris Compiler and Environment
A.1.1 OS X
A.1.2 Windows
A.1.3 Unix-like platforms, installing from source
A.2 Editor Modes
A.2.1 Atom
A.2.2 Other Editors
Appendix B: Interactive Editing Commands
Appendix C: REPL Commands
Version 13
MEAP Edition
Manning Early Access Program
Type-Driven Development with Idris
Copyright 2016 Manning Publications
For more information on this and other Manning titles go to
www.manning.com
Licensed to UNKNOWN µ
©Manning Publications Co. We welcome reader comments about anything in the manuscript - other than typos and other simple mistakes. These will be cleaned up during production of the book by copyeditors and proofreaders. https://forums.manning.com/forums/type-driven-development-with-idris
Welcome
Hello, and welcome to the MEAP for Type Driven Development with Idris. This is an
exciting stage not only in the development of this book, but in the development of the Idris
programming language itself, and I'm very pleased you've decided to buy this MEAP and
join me in this project. Thanks!
This book is about making types work for you. Types are often seen as a tool for
checking for errors, with the programmer writing a complete program first and using the
type checker to detect errors. In type-driven development, we use types as a tool for
constructing programs, using the type checker as our assistant, guiding us to a complete and
working program.
I've been working with Idris and contributing to its development for several years now,
and in this book I aim to explain the various type-driven programming techniques that I and
others in the community have discovered and developed over the last few years.
To get the most out of this book, ideally you'll already be familiar with the basic ideas of
functional programming, and have a good working knowledge of data structures such as lists
and trees. If you understand concepts such as closures, recursive types and functions, higher
order functions and programming with immutable data, then you should get on fine. No
knowledge of any specific language is assumed.
At this stage, we're releasing the first two Chapters, which will get you up to speed with
the main ideas behind type-driven development, and with the Idris language and
environment. You'll learn about what it means to be a type, and how we treat a type as a
plan for a program. You'll also learn about the built-in types and functions provided by Idris,
and how to structure these into complete programs. If you're already familiar with a
functional programming language, these chapters will get you up to speed on the basics of
Idris before we dive more deeply into dependent types and type-driven development in the
later chapters.
As you work through these early chapters, I'd love to hear from you! Your feedback is
vital to making this book the best it can possibly be. Please use the Author Online forum to
let me know if anything needs more explanation, if you think you've spotted a mistake, or
even just to let me know how you're getting on.
Have fun!
—Edwin Brady
Licensed to UNKNOWN µ
©Manning Publications Co. We welcome reader comments about anything in the manuscript - other than typos and other simple mistakes. These will be cleaned up during production of the book by copyeditors and proofreaders. https://forums.manning.com/forums/type-driven-development-with-idris
brief contents
PART 1: INTRODUCTION
1 Overview
2 Getting Started with Idris
PART 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
11 Streams and Processes : Working with Infinite Data
PART 3: IDRIS AND THE REAL WORLD
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
APPENDIXES
A Installing Idris & Editor Types
B Interactive Editing Commands
C REPL Commands
D The Packaging System
Licensed to UNKNOWN µ
©Manning Publications Co. We welcome reader comments about anything in the manuscript - other than typos and other simple mistakes. These will be cleaned up during production of the book by copyeditors and proofreaders. https://forums.manning.com/forums/type-driven-development-with-idris
1
Overview
This chapter covers
Introducing Type-driven Development
The essence of pure functional programming
Getting started with Idris
This book teaches a new approach to building robust software,
,
Type-driven Development
using the Idris programming language. Traditionally, types are seen as a tool for
checking for errors, with the programmer writing a complete program first and using
either the compiler or run-time system to detect type errors. In Type-driven
Development, we use types as a tool for constructing programs. We put the
first,
treating it as a
for a program, and use the compiler and type checker as our assistant,
guiding us to a complete and working program which satisfies the type. The more
expressive a type we give up front, the more confidence we have that the resulting
program will be correct.
plan
type
NOTE
Types and tests
The name "Type-driven Development" suggests an analogy with
Test-driven Development. There is a similarity, in that writing tests first
helps establish a program's purpose and whether it satisfies some basic
requirements. The difference is that unlike tests, which can usually only
be used to show the
of errors, types (used appropriately) can
show their
presence
absence
.
Even so, while types
reduce
the need for tests, they rarely eliminate it
entirely.
Idris is a relatively young programming language, designed from the beginning to
support Type-driven Development. A prototype implementation first appeared in 2008,
Licensed to UNKNOWN µ
©Manning Publications Co. We welcome reader comments about anything in the manuscript - other than typos and other simple mistakes. These will be cleaned up during production of the book by copyeditors and proofreaders. https://forums.manning.com/forums/type-driven-development-with-idris1
with development of the current implementation beginning in 2011. It builds on decades
of research into the theoretical and practical foundations of programming languages and
type systems.
In Idris, types are a
language construct. Types can be manipulated, used,
passed as arguments to functions and returned from functions just like any other value
such as numbers, strings, or lists. This is a simple but powerful idea, which allows:
first-class
relationships to be expressed between values, for example that two lists have the same
length
assumptions to be made explicit and checkable by the compiler, for example if we
assume that a list is non-empty then Idris can ensure this assumption always holds before
the program is run
if desired, program behaviour to be formally stated and proven correct
In this chapter, I'll introduce the Idris programming language and give a brief tour of
its features and environment. I'll also give an overview of Type-driven Development,
discussing why types matter in programming languages, and how they can be used to
guide software development. But first, it is important to understand exactly what we
mean when we talk about "types".
1.1 What is a Type?
We are taught from an early age to recognise and distinguish
of objects. As a young
child, you may have had a "shape sorter" toy. This consists of a box with various shaped
holes in the top, as illustrated in Figure 1.1, and some shapes which fit through the holes.
Sometimes, they are equipped with a small plastic hammer. The idea is to fit each shape
(think of this as a "value") into the appropriate hole (think of this as the "type") possibly
with coercion from the hammer.
types
Figure 1.1 The top of a "shape sorter" toy.
The shapes correspond the "types" of
objects which will fit through the holes.
Licensed to UNKNOWN µ
©Manning Publications Co. We welcome reader comments about anything in the manuscript - other than typos and other simple mistakes. These will be cleaned up during production of the book by copyeditors and proofreaders. https://forums.manning.com/forums/type-driven-development-with-idris2
and
In programming, types are a means of classifying values. For example, the values
, 94
could respectively be classified as an integer, a string and a
"thing"
list of integers. Just as we can't put a square shape in a circular hole in the shape sorter,
we can't use a string like
in a part of a program where we need an integer.
[1,2,3,4,5]
"thing"
All modern programming languages classify values by type, although they differ
enormously in when and how they do so (for example whether they are checked statically
at compile-time or dynamically at run-time, whether conversions between types are
automatic or not, and so on.) Types serve several important roles:
, types describe how bit patterns in memory are to be interpreted
, types help ensure that bit patterns are interpreted
1.
2.
3.
machine
compiler or interpreter
For a
For a
consistently when a program runs
For a
supporting interactive editing environments
programmer
, types help name and organise concepts, aiding documentation and
,
,
From our point of view in this book, the most important purpose of types is the third.
Types help the programmer by allowing the naming and organisation of concepts (e.g.
), explicit documentation of the purpose of
Square Circle Triangle
variables, functions and programs, and by driving code completion in an interactive
editing environment. All modern statically typed languages support this to some extent,
but as we will see, the expressivity of the Idris type system leads to powerful automatic
code generation.
Hexagon
and
1.2 Introducing Type-driven Development
Type-driven Development is a style of programming in which we write types first and
use those types to guide the definition of functions. The overall process is to write the
necessary data types, then, for each function:
1.
2.
3.
Write the input and output types
Define the function, using the structure of the input types to guide the implementation
Refine and edit the type and function definition as necessary
In Type-driven Development, instead of thinking of types in terms of
, with
the type checker criticising us when we make a mistake, we think of types as being a plan
, with the type checker acting as our guide leading us to a working, robust program.
Starting with a type and an empty function body, we gradually add details to the
definition until it's complete, regularly using the compiler to check that the program so
far satisfies the type. Idris, as we'll soon see, strongly encourages this style of
programming by allowing
function definitions to be checked, and by
providing an expressive language for describing types.
incomplete
checking
Licensed to UNKNOWN µ
©Manning Publications Co. We welcome reader comments about anything in the manuscript - other than typos and other simple mistakes. These will be cleaned up during production of the book by copyeditors and proofreaders. https://forums.manning.com/forums/type-driven-development-with-idris3
NOTE
Types as Models
When we write a program, we typically have a conceptual
in our
head (or, if we're being disciplined, even on paper) of how it's supposed
to work, how the components interact and how the data is organised. This
model is likely to be quite vague at first, and become more precise as the
program evolves and our understanding of the problem develops.
model
Types allow us to make these models explicit in code, and ensure that
implementation
of a program matches the model in our head. Idris
our
has an expressive type system which allows us to describe models as
precisely as we need, and to refine the model at the same time as
developing the implementation.
To illustrate further, in this section I'll describe some examples of how we can use
types to describe in detail what a program is intended to do: matrix arithmetic; modelling
an Automated Teller Machine (ATM); and writing concurrent programs. Then, I'll
summarise the process of Type-driven Development and introduce the concept of
dependent types
, which allow us to express detailed properties of our programs.
1.2.1 Matrix Arithmetic
matrix
is a rectangular grid of numbers, arranged in rows and columns. They have
A
several scientific applications, and in programming in particular they have applications in
cryptography, 3D graphics. machine learning and data analytics. The following, for
example, is a 3x4 matrix:
We can implement various arithmetic operations on matrices, such as addition and
multiplication. To
add
two matrices, we add the corresponding elements. For example:
When programming with matrices, if we begin by defining a
data type, then
addition requires two inputs of type
. But,
since adding matrices involves adding corresponding elements of the inputs, what
happens if the two inputs have different dimensions? For example:
Matrix
Matrix
and gives an output of type
Matrix
Licensed to UNKNOWN µ
©Manning Publications Co. We welcome reader comments about anything in the manuscript - other than typos and other simple mistakes. These will be cleaned up during production of the book by copyeditors and proofreaders. https://forums.manning.com/forums/type-driven-development-with-idris4
相关推荐
2023年江西萍乡中考道德与法治真题及答案.doc
2012年重庆南川中考生物真题及答案.doc
2013年江西师范大学地理学综合及文艺理论基础考研真题.doc
2020年四川甘孜小升初语文真题及答案I卷.doc
2020年注册岩土工程师专业基础考试真题及答案.doc
2023-2024学年福建省厦门市九年级上学期数学月考试题及答案.doc
2021-2022学年辽宁省沈阳市大东区九年级上学期语文期末试题及答案.doc
2022-2023学年北京东城区初三第一学期物理期末试卷及答案.doc
2018上半年江西教师资格初中地理学科知识与教学能力真题及答案.doc
2012年河北国家公务员申论考试真题及答案-省级.doc
2020-2021学年江苏省扬州市江都区邵樊片九年级上学期数学第一次质量检测试题及答案.doc
2022下半年黑龙江教师资格证中学综合素质真题及答案.doc
