Is Sized Typing for Coq Practical?
summary
Implementation of CIC^ sized type theory inside a Coq 8.12 kernel fork produces a full size-inference pipeline that emits difference constraints solved by Bellman-Ford O(V·C). Evaluation shows practical failure: compiling MSetList slows by 5.5×* with many constraint checks, worst cases reaching ~4,000 variables and 2,500 constraints (V·C ≈ 10 million) and contrived Nats6 taking >2 minutes. Conclusion: fully automatic, backward-compatible size inference is impractical; manual top-level annotations are a possible mitigation.
AI-written summary · about
chapters (15)
- 0:00Size typing for Coq intro
- 1:05Coq needs termination checking
- 3:12What size types are
- 5:39Past size types in CIC
- 7:09Cic hat star goals
- 8:12Size typing pipeline
- 10:23Fixpoint typing rules
- 12:12Cumulativity and constraints
- 13:56Constraint satisfiability
- 15:42Constraint growth issues
- 17:06Impact on Coq library
- 18:56Why size typing impractical
- 19:38Future directions
- 20:45Paper details & Q&A
- 21:27Q&A
related talks
30mConvenient Algebraic Programming with Coercive Subtyping
24mA Type-Based Approach to Divide-and-Conquer Recursion in Coq
43mShape-Constrained Array Programming with Size-Dependent Types
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
46mThe Calculated Typer (Functional Pearl)
01h 34mFormal Logic Undressed
01h 00mInvited Talk: Type inference in OCaml and GHC using Levels
35mHow to make ad hoc proof automation less ad hoc