Edwin Brady – författare

DESCRIPTION

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 typedriven

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.

 

Type-Driven Development with Idris, 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. This

book teaches readers using Idris, a language designed from the very

beginning to support type-driven development. Readers learn how to

manipulate types just like any other construct (numbers, strings, lists,

etc.). This book teaches 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, readers will be able to develop robust and verified software

in Idris and apply type-driven development methods to programming

in other languages.

 

KEY FEATURES

• Written by the creator of Idris

• Improve performance and accuracy of programs

• Teaches Idris, a new type-driven development language

• Hands-on code examples

• Build real-world software

 

AUDIENCE

Written for programmers with knowledge of basic functional programming

concepts.

 

ABOUT THE TECHNOLOGY

Type-driven development lets you write extensible code, create simple

specifications very early in development, and easily create mock

implementation for testing. In type-driven development, types become your

tools for constructing programs and, used appropriately, can show the

absence of errors.

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 Contents

PART 1 - INTRODUCTION

OverviewGetting started with Idris

PART 2 - CORE IDRIS

Interactive 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 matching

PART 3 - IDRIS AND THE REAL WORLD

Streams and processes: working with infinite dataWriting programs with stateState machines: verifying protocols in typesDependent state machines: handling feedback and errorsType-safe concurrent programming

This book constitutes the refereed proceedings of the 12th International Conference on Intelligent Computer Mathematics, CICM 2019, held in Prague, Czech Republic, in July 2019. The 19 full papers presented were carefully reviewed and selected from a total of 41 submissions. The papers focus on digital and computational solutions which are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value.