Introduction to programming with dependent types in Scala
Offered By: Stepik
Course Description
Overview
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.
Syllabus
- Installing software
- Boolean type
- ProvingGround DSL
- Type of natural numbers
- Combining booleans and natural numbers
- List type
- Dependent types
- Type classes. Simulacrum
- Product type
- Co-product type (sum type)
- Function type
- Empty and unit types
- Type family List(A)
- Dependent pair type (Σ-type)
- Dependent function type (Π-type)
- Type of length-indexed vectors
- Heterogeneous list (HList)
- Matrices
- Identity type. Curry–Howard correspondence
- Eliminators into dependent types (induction)
- Type-level programming. Shapeless
Taught by
Dmytro Mitin
Related Courses
Functional Programming Principles in ScalaÉcole Polytechnique Fédérale de Lausanne via Coursera Functional Program Design in Scala
École Polytechnique Fédérale de Lausanne via Coursera Parallel programming
École Polytechnique Fédérale de Lausanne via Coursera Big Data Analysis with Scala and Spark
École Polytechnique Fédérale de Lausanne via Coursera Functional Programming in Scala Capstone
École Polytechnique Fédérale de Lausanne via Coursera