BROADCASTS.com

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.\n\nBut 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.\n\nI 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.\n1. We start from zero. Introduction to Lean 4 syntax, side-by-side with Rust. Sum and product types, `List`, some easy intro examples.\n2. _Dependent types_: Example of `Vec`, i.e. lists with statically known length. Dependent pattern matching.\n3. _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?\n4. 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?\n5. _Metaprogramming_: Custom syntax, custom elaborators. Using what we learned to make type-safe SQL queries work, such as (note the absence of string quotes):\n```\nlet dragons : Table Dragon := [...here be dragons...]\nlet dragons2 : Table ?huh? := SELECT name, coins FROM dragons\n```\nCode samples from slides: https://gist.github.com/Kiiyya/5566f09b2d1af6aa0d85ba01179dcfdb\nabout this event: https://cfp.gulas.ch/gpn22/talk/WWMGVN/