The Idris 2 Programming Langauge

Core Language Features

• Introduction
  • About The Idris Programming Language
  • Using the REPL
  • A First Idris Program
  • The Shape of an Idris Definition
  • Where to Get Help
  • Conclusion
• Introduction To Functions
  • Functions With More Than One Argument
  • Function Composition
  • Higher Order Functions
  • Currying
  • Anonymous Functions
  • Operators
  • Introductory Function Exercises
  • Conclusion
• Algebraic Data Types
  • Enumerations
  • Enumeration Exercises
  • Sum Types
  • Sum Type Exercises
  • Records
  • Record Exercises
  • Generic Data Types
  • Generic Data Type Exercises
  • Alternative Syntax for Data Definitions
  • Conclusion
• Interfaces
  • Interface Basics
  • Exercises
  • More About Interfaces
  • Exercises
  • Interfaces in the Prelude
  • Exercises
  • Conclusion
• Functions Part 2
  • Let Bindings and Local Definitions
  • Exercises
  • The Truth about Function Arguments
  • Programming with Holes
  • Conclusion
• Dependent Types
  • Length-Indexed Lists
  • Exercises
  • Fin: Safe Indexing Into Vectors
  • Exercises
  • Compile-Time Computations
  • Exercises
  • Conclusion
• IO: Programming with Side Effects
  • Pure Side Effects?
  • Exercises
  • Do Blocks, Desugared
  • Exercises
  • Working With Files
  • Exercises
  • How IO is Implemented
  • Conclusion
• Functor and Friends
  • Functor
  • Exercises
  • Applicative
  • Exercises
  • Monad
  • Exercises
  • Background and further Reading
  • Conclusion
• Recursion and Folds
  • Recursion
  • Exercises
  • Notes on Totality Checking
  • Exercises
  • Interface Foldable
  • Exercises
  • Conclusion
• Effectful Traversals
  • Reading CSV Tables
  • Exercises
  • Programming with State
  • Exercises
  • The Power of Composition
  • Exercises
  • Conclusion
• Sigma Types
  • Dependent Pairs
  • Exercises
  • Use Case: Nucleic Acids
  • Exercises
  • Use Case: CSV Files with a Schema
  • Exercises
  • Conclusion
• Propositional Equality
  • Equality as a Type
  • Exercises
  • Programs as Proofs
  • Exercises
  • Into the Void
  • Exercises
  • Rewrite Rules
  • Exercises
  • Conclusion
• Predicates and Proof Search
  • Preconditions
  • Exercises
  • Contracts between Values
  • Exercises
  • Use Case: Flexible Error Handling
  • Exercises
  • The Truth about Interfaces
  • Conclusion
• Primitives
  • How Primitives are Implemented
  • Working with Strings
  • Exercises
  • Integers
  • Exercises
  • Refined Primitives
  • Exercises

---

Appendices

• Getting Started with pack and Idris 2
• Interactive Editing in Neovim
• Structuring Idris Projects
• A Deep Dive into Quantitative Type Theory

---

Exercise Solutions

• Introductory Function Exercises
• Algebraic Data Types
• Interfaces
• Functions Part 2
• Dependent Types
• IO: Programming with Side Effects
• Functor and Friends
• Recursion and Folds
• Effectful Traversals
• Sigma Types
• Propositional Equality
• Predicates and Proof Search
• Primitives