A Limited Case for Reification by Type Inference
summary
Claims that Coq’s notation system plus type inference can perform reification for a restricted class of problems, specifically extracting the curried argument type structure of functions to support uncurrying, reassociation, and reordering. Implementation uses an inductive list-of-types, a denotation function, and notations that insert reify here functions at each binder so type inference builds the list; example code produces a reversed uncurried function and works, but requires an extra unit tail and has limited applicability (universe/list pitfalls and binder-shape constraints).
AI-written summary · about
chapters (6)
- 0:00Reification by type inference
- 1:45Querying with uncurried functions
- 4:58Call-by-value uncurry semantics
- 6:07Inductive unquery types
- 8:58Reversing type representations
- 10:03Q&A
related talks
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
25mDeriving Instances with Dependent Types
19mType Inference Logics
22mA Calculus of Inductive Linear Constructions
19mExtensible Metatheory Mechanization via Family Polymorphism
11mLocal algebraic effect theories
15mElaboration with First-Class Implicit Function Types
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...