Dependent types are a concept that allows developers to write proof-carrying code. Idris is a programming language that supports dependent types. This book will teach you the mathematical foundations of Idris as well as how to use it to write software and mathematically prove properties.
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.
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.
Author(s): Boro Sitnikovski
Edition: 1
Publisher: Apress
Year: 2023
Language: English
Commentary: Publisher's PDF
Pages: 128
City: New York, NY
Tags: Proofs; Mathematical Logic; Trees; Type-Driven Development; Lambda Calculus; Idris; Dependent Types; Type Theory
Table of Contents
About the Author
About the Technical Reviewers
Acknowledgments
Preface
Introduction
Chapter 1: Formal Systems
1.1. MU Puzzle Example
Chapter 2: Classical Mathematical Logic
2.1. Hierarchy of Mathematical Logic and Definitions
2.1.1. Propositional Logic
2.1.2. First-order Logic
2.1.3. Higher-order Logic
2.2. Set Theory Abstractions
2.3. Substitution and Mathematical Proofs
2.3.1. Proofs by Truth Tables
2.3.2. Three-column Proofs
2.3.3. Formal Proofs
2.3.4. Mathematical Induction
Chapter 3: Type Theory
3.1. Lambda Calculus
3.1.1. Term Reduction
3.2. Lambda Calculus with Types
3.3. Dependent Types
3.4. Intuitionistic Theory of Types
3.4.1. Intuitionistic Logic
Chapter 4: Programming in Idris
4.1. Basic Syntax and Definitions
4.1.1. Defining Functions
4.1.2. Defining and Inferring Types
4.1.3. Anonymous Lambda Functions
4.1.4. Recursive Functions
4.1.5. Recursive Data Types
4.1.6. Total and Partial Functions
4.1.7. Higher-Order Functions
4.1.8. Dependent Types
4.1.9. Implicit Parameters
4.1.10. Pattern-Matching Expressions
4.1.11. Interfaces and Implementations
4.2. Curry-Howard Isomorphism
4.3. Quantitative Type Theory
Chapter 5: Proving in Idris
5.1. Weekdays
5.1.1. First Proof (Auto-Inference)
5.1.2. Second Proof (Rewrite)
5.1.3. Third Proof (Impossible)
5.2. Natural Numbers
5.2.1. First Proof (Auto-Inference and Existence)
5.2.2. Second Proof (Introduction of a New Given)
5.2.3. Third Proof (Induction)
5.2.4. Ordering
5.2.5. Safe Division
5.2.6. Maximum of Two Numbers
5.2.7. List of Even Naturals
5.2.8. Partial Orders
5.3. Computations as Types
5.3.1. Same Elements in a List (Vector)
5.3.2. Evenness of Numbers
5.4. Trees
5.4.1. Depth
5.4.2. Map and Size
5.4.3. Length of Mapped Trees
Capture.PNG
