Boolean Constraints for Binding-Time Analysis

Abstract

To achieve acceptable accuracy, many program analyses for functional programs are “property polymorphic”. That is, they can infer different input-output relations for a function at separate applications of the function, in a manner similar to type inference for a polymorphic language. We extend a property polymorphic (or “polyvariant”) method for binding-time analysis, due to Dussart, Henglein, and Mossin, so that it applies to languages with ML-style type polymorphism. The extension is non-trivial and we have implemented it for Haskell. While we follow others in specifying the analysis as a non-standard type inference, we argue that it should be realised through a translation into the well-..