31.05, 14:30–15:30 (Europe/Berlin), ZKM Vortragssaal
Sprache: English
Type theory is the secret sauce that makes a programming language awesome. The more knowledge we can make the compiler aware of, the more we can rely on the compiler.
But what is the limit? What if we could take make bad state unrepresentable to the mathematical extreme? What is a proof anyway, can you eat it? Come on a wonderful journey into the land of dependent types, where we try building type-safe SQL queries, and sweeten the deal with our own syntactic sugar.
I give a compressed intro and overview of Lean 4, a purely functional, dependently typed programming language and interactive theorem prover. Knowledge of purely functional languages is not required.
1. We start from zero. Introduction to Lean 4 syntax, side-by-side with Rust. Sum and product types, List, some easy intro examples.
2. Dependent types: Example of Vec, i.e. lists with statically known length. Dependent pattern matching.
3. Propositions-as-types: You can have logical And and Or in Rust, too! But how do you model forall quantifiers? How do you model x <= y in the type system?
4. Playing around with types as first-class objects, using heterogenous lists and projections on them as example. You can't pattern match on types themselves, or... can you?
5. Metaprogramming: Custom syntax, custom elaborators. Using what we learned to make type-safe SQL queries work, such as (note the absence of string quotes):
let dragons : Table Dragon := [...here be dragons...]
let dragons2 : Table ?huh? := SELECT name, coins FROM dragons
Both speech and slides are essential to understanding the content. Slides have almost only code snippets with no explanations. Explanations are almost entirely speech, and I will be pointing to code snippets extensively.
