Agda from Nothing: Order in the Types

on YouTube ↗01h 47m

" summary

Claims how to build binary search tree implementations in Agda that are correct-by-construction, following Conor McBride’s paper and using literate Agda (TeX) and Agda + Emacs live coding from a GitHub repo. Workshop implements insert, from-list and flatten, then generalizes to a universe of ordered containers and 2–3 trees; the type-level trick stores ordering proofs in leaves so only about n+1 proofs appear for n values. Code runs (normalizes) and produces ordered lists as shown.

AI-written summary · about

" chapters (10)

1. 0:00Agda introduction
2. 16:41Agda syntax and types
3. 26:56Binary search trees in Agda
4. 38:13Tree invariants enforcement
5. 55:22Dependent types and proofs
6. 1:00:03Inserting with bounds
7. 1:16:59Ordered lists construction
8. 1:28:25Two-three trees balancing
9. 1:37:35Generic programming in Agda
10. 1:46:23Summary

" related talks

• 01h 20mA Practical Introduction to Haskell GADTsRichard A. Eisenberg · LambdaConf 2015
• 55mParallel-by-construction Tree Manipulation with APL (Part 1)Aaron W Hsu · LambdaConf 2018
• 47mIntroduction to FP Using Haskell (Part 2)Tony Morris · LambdaConf 2018
• 46mCorecursion, Codata, and Just a Little Combinatorial Game TheoryCarlos Rodrigues · LambdaConf 2017
• 45m(Programming Languages) in Agda = Programming (Languages in Agda)Philip Wadler · Full Stack Fest 2019
• 46mChasing Arrows, in categories containing functors and monadsJim Newton, Uli · Scala.IO 2024 - Nantes
• 01h 39mIsomorphic Reasoning: Counting with Types Part 1Alexander Konovalov, Emily Pillmore · LambdaConf 2019
• 36mCategory Theory: An Abstraction for AnythingAlissa Pajer · Strange Loop 2013