# Revisiting Occurrence Typing

## TL;DR

This paper revisits occurrence typing, enhancing it with set-theoretic types to create a unified framework that improves type inference, supports intersection types, and optimizes compilation in gradually typed languages.

## Contribution

It introduces a general set-theoretic type framework for occurrence typing, unifying and extending existing approaches and enabling new applications.

## Key findings

- Develops a comprehensive set-theoretic occurrence typing framework
- Enables reconstruction of intersection types for unannotated functions
- Improves compilation efficiency for gradually typed languages

## Abstract

We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capturesome programming patterns used in untyped languages. Although occurrence typing was tied from its inceptionto set-theoretic types-union types, in particular-it never fully exploited the capabilities of these types. Here weshow how, by using set-theoretic types, it is possible to develop a general typing framework that encompasses andgeneralizes several aspects of current occurrence typing proposals and that can be applied to tackle other problemssuch as the reconstruction of intersection types for unannotated or partially annotated functions and the optimizationof the compilation of gradually typed languages.