SAFETY ANALYSIS VERSUS TYPE INFERENCE

Safety analysis is an algorithm for determining if a term in an untype d lambda calculus with constants is safe, i.e., if it does not cause a n error during evaluation. This ambition is also shared by algorithms for type inference. Safety analysis and type inference are based on ra ther different perspectives, however. Safety analysis is global in tha t it can only analyze a complete program. In contrast, type inference is local in that it can analyze pieces of a program in isolation. In t his paper we prove that safety analysis is sound, relative to both a s trict and a lazy operational semantics. We also prove that safety anal ysis accepts strictly more safe lambda terms than does type inference for simple types. The latter result demonstrates that global program a nalyses can be more precise than local ones. (C) 1995 Academic Press, Inc.