Computing with Generic Trees in Agda
summary
Shows that a small tweak to W-types makes generic tree definitions compute in Agda: replace function-indexed places with a mix of finitary tuples and labeled infinite parts. Implements finitary domains as explicit finite codes, then builds an Infinity W-type using partition sets that separate finite from infinite places. Demonstrates the induction principle now reduces definitionally (three distinct recursive occurrences in the example) and the construction works in Agda without breaking definitional equality.
AI-written summary · about
chapters (6)
- 0:00Start
- 2:57Writing the Induction Principle for Binary Trees
- 7:19Finite Types
- 10:22Lambda and Application Functions
- 11:25Dependent Functions
- 16:09Induction Principle
related talks
44mAbstract data types in region of abysmal pain & how to navigate them
26mAbstraction Functions as Types
40mHigher Inductive Types in Homotopy Type Theory
27mIntrinsically Correct Sorting in Cubical Agda
01h 00mInvited Talk: Type inference in OCaml and GHC using Levels
01h 32mAlgorithms for Trees - Foldable, Applicative, Traversable
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
21mGraded Monoids for Dependently Typed Array Programming