This course is an introduction to type theory, homotopy type theory (HoTT), dependent-type programming, type-level programming, and theorem proving using Scala. It covers such topics as dependent types (including path dependent types), type families, sum and product types, functions, dependent Σ- and Π-type, inductive types, identity type, type classes, eliminators (recursion and induction), β-reduction, η-conversion, Curry–Howard isomorphism, programming at type level.
Overview
Syllabus
- Installing software
- Boolean type
- ProvingGround DSL
- Type of natural numbers
- Combining booleans and natural numbers
- List type
- Dependent types
- Type classes. Simulacrum
- Product type
- Co-product type (sum type)
- Function type
- Empty and unit types
- Type family List(A)
- Dependent pair type (Σ-type)
- Dependent function type (Π-type)
- Type of length-indexed vectors
- Heterogeneous list (HList)
- Matrices
- Identity type. Curry–Howard correspondence
- Eliminators into dependent types (induction)
- Type-level programming. Shapeless
Taught by
Dmytro Mitin
