| Abstract: |
Logical relations are a fundamental and powerful tool for reasoning
about programs in languages with parametric polymorphism. Logical
relations suitable for reasoning about observational behavior in
polymorphic calculi supporting various programming language features
have been introduced in recent years. Unfortunately, the calculi
studied are typically idealized, and the results obtained for them
offer only partial insight into the impact of such features on
observational behavior in implemented languages. In this paper we
show how to bring reasoning via logical relations closer to bear on
real languages by deriving results that are more pertinent to an
intermediate language for the (mostly) lazy functional language
Haskell like GHC Core. To provide a more fine-grained analysis of
program behavior than is possible by reasoning about program
equivalence alone, we work with an abstract notion of relating
observational behavior of computations which has among its
specializations both observational equivalence and observational
approximation. We take selective strictness into account, and we
consider the impact of different kinds of computational failure,
e.g., divergence versus failed pattern matching, because such
distinctions are significant in practice. Once distinguished, the
relative definedness of different failure causes needs to be
considered, because different orders here induce different
observational relations on programs (including the choice between
equivalence and approximation). Our main contribution is the
construction of an entire family of logical relations, parameterized
over a definedness order on failure causes, each member of which
characterizes the corresponding observational relation. Although we
deal with properties very much tied to types, we base our results on
a type-erasing semantics since this is more faithful to actual
implementations.
|