EMBER_CLI_FASTBOOT_BODY

ThCS. Introduction to programming with dependent types in Scala

This course is adaptive: it will adjust according to your skill
Video Player is loading.
Current Time 0:00
/
Duration 0:00
Loaded: 0%
Progress: 0%
Stream Type LIVE
Remaining Time -0:00
 
1x
Play
To watch this video please visit https://stepik.org/lesson//step/

About the course

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

Instructors

  1. User picture
    Dmytro Mitin
    https://www.researchgate.net/profile/Dmytro_Mitin https://www.linkedin.com/in/dmitin https://stackoverflow.com/users/5249621/dmytro-mitin?tab=profile

Reviews

5
Thank you so much for the course! IMHO it would be great if in some assignments student were forced to write a solution in more modular way. For example write induction base and induction steps separately and then combine it. It would help to demystify Proving Ground API signatures.
abo wang April 24, 2017 link
5
thanks for all the support and this awesome class What did I like? I like the overall course, and most importantly support from @Dmytro_Mitin What didn't I like? the grader, it could be more intelligent Did I find anything new for you? yep, I took this course because this is relatively new for me. programming using type constraints. Was it useful for me? theoretically yes, practically haven't find any area where I can adopt my learning. Whom could you recommend the course? I will recommend to friend who is interested in type level programming.
Marco Blažek April 7, 2017 link
5
I'm here from reddit. Great course! Thank you.
Video Player is loading.
Current Time 0:00
/
Duration 0:00
Loaded: 0%
Progress: 0%
Stream Type LIVE
Remaining Time -0:00
 
1x
Play
To watch this video please visit https://stepik.org/lesson//step/
5 All reviews

Theoretical Computer Science. Introduction to programming with dependent types in Scala

Open date:
Mar 31, 2017
Workload:
Anyone can take this course with his/her own speed.
Expected time to complete:
13 hours
Language:
English
Certificate:
Not issuing

About the course

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

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

This course is entirely free. All content is available now.