Reducing the Slippery Surface of Failure with Dependent Types

Scala's type system allows us to enforce compile-time constraints on our programs, and to take advantage of these constraints to help reason about our code. Yet we still frequently encounter situations where extracting a value from a map is not guaranteed to succeed, or mapping across a set of cases is not guaranteed to be exhaustive. With dependent types we can make operations like these completely safe by construction, in the process eliminating entire classes of errors, and furthermore we can do this without complicating user code. The talk will cover several simple and intermediate examples using dependent types, and will give a brief outline of some of the the challenges involved in implementing typesafe libraries with dependent types in Scala.

Talk objectives:

Demonstrating how dependent types can help users write safer, more reliable software.

Target audience:

The talk will be accessible to all programmers, though a basic understanding of Scala syntax and type systems will be useful.