The Dependently Typed Revolution
Dependently typed programming languages have a more powerful type system, allowing types to impose arbitrarily complex constraints on the relationships between function inputs and outputs.
In this workshop, we will explore some theory of dependently typed programming, and then learn to use Idris, a dependently typed language, on a toy problem (proving that certain moves in the game Minesweeper are safe). We will then briefly look at an HTTP server written in Idris to learn how dependent types can be used to improve type safety in real world systems.
Outline/Structure of the Workshop
- I will start with an introduction of the definition of 'dependently typed', with some motivating examples.
- I will then introduce the audience to the Curry-Howard Correspodence, and explain what consequence that has for proving things at the type level. I will also explain the concept of formal verification.
- I will introduce Proofsweeper (https://github.com/A1kmm/proofsweeper), a mine-sweeper game where you have to formally prove in Idris that a square is or isn’t a mine before marking it, and will take the audience through a basic proof, explaining how formal proofs are constructed in practice.
- After that point, I will demonstrate how http4idris uses dependent types to provide type safety for real world systems.
Attendees can expect to learn what dependent types are, what formal verification is, and to know some basic concepts around of how dependent types can be applied to formally verify properties of functional programs in the real world.
Functional programmers who don’t yet know much about dependent types, and are ready to take type safety to the next level.
Prerequisites for Attendees
Experience with statically typed functional programming is assumed. No prior knowledge of dependently typed programming will be assumed.