assignment Niveau : Introductif
chat_bubble_outline Langue : Anglais
card_giftcard 0 point
- /5
Avis de la communauté
0 avis

Les infos clés

credit_card Formation gratuite

En résumé

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.

more_horiz Lire plus
more_horiz Lire moins

Le programme

Course format
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.

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


Les intervenants

Dmytro Mitin


La plateforme est un LMS basé sur le cloud conçu pour l'informatique. Créez des cours en ligne avec plus de 20 types d'affectation interactive gratuitement.

Vous êtes le concepteur de ce MOOC ?
Quelle note donnez-vous à cette ressource ?