О курсе
UPDATED VERSION OF THIS COURSE: https://stepik.org/course/49181
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
Syllabus
1 Theory
1.1 Installing software https://goo.gl/ZmIdzy
1.2 Dependent types https://goo.gl/6AhLf7
1.3 Path-dependent types https://goo.gl/bWgUCr
1.4 Type classes. Simulacrum https://goo.gl/zqx1ra
1.5 Product type https://goo.gl/KAdaSD
1.6 Co-product type (sum type) https://goo.gl/qogGSF
1.7 Function type https://goo.gl/j1fRio
1.8 Dependent pair type (Σ-type) https://goo.gl/h8cmDG
1.9 Dependent function type (Π-type) https://goo.gl/6hGcq3
1.10 Empty and unit types https://goo.gl/e9JTD7
1.11 Boolean type https://goo.gl/vlR833
1.12 Type of natural numbers https://goo.gl/lBnbh8
1.13 List type https://goo.gl/H64rOg
1.14 Type of fixed-length vectors https://goo.gl/9p5KwO
1.15 Identity type. Curry–Howard correspondence https://goo.gl/15EDMw
1.16 Eliminators into dependent types (induction) https://goo.gl/C2Mrd7
1.17 Type-level programming. Shapeless https://goo.gl/5XPk4K
2 Practice
Press button "Continue" / "Продолжить" or choose exercise below.
2.1 Boolean type: OR, XOR, isEqual https://goo.gl/B1XlVJ
2.2 Type of natural numbers. Part 1: triple, predecessor, square https://goo.gl/RD70kA
2.3 Type of natural numbers. Part 2: multiplication, add3 https://goo.gl/X1V6KN
2.4 Type of natural numbers. Part 3: exponentiation, factorial https://goo.gl/1mm98T
2.5 Type of natural numbers. Part 4: isZero, isOdd/isEven https://goo.gl/97DeIz
2.6 Type of natural numbers. Part 5: isEqual, isLess/isGreater https://goo.gl/bdKxtr
2.7 Type of natural numbers. Part 6: subtract, Fibonacci https://goo.gl/1xuFLn
2.8 Product type: half, Fibonacci https://goo.gl/8hHjLF
2.9 Dependent function type (Π-type): ifElse https://goo.gl/H2Hn70
2.10 List type. Part 1: head, tail, isNil https://goo.gl/MdzxzJ
2.11 List type. Part 2: last, init, append https://goo.gl/lxyzgL
2.12 List type. Part 3: revert, concatenation, take/drop https://goo.gl/BiFbQX
2.13 Type family List(A). Part1: map, filter https://goo.gl/stQOqK
2.14 Type family List(A). Part2: foldl/foldr https://goo.gl/KKcRLx
2.15 Type family List(A). Part 3: zip, isEqual https://goo.gl/EDPnn9
2.16 Type of fixed-length vectors. Part 1: append, concatenation https://goo.gl/OpZir7
2.17 Type of fixed-length vectors. Part 2: addition, scalar product https://goo.gl/DpRBKP
2.18 Matrices: transpose https://goo.gl/7QqsVv
2.19 Identity type. Part 1: symmetricity, transitivity, mapping https://goo.gl/LREICv
2.20 Identity type. Part 2: NOT(NOT), AND true/false, de Morgan https://goo.gl/Qc8GjQ
2.21 Identity type. Part 3: AND is commutative, 0 is neutral element https://goo.gl/3vuZe7
2.22 Type classes: list as a Monad and binary tree as a Foldable https://goo.gl/GiejFv
2.23 Type-level programming. Part 1: number exponentiation https://goo.gl/zHTbn1
2.24 Type-level programming. Part 2: vector concatenation https://goo.gl/rwhrR4
Для кого этот курс
People who are interested in functional programming (Scala, Haskell), programming with dependent types (Idris), type-level programming (Shapeless).
Начальные требования
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.