Les infos clés
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.
Slides, video lectures, programming exercices (in pure Scala and in Scala + ProvingGround library)
- Scala, Git, sbt, and ProvingGround library from Github should be pre-installed for completing most exercises.
- Some experience with Scala is expected (e.g. reading book "Programming in Scala" by Martin Odersky et al. or taking first courses from Scala specialization at Coursera).
- Basic knowledge of functional programming (Haskell or ML) and general OOP language like Java (or C++) would be helpful.
- General familiarity with ideas of recursion and induction is presumed.
- Although such Scala libraries as Shapeless, Simulacrum, Matryoshka, Cats/Scalaz/Algebird etc. can be mentioned from time to time and code samples in Idris are shown, deep understanding of these libraries or languages is NOT necessary.
- People who are interested in functional programming (Scala, Haskell), programming with dependent types (Idris), type-level programming (Shapeless).
1.1 Installing software
1.2 Dependent types
1.3 Path-dependent types
1.4 Type classes. Simulacrum
1.5 Product type
1.6 Co-product type (sum type)
1.7 Function type
1.8 Dependent pair type (Σ-type)
1.9 Dependent function type (Π-type)
1.10 Empty and unit types
1.11 Boolean type
1.12 Type of natural numbers
1.13 List type
1.14 Type of fixed-length vectors
1.15 Identity type. Curry–Howard correspondence
1.16 Eliminators into dependent types (induction)
1.17 Type-level programming. Shapeless
2.1 Boolean type: OR, XOR, isEqual
2.2 Type of natural numbers. Part 1: triple, predecessor, square
2.3 Type of natural numbers. Part 2: multiplication, add3
2.4 Type of natural numbers. Part 3: exponentiation, factorial
2.5 Type of natural numbers. Part 4: isZero, isOdd/isEven
2.6 Type of natural numbers. Part 5: isEqual, isLess/isGreater
2.7 Type of natural numbers. Part 6: subtract, Fibonacci
2.8 Product type: half, Fibonacci
2.9 Dependent function type (Π-type): ifElse
2.10 List type. Part 1: head, tail, isNil
2.11 List type. Part 2: last, init, append
2.12 List type. Part 3: revert, concatenation, take/drop
2.13 Type family List(A). Part1: map, filter
2.14 Type family List(A). Part2: foldl/foldr
2.15 Type family List(A). Part 3: zip, isEqual
2.16 Type of fixed-length vectors. Part 1: append, concatenation
2.17 Type of fixed-length vectors. Part 2: addition, scalar product
2.18 Matrices: transpose
2.19 Identity type. Part 1: symmetricity, transitivity, mapping
2.20 Identity type. Part 2: NOT(NOT), AND true/false, de Morgan
2.21 Identity type. Part 3: AND is commutative, 0 is neutral element
2.22 Type classes: list as a Monad and binary tree as a Foldable
2.23 Type-level programming. Part 1: number exponentiation
2.24 Type-level programming. Part 2: vector concatenation