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
```
Code samples from slides: https://gist.github.com/Kiiyya/5566f09b2d1af6aa0d85ba01179dcfdb