9. Draft

All the sections of this chapter are very DRAFT.

• 9.1. Hoare State Monad (Swierstra)
  • 9.1.1. Without Monad
  • 9.1.2. With Monad
  • 9.1.3. Hoare Monad
  • 9.1.4. Certified Relabelling
  • 9.1.5. Some Analysis
  • 9.1.6. Example: Open File Descriptors
  • 9.1.7. Example: Open File Descriptors (2)
  • 9.1.8. Example: Open File Descriptors (3)
• 9.2. IO
  • 9.2.1. Console Programs
  • 9.2.2. IO Interface
  • 9.2.3. Sinks
  • 9.2.4. Buffers
  • 9.2.5. Appendix
    • 9.2.5.1. Length Indexed Buffers
• 9.3. Effects (Idris)
• 9.4. Wellfounded Recursion
  • 9.4.1. W Types
  • 9.4.2. Unbounded Search with Bound Function
  • 9.4.3. Merge Sorted Lists
  • 9.4.4. Ackermann Function
  • 9.4.5. Unbounded Search for Natural Numbers
  • 9.4.6. Wellfounded Relations on Inductive Types
• 9.5. Monad Recursion
  • 9.5.1. Parsing Monad
  • 9.5.2. Monadic Parser with Progress Indicator
  • 9.5.3. State and Continuation Monads and Progress
  • 9.5.4. Progress in IO
• 9.6. Group Theory
  • 9.6.1. Subgroups
  • 9.6.2. The Integers mod n
  • 9.6.3. Cyclic Subgroups
• 9.7. Records, Objects, …
  • 9.7.1. Inductive Data Types
  • 9.7.2. Records
• 9.8. Platforms
  • 9.8.1. Unix Console Applications
  • 9.8.2. Browser Applications
  • 9.8.3. Server Applications
• 9.9. Pattern Match
  • 9.9.1. Ideas from “Implementation of Functional Languages” of Simon Peyton Jones.
  • 9.9.2. Examples
• 9.10. Pattern Match Compiler
  • 9.10.1. Basics
  • 9.10.2. ?
  • 9.10.3. Example nodups
  • 9.10.4. Example: Eliminate Duplicates
  • 9.10.5. Examply unwieldy
  • 9.10.6. Example: demo
  • 9.10.7. Example: less equal
  • 9.10.8. Example: greater equal
  • 9.10.9. Example: map2
• 9.11. Pattern Guard