Kats Workshop, May 2016

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