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)