Revisiting Occurrence Typing

Giuseppe Castagna (1, 2) , Victor Lanvin (2) , Mickaël Laurent (2) , Kim Nguyen (3)

1 CNRS - Centre National de la Recherche Scientifique
2 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
3 LMF - Laboratoire Méthodes Formelles

We revisit occurrence typing, a technique to re ne the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages. Although occurrence typing was tied from its inception to set-theoretic types-union types, in particular-it never fully exploited the capabilities of these types. Here we show how, by using set-theoretic types, it is possible to develop a general typing framemork that encompasses and generalizes several aspects of current occurrence typing proposals and that can be applied to tackle other problems such as the inference of intersection types for functions and the optimization of the compilation of gradually typed languages.

Keywords: occurrence typing; type inference; union types; intersection types; TypeScript; Flow language; dynamic languages; type case; gradual typing; CCS Concepts: • Theory of computation → Type structures; • Software and its engi- neering → Functional languages; Functional languages; Type structures; Theory of computation; Program analysis

Domains: Programming Languages [cs.PL]

Giuseppe Castagna, Victor Lanvin, Mickaël Laurent, Kim Nguyen. Revisiting Occurrence Typing. 2021. ⟨hal-02181137v4⟩