Outline
The workshop will roughly follow the structure below. I’ll assume you have some experience with a functional programming language (either Haskell, ML or Scala). Each section is covered in more depth in Type-driven Development with Idris; if you download and read the free sample chapter beforehand you’ll be ready to get started with Idris.
-
10:30 Fundamentals: First class types, vectors, defining data types.
(Chapters 1-4, 6-7 of TypeDD) - 11:30 Break and Exercises (Exercise sheet)
- 12:00 Relationships between data: equality proofs, expressing assumptions in types.
(Chapters 8-9 of TypeDD) - 13:00 Lunch (Exercise sheet)
- 14:30 Effects: IO, Side effects, reasoning about state
(Chapters 5, 12-13 of TypeDD) - 16:00 Break and Exercises (Exercise sheet)
- 16:30 Total Functional Programming: views, streams, processes and type safe concurrency
(Chapters 10-11 of TypeDD)
Materials
- Type-driven Development with Idris – please download and read the sample chapter before the workshop to get started with Idris.
- Source code for the examples
- Slides
- Exercises:Part 1, Part 2, Part 3.