Functional Programming in Idris 2

中文翻译, 日本語訳

The goal of this project is quickly explained: To become a more or less comprehensive guide to the Idris programming language, with a lot of introductory material targeted at newcomers to functional programming.

The content will be organized in several parts, with the part about the core language features being the main guide to functional programming in Idris. Every part consists of several chapters, each trying to cover in depth a certain aspect of the Idris programming language and its core libraries. Most chapters come with (sometimes lots of) exercises, with solutions available in directory src/Solutions.

Right now, even the part about core language features is not yet finished, but is being actively developed and tried on several of my own students, some of which are completely new to functional programming.

Table of Contents

Part 1: Core Language Features

This part tries to give a solid introduction to the Idris programming language. If you are new to functional programming, make sure to follow these chapters in order and solve all the exercises.

If you already used other pure functional programming languages like Haskell, you might go through the introductory material (Functions Part 1, Algebraic Data Types, and Interfaces) pretty quickly, as most of this stuff will already be familiar to you.

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

Part 2: Appendices

The appendices can be used as references for the topics at hand. I plan to eventually have a concise reference on Idris syntax, typical error messages, the module system, interactive editing and possibly others.

1. Getting Started with pack and Idris2
2. Interactive Editing in Neovim
3. Structuring Idris Projects
4. A Deep Dive into Quantitative Type Theory

Prerequisites

At the moment, this project is being actively developed and evolved against the main branch of the Idris 2 repository. It is being tested nightly on GitHub and built against the latest version of pack's package collection.

In order to follow along with this tutorial, it is strongly suggested to install Idris via the pack package manager as described here.