Probabilistic programming languages have recently gained a lot of attention, in particular due to their applications in domains such as machine learning and differential privacy. To establish invariants of interest, many such languages include some form of static checking in the form of type systems. However, adopting such a type discipline can be cumbersome or overly conservative. Gradual typing addresses this problem by supporting a smooth transition between static and dynamic checking, and has been successfully applied for languages with different constructs and type abstractions. Nevertheless, its benefits have never been explored in the context of probabilistic languages. In this work, we present and formalize GPLC, a gradual source probabilistic lambda calculus. GPLC includes a binary probabilistic choice operator and allows programmers to gradually introduce/remove static type -- and probability -- annotations. The static semantics of GPLC heavily relies on the notion of probabilistic couplings, as required for defining several relations, such as consistency, precision, and consistent transitivity. The dynamic semantics of GPLC is given via elaboration to the target language TPLC, which features a distribution-based semantics interpreting programs as probability distributions over final values. Regarding the language metatheory, we establish that TPLC -- and therefore also GPLC -- is type safe and satisfies two of the so-called refined criteria for gradual languages, namely, that it is a conservative extension of a fully static variant and that it satisfies the gradual guarantee, behaving smoothly with respect to type precision.

翻译：概率编程语言近年来备受关注，特别是在机器学习和差分隐私等领域的应用。为建立相关不变量，许多这类语言通过类型系统引入某种形式的静态检查。然而，采用此类类型规范可能显得繁琐或过于保守。渐进类型化通过支持静态与动态检查之间的平滑过渡解决了这一问题，并已成功应用于具有不同构造和类型抽象的语言中。尽管如此，其优势从未在概率语言背景下得到探索。本文提出并形式化了GPLC——一种渐进式源概率Lambda演算。GPLC包含二元概率选择算子，允许程序员逐步引入/移除静态类型与概率注释。GPLC的静态语义高度依赖概率耦合的概念，这是定义一致性、精确性及一致传递性等若干关系所必需的。GPLC的动态语义通过精化到目标语言TPLC实现，该目标语言采用基于分布的语义，将程序解释为最终值上的概率分布。在语言元理论方面，我们证明TPLC（从而GPLC）具有类型安全性，并满足渐进语言的所谓精细化准则中的两条：即它是完全静态变体的保守扩展，且满足渐进保证，在类型精确性方面表现平滑。