Convenient Algebraic Programming with Coercive Subtyping
summary
System automatically inserts the roll/unroll and catamorphism coercions so algebraic programs typecheck without manual coercive subtyping annotations, claiming the inferred coercions preserve the totality guarantees of Menler-style algebras. A custom logic-programming solver called Chronolog solves generated subtyping constraints with a suspend/resume discipline to avoid divergent proof search; an implementation and an Agda formalization exist. Solver is research-grade with rule indexing for speed, coherence and broader recursion schemes remain open work.
AI-written summary · about
chapters (19)
- 0:00Algebraic programming goals
- 1:10Strong functional programming
- 2:31F-algebras and catamorphisms
- 4:15Menler style algebras
- 6:25Introducing LCA language
- 7:31Programming examples and coercion
- 8:38Motivation for coercive subtyping
- 10:03Subtyping rules in LCA
- 12:14Algorithmic subtyping without transitivity
- 13:39Connecting subtyping to coercions
- 14:43Implicit subtyping in LCA-minus
- 15:47Constraint generation process
- 17:33Constraint solving with suspended goals
- 19:20Correspondence between LCA and LCA-minus
- 20:49Convenient algebraic programming
- 21:12Leveraging coercive subtyping
- 21:54Future work on coherence and inference
- 23:00Extending to coinductive data types
- 23:41Q&A
related talks
46mThe Calculated Typer (Functional Pearl)
15mLogic Programming with Extensible Types (Lightning talk)
24mA Type-Based Approach to Divide-and-Conquer Recursion in Coq
01h 34mFormal Logic Undressed
35mHow to make ad hoc proof automation less ad hoc
41mThe Dialectics of Type-Level Programming
52mWhat logic can teach us, Scala programmers
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)