Type level programming for everyone

Strongly and statically typed programming languages ​​are found in almost every field of IT. They even settled in many niches, so far, it would seem, reserved for dynamic languages ​​(e.g. the popularity of TypeScript on the frontend). In addition to better guarantees of data correctness and the state of our program, static typing can give us a lot more. In theory, at compile time on the type level, it is possible to perform any computation that can be performed on values ​​at run time. Until now, these capabilities were only available in a handful of programming languages ​​and required a thorough understanding of the mathematical underpinnings of the type system. Scala 3 has brought a big change here, giving developers easy-to-use and intuitive tools to achieve compile-time validation that would be inexpressible in other languages.

As part of the lecture, we will present some tools available in the Scala 3 type system. We will also show how they can be used for advanced verification of program correctness and transfer of some calculations from program execution time to compilation time. The lecture will be of a practical nature. It does not require participants to have any knowledge of type theory.