Types that Count: a Journey across Qualitative and Quantitative Intersection Type Disciplines

Since their introduction more than 45 years ago, intersection types have found countless uses in both the syntactic and semantic study of programming languages. This thesis continues such tradition, presenting two lines of research centred around intersection type disciplines. A first line explores the connections between idempotent (qualitative) and non-idempotent (quantitative) intersection type systems for λ-calculus. We start by introducing uniform types, a decidable restriction of non-idempotent intersection types that turns out to be the quantitative counterpart of simple types. We provide two alternative proofs of this correspondence. In the first one, a general intersection type inference semi-algorithm is progressively refined into an algorithm tailored to the uniform system, exploiting the fact that term normalization and termination of inference procedures are intimately related. Following a complementary approach, the result is also achieved by means of a novel, mechanically verified proof of subject expansion in intersection type systems without nullary intersection. As notable byproducts, our investigation yields a new syntactic proof of strong normalization for simply typed terms, as well as a family of perpetual reduction strategies. Finally, leveraging intuitions developed in the uniform case, and taking inspiration from Linear Logic, we present some preliminary ideas on a general technique for transforming qualitative type derivations into quantitative ones. A second line of research employs quantitative types in the study of probabilistic computations, with the aim of integrating the expressiveness of higher-order programming languages with the efficiency of Bayesian networks. Specifically, we introduce a Linear Logic-inspired probabilistic λ-calculus and an associated non-idempotent intersection type system, whose intrinsic resource-consciousness allows to track the generation of random variables and the dependencies between them. We use this information to endow typed terms with a compositional and costaware semantics based on factors, a mathematical notion widely used in Bayesian inference, and to prove soundness and completeness of our language w.r.t. Bayesian networks. Higher-order and possibly recursive programs of suitable type are put into correspondence with Bayesian networks operationally, via rewriting, and semantically, via an acyclic graph structure built on top of type derivations. Our perspective contributes to a rigorous understanding (in a functional setting) of templates, informal depictions of stochastic models used to enhance the expressiveness of standard Bayesian networks.