logo资料库

Type-Driven Development with Idris.pdf

发布时间：2022-06-14 发布人：admin 分类：说明书 资料大小：10.53M 资料格式：pdf 举报 版权申诉
第1页 / 共484页
第2页 / 共484页
第3页 / 共484页
第4页 / 共484页
第5页 / 共484页
第6页 / 共484页
第7页 / 共484页
第8页 / 共484页
资料共484页，剩余部分请下载后查看
    Type-Driven Development with Idris
    brief contents
    contents
    preface
    acknowledgments
    about this book
    Who should read this book
    Roadmap
    Code conventions and downloads
    Author Online
    Other online resources
    about the author
    about the cover illustration
    Part 1 Introduction
    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.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 First-class types
    1.5 Summary
    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 Summary
    Part 2 Core Idris
    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.3 Example: type-driven development of matrix functions
    3.3.1 Matrix operations and their types
    3.3.2 Transposing a matrix
    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
    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.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.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.4 Summary
    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.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.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.4 Summary
    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.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.4 Summary
    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.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.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.4 Summary
    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.2 Equality in practice: types and reasoning
    8.2.1 Reversing a vector
    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.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.4 Summary
    9 Predicates: expressing assumptions and contracts in types
    9.1 Membership tests: the Elem predicate
    9.1.1 Removing an element from a Vect
    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.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
    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.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.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.4 Summary
    Part 3 Idris and the real world
    11 Streams and processes: working with infinite data
    11.1 Streams: generating and processing infinite lists
    11.1.1 Labeling 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.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.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.4 Summary
    12 Writing programs with state
    12.1 Working with mutable state
    12.1.1 The tree-traversal example
    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.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.4 Summary
    13 State machines: verifying protocols in types
    13.1 State machines: tracking state in types
    13.1.1 Finite state machines: modeling a door as a type
    13.1.2 Interactive development of sequences of door operations
    13.1.3 Infinite states: modeling a vending machine
    13.1.4 A verified vending machine description
    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.3 Summary
    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: modeling 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.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
    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
    The Idris compiler and environment
    Mac OS
    Windows
    Unix-like platforms, installing from source
    Editor modes
    Atom
    Other editors
    appendix B Interactive editing commands
    appendix C REPL commands
    appendix D Further reading
    Functional programming in Haskell
    Other languages and tools with expressive type systems
    Theoretical foundations
    Total functional programming
    Types for concurrency
    index
    Symbols
    A
    B
    C
    D
    E
    F
    G
    H
    I
    J
    L
    M
    N
    O
    P
    Q
    R
    S
    T
    U
    V
    W
    Z
    Edwin Brady M A N N I N G
    The Idris read-eval-print loop (REPL) provides several commands. The most common commands, listed below, are introduced over the course of this book. Command Arguments Description None Displays the result of evaluating the expression. The variable it contains the result of the most recent evaluation. :t :total :doc :let :exec :c :r :l Displays the type of the expression. Displays whether the function with the given name is total. Displays documentation for name. Adds a new definition. Compiles and executes the expression. If none is given, compiles and executes main. Compiles to an executable with the entry point main. None Reloads the current module. Loads a new file. :module Imports an extra module for use at the REPL. :printdef :apropos :search :browse Displays the definition of name. Searches function names, types, and documentation for the given word. Searches for functions with the given type. Displays the names and types defined in the given namespace. :q None Exits the REPL.
    Type-Driven Development with Idris
    Type-Driven Development with Idris EDWIN BRADY M A N N I N G SHELTER ISLAND
    For online information and ordering of this and other Manning books, please visit www.manning.com. The publisher offers discounts on this book when ordered in quantity. For more information, please contact Special Sales Department Manning Publications Co. 20 Baldwin Road PO Box 761 Shelter Island, NY 11964 Email: orders@manning.com ©2017 by Manning Publications Co. All rights reserved. No part of this publication may be reproduced, stored in a retrieval system, or transmitted, in any form or by means electronic, mechanical, photocopying, or otherwise, without prior written permission of the publisher. Many of the designations used by manufacturers and sellers to distinguish their products are claimed as trademarks. Where those designations appear in the book, and Manning Publications was aware of a trademark claim, the designations have been printed in initial caps or all caps. Recognizing the importance of preserving what has been written, it is Manning’s policy to have the books we publish printed on acid-free paper, and we exert our best efforts to that end. Recognizing also our responsibility to conserve the resources of our planet, Manning books are printed on paper that is at least 15 percent recycled and processed without the use of elemental chlorine. Manning Publications Co. 20 Baldwin Road PO Box 761 Shelter Island, NY 11964 Development editor: Dan Maharry Review editor: Aleksandar Dragosavljevic´ Technical development editor: Andrew Gibson Project editor: Kevin Sullivan Copyeditor: Andy Carroll Proofreader: Katie Tennant Technical proofreaders: Arnaud Bailly, Nicolas Biri Typesetter: Dottie Marsico Cover designer: Marija Tudor ISBN 9781617293023 Printed in the United States of America 1 2 3 4 5 6 7 8 9 10 – EBM – 22 21 20 19 18 17
    brief contents PART 1 INTRODUCTION................................................................ 1 1 ■ Overview 3 2 ■ Getting started with Idris 25 PART 2 CORE IDRIS .................................................................... 53 Interactive development with types 55 Interactive programs: input and output processing 123 3 ■ 4 ■ User-defined data types 87 5 ■ 6 ■ Programming with first-class types 147 7 ■ 8 ■ Equality: expressing relationships between data 208 9 ■ Predicates: expressing assumptions and contracts in types 236 10 ■ Views: extending pattern matching 258 Interfaces: using constrained generic types 182 PART 3 IDRIS AND THE REAL WORLD ......................................... 289 11 ■ Streams and processes: working with infinite data 291 12 ■ Writing programs with state 324 13 ■ State machines: verifying protocols in types 352 14 ■ Dependent state machines: handling feedback and errors 373 15 ■ Type-safe concurrent programming 403 v
    分享到：
    赞 收藏

    相关推荐

    资料库

    开发技术

    共收录19306份资料，累计14个分类，关注成员有19位，主要包括：Actionscript,Javascript,PHP,VB,Perl,Delphi,Python,C#,C,Java,C++,Web开发,硬件开发,其它

    热门标签

    Actionscript Javascript PHP VB Perl Delphi Python C# C Java C++ Web开发 硬件开发 其它

    最新资料