Safety Analysis versus Type Inference

Abstract

Safety analysis is an algorithm for determining if a term in the untyped lambda calculus with constants is safe, i.e., if it does not cause an error during evaluation. This ambition is also shared by algorithms for type inference. Safety analysis and type inference are based on rather different perspectives, however. Safety analysis is based on closure analysis, whereas type inference attempts to assign a type to all subterms.

In this paper we prove that safety analysis is sound, relative to both a strict and a lazy operational semantics, and superior to type inference, in the sense that it accepts strictly more safe lambda terms.

The latter result may indicate the relative potentials of static program analyses based on respectively closure analysis and type inference.