Type-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints
summary
Survey of 15 recent works finds type systems recurring in prompt frameworks and presents a formal proposal called lambda Prompt, a dependently typed calculus with probabilistic refinements; the paper catalogs 13 constraints (nine commonly encoded, four underexplored C9–C13) and demonstrates syntactic enforcement on Text-to-SQL and JSON-schema outputs; it proposes a constraint-preserving optimization rule that mutates prompts (summarization, example selection, reordering) and sketches compilation of prompts, while experiments report Text-to-SQL repair needs many retries.
AI-written summary · about
chapters (14)
- 0:00Type-driven prompt programming intro
- 1:48System vs user prompts
- 3:32System prompts as components
- 5:25Typed prompts in apps
- 7:17Motivation for structured prompts
- 8:43Industry adoption of type systems
- 10:27Compiling prompts efficiently
- 12:23Formalizing prompt programs
- 15:36Research gaps in prompt optimization
- 17:25Optimizing via mutation and constraints
- 19:19Token-level type safety
- 20:24Emerging type-driven research
- 21:32Why type systems are essential for safe LLM usage
- 22:42Q&A
related talks
30mIs Prompt Engineering Dead? How Auto-Optimization is Changing the Game
22mNavigating the Evolution of Prompt Engineering
13mPrompt Engineering Simplified
19mUnlocking the Full Potential of LLMs: Advanced Prompt Engineering Techniques
30mIs Prompt Engineering Dead?
16mPrompt Engineering for Testers: Types and Applications
02h 01mPrompt Engineering and AI Red Teaming
55mKeynote: Propositions as Types