Type-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints

TL;DR

This paper introduces Lambda Prompt, a dependently typed calculus with probabilistic refinements, to enhance constraint expressiveness and support algorithms in prompt programming frameworks for large language models.

Contribution

It proposes a type-theoretic foundation for prompt programming, addressing gaps in constraint expressiveness and algorithm support through a new calculus and optimization rules.

Findings

Catalog of 13 constraints for prompt programming

Identification of underexplored areas in constraint expressiveness

Proposal of a constraint-preserving optimization rule

Abstract

Prompt programming treats large language model prompts as software components with typed interfaces. Based on a literature survey of 15 recent works from 2023 to 2025, we observe a consistent trend: type systems are central to emerging prompt programming frameworks. However, there are gaps in constraint expressiveness and in supporting algorithms. To address these issues, we introduce the notion of Lambda Prompt, a dependently typed calculus with probabilistic refinements for syntactic and semantic constraints. While this is not yet a full calculus, the formulation motivates a type-theoretic foundation for prompt programming. Our catalog of 13 constraints highlights underexplored areas in constraint expressiveness (constraints 9 through 13). To address the algorithmic gap, we propose a constraint-preserving optimization rule. Finally, we outline research directions on developing a compiler for prompt programs.