Название: Introduction to Dependent Types with Idris: Encoding Program Proofs in Types
Автор: Boro Sitnikovski
Издательство: Apress
Год: 2023
Страниц: 128
Язык: английский
Формат: pdf
Размер: 10.2 MB

Idris is a programming language designed to encourage Type-Driven Development. Dependent types are a concept that allows developers to write proof-carrying code. In Idris, types are first-class constructs in the language. This means types can be passed as arguments to functions, and returned from functions just like any other value, such as numbers, strings, or lists. This book will teach you the mathematical foundations of Idris as well as how to use it to write software and mathematically prove properties.

Idris is a general-purpose functional1 programming language that supports dependent types. The features of Idris are influenced by Haskell, another general-purpose functional programming language. Thus, Idris shares many features with Haskell, especially in the part of syntax and types, where Idris has a more advanced type system. There are several other programming languages that support dependent types; however, I chose Idris for its readable syntax.

The first part of the book serves as an introduction to the language's underlying theories. It starts by reviewing formal systems and mathematical logical systems as foundational building blocks, then gradually builds up to dependent types. Next, you'll learn type theory for dependent types. Following this, you'll explore the Idris programming language and conclude by exploring the depths of formal systems and type checkers by implementing them.

Introduction to Dependent Types with Idris will walk you through simple examples through more advanced techniques, stepping up the difficulty as you gain more knowledge. Every chapter includes a set of exercises based on what it covered to further cement your learning. No specialized knowledge of mathematics is expected beyond the basics, so it is perfect for novices.

This book aims to be accessible to novices who have no prior experience beyond high school mathematics. Thus, this book is designed to be self- contained. No programming experience is assumed. However, having some kind of programming experience with the functional programming paradigm will make things easier to grasp in the beginning. After you finish reading the book, I recommend that you check the “Further Reading” section if you are interested in diving deeper into some of the topics discussed.

What You Will Learn:
Understand Lambda calculus and dependent types
Gain insight into functional programming
Write mathematical proofs with Idris

Who This Book Is For:
Programmers, mathematicians, academics, and anyone else interested learning dependent types and lambda calculus.