Syntax-Generic Operations, Reflectively Reified (Extended Abstract)
summary
Ports a core part of Allais et al.'s datatype-generic library into a new framework that uses Agda elaborator reflection to reify generic constructions into native-looking functions, generating rename/rename-like operations and folds instead of forcing users to write universe encodings. The pipeline extracts a data-type description, requires a small syntax predicate (PCF example has 5 constructors) whose proofs are mostly trivial, and emits hand-written-style code; the approach reduces boilerplate but proof-generation and broader automation remain unfinished.
AI-written summary · about
chapters (5)
related talks
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
26mAbstraction Functions as Types
31mDependently-Typed Programming with Logical Equality Reflection
45mAPLicative Programming with Naperian Functors
23mReasoning about types and code
49mFinite functional programming via graded effects and relevance types
17mTowards Generic Higher-Order Unification Implementations in Haskell
59mHaskell Design Patterns for Genericity & Asynchronous Behavior