Introduction to programming with dependent types in Scala

Course format
Slides, video lectures, programming exercices (in pure Scala and in Scala + ProvingGround library)

Requirements

• 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.

Target audience

• 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 Practice
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