Test-Driven Design (or Development) is a well-known technique that uses "examples" to let the design of a piece of software emerge from the gradual refinement of features, providing evidence of the correct behaviour of the code through the execution of tests.

TDD is great, but, from a modelling perspective, it makes it hard to see the "big picture", to express properties of our domain elements in both a human-readable and machine-checkable form.

Modern type systems as exemplified in functional programming languages like Haskell, Elm, or Idris, are powerful tools to help design and model complex domains: A type can be more than a name or structure definition, it can embed properties of parts of a domain, in order to make impossible states unrepresentable.

The goal of this lab is to introduce the audience to some principles of Type-Driven Development, using features provided by functional programming languages like Haskell and Idris. After a short introduction to algebraic structures and dependent types, we will work on a small but interesting enough domain to model it using a few techniques and tools made possible by "advanced" type systems, hopefully improving both the robustness and the expressiveness of the code.