About this course
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 for the intro video: PDF
This is updated version of the course. Former version was here:
https://stepik.org/course/2294/
https://stepik.org/course/2608/syllabus (#9)
Whom this course is for
People who are interested in functional programming (Scala, Haskell), programming with dependent types (Idris), type-level programming (Shapeless).
Initial requirements
In the course programming assignments can be performed online. Also Scala, Git, mill/sbt, and ProvingGround library from Github can be installed locally.
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.