Deriving Instances with Dependent Types
summary
Automates building typeclass instances for Coq inductives: the deriving library generates EQ, Choice, Countable/Fin-like and other instances without plugins and with generates math-comp instances by default by extracting constructor signatures from the type’s eliminator (so it extracts signature from eliminator). Representation uses an initial-algebra/functor fold and dependently typed combinators; already covers over 40 types. Limitations: slow inference (quadratic blowup on large constructors), poor binder naming, and no mutual or indexed-inductive support yet.
AI-written summary · about
chapters (7)
- 0:00Problem introduction
- 4:17Deriving library intro
- 7:59Inductive types representation
- 15:54Automatic representation inference
- 16:14Custom instances demo
- 20:09Future work and conclusion
- 20:56Q&A
related talks
14mA Limited Case for Reification by Type Inference
22mA Calculus of Inductive Linear Constructions
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
24mDerive class instances topdown and derive ttg automatically
19mExtensible Metatheory Mechanization via Family Polymorphism
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
30mDotty and types: the story so far
20mPractical and sound equality tests, automatically