『Type-Driven Development with Idris』
PART 1: INTRODUCTION
1. OVERVIEW ►
2. GETTING STARTED WITH IDRIS ►
PART 2: CORE IDRIS
3. INTERACTIVE DEVELOPMENT WITH TYPES ►
4. USER DEFINED DATA TYPES ►
5. INTERACTIVE PROGRAMS: INPUT AND OUTPUT PROCESSING ▸
6. PROGRAMMING WITH FIRST CLASS TYPES ‣
7. INTERFACES: USING CONSTRAINED GENERIC TYPES ►
8. EQUALITY: EXPRESSING RELATIONSHIPS BETWEEN DATA ►
9. PREDICATES: EXPRESSING ASSUMPTIONS AND CONTRACTS IN TYPES ►
10. VIEWS: EXTENDING PATTERN MATCHING ►
PART 3: IDRIS AND THE REAL WORLD
11. STREAMS AND PROCESSES: WORKING WITH INFINITE DATA ►
12. WRITING PROGRAMS WITH STATE ▸
13. STATE MACHINES: VERIFYING PROTOCOLS IN TYPES ‣
14. DEPENDENT STATE MACHINES: HANDLING FEEDBACK AND ERRORS ►
15. TYPE-SAFE CONCURRENT PROGRAMMING ►
APPENDIXES
APPENDIX A: INSTALLING IDRIS AND EDITOR MODES ►
APPENDIX B: INTERACTIVE EDITING COMMANDS
APPENDIX C: REPL COMMANDS
APPENDIX D: THE PACKAGING SYSTEM