View publication

Title A Gradual Probabilistic Lambda Calculus
Authors Matías Toro, Federico Olmedo
Publication date April 2023
Abstract 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.
Pages 256-285
Volume 7
Journal name Proceedings of the ACM Programming Languages
Publisher ACM Press (New York, NY, USA)
Reference URL View reference page