- Author
- The Idris Community
- Published
- Undated; copyright 2020-2023
- Kind
- Official documentation page, a chapter-by-chapter list of code changes
- Original
- idris2.readthedocs.io/en/latest/typedd/typedd.html
- Subject
- Programming languages and types
What it is
The Idris Community wrote this page for the Idris 2 documentation. It covers Chapters 1 to 14 of the book Type-Driven Development with Idris. Chapter 15 has a heading but no entries.
What it says
- The page lists changes for running Type-Driven Development with Idris under Idris 2.
- It recommends doing the first 3-4 chapters with Idris 1 and then using this page.
- Unbound implicits have multiplicity 0, so many functions need explicit braces for run-time lengths.
- The Prelude is smaller, so many examples need extra imports such as Data.String.
- Functions must be covering by default, so some need a partial annotation.
- Chapter 10 needs many changes to views because Idris 2 unifies more precisely.
- A first-person note in Chapter 10 calls one Idris 1 behavior embarrassing and unexplained.
What evidence it gives
The page gives code before-and-after for many files. It says the updated code will join the Idris 2 test suite. It offers no tests or results of its own.
Interests and limits
It assumes the reader owns the book, and it quotes no book text. Chapter 15 is empty. It describes one language version at one time, and the page is undated.