Generalization of meta programs with dependent types in mtac2 with mtac2
summary
Presents a concrete tool that automatically transforms meta-functions to expose dependent arguments: lift analyzes a function’s signature (via a ty tree) and emits a version that moves monadic results under dependent foralls. It uses Mtac2 itself and the Mtac2 telescopes to describe dependencies, generates a generalized bind (and other operators) so mfix-based convoy patterns work, and notes mfix and match remain too complex; telescope inference is planned but not yet automatic.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:05Tactics
- 2:28Monets
- 6:06The problem
- 12:24The signature
- 13:04Telescopes
- 14:43Tie trees
- 17:45Lift
related talks
25mMonadic typed tactic programming by reflection
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
36mDependently Typed Multi-Stage Programming, Revisited
50mA Type-Theoretic Framework for Certified Meta-programming
56mOn Type-Based Techniques for Program Manipulation
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
01h 03mVerifying Dependent Type-checkers
25mAdapTT: Functoriality for Dependent Type Casts