Abstract

Probabilistic programming languages have recently gained a lot of attention, in particular due to their applications in domains such as machine learning and di similar to erential 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 di similar to erent constructs and type abstractions. Nevertheless, its bene similar to ts 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 de similar to ning 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 similar to nal values. Regarding the language metatheory, we establish that TPLC-and therefore also GPLC- is type safe and satis similar to es two of the so-called re similar to ned criteria for gradual languages, namely, that it is a conservative extension of a fully static variant and that it satis similar to es the gradual guarantee, behaving smoothly with respect to type precision.