Содержание курса
Theory
17 уроков
1.
Installing software
↗
2.
Dependent types
↗
3.
Path-dependent types
↗
4.
Type classes. Simulacrum
↗
5.
Product type
↗
6.
Co-product type (sum type)
↗
7.
Function type
↗
8.
Dependent pair type (Σ-type)
↗
9.
Dependent function type (Π-type)
↗
10.
Empty and unit types
↗
11.
Boolean type
↗
12.
Type of natural numbers
↗
13.
List type
↗
14.
Type of fixed-length vectors
↗
15.
Identity type. Curry–Howard correspondence
↗
16.
Eliminators into dependent types (induction)
↗
17.
Type-level programming. Shapeless
↗
Practice
24 урока
1.
Boolean type: OR, XOR, isEqual
↗
2.
Type of natural numbers. Part 1: triple, predecessor, square
↗
3.
Type of natural numbers. Part 2: multiplication, add3
↗
4.
Type of natural numbers. Part 3: exponentiation, factorial
↗
5.
Type of natural numbers. Part 4: isZero, isOdd/isEven
↗
6.
Type of natural numbers. Part 5: isEqual, isLess/isGreater
↗
7.
Type of natural numbers. Part 6: subtract, Fibonacci
↗
8.
Product type: half, Fibonacci
↗
9.
Dependent function type (Π-type): ifElse
↗
10.
List type. Part 1: head, tail, isNil
↗
11.
List type. Part 2: last, init, append
↗
12.
List type. Part 3: revert, concatenation, take/drop
↗
13.
Type family List(A). Part1: map, filter
↗
14.
Type family List(A). Part2: foldl/foldr
↗
15.
Type family List(A). Part 3: zip, isEqual
↗
16.
Type of fixed-length vectors. Part 1: append, concatenation
↗
17.
Type of fixed-length vectors. Part 2: addition, scalar product
↗
18.
Matrices: transpose
↗
19.
Identity type. Part 1: symmetricity, transitivity, mapping
↗
20.
Identity type. Part 2: NOT(NOT), AND true/false, de Morgan
↗
21.
Identity type. Part 3: AND is commutative, 0 is neutral element
↗
22.
Type classes: list as a Monad and binary tree as a Foldable
↗
23.
Type-level programming. Part 1: number exponentiation
↗
24.
Type-level programming. Part 2: vector concatenation
↗