Abstraction barriers and refinement in the polymorphic lambda calculus

• Main Author: Hannay, Jo E.
• Other Authors: Sannella, Donald. : Hofmann, Martin
• Published: University of Edinburgh 2001
• Subjects: 515.15
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561785

This thesis examines specification refinement in the setting of polymorphic type theory and a complementary logic for relational parametricity. The starting point is the specification of abstract data types as done in the discipline of algebraic specification. Here, algebras are seen to match the standard notion of data type, i.e., a data representation together with operations on that data representation. An abstract data type is then a collection of data types sharing some well-defined abstract properties. In algebraic specification, these properties are specified algebraically by axioms in some suitable logic. Specification refinement then encompasses the idea that high-level specifications may be stepwise refined to executable programs that satisfy the initial specification; all in the framework of formal language and logic. This makes certain aspects of program development amenable to formal, computer-aided proofs of correctness. On the other hand, the discipline of type theory, lambda calculus, and its semantics is the prime field for research on programming languages. This framework is capable of characterising essentially any existing sequential programming-language feature, also advanced features such as recursive types, polymorphism and class-based object orientation. Furthermore, type theory provides a powerful framework for mechanised reasoning. This thesis is a contribution to lifting the idea of algebraic specification refinement into the more powerful domain of type theory and lambda calculus, thus giving the opportunity to expand in a sensible way a traditionally first order and functional framework to a wider range of programming aspects. We take a particular account of specification refinement and express it in a type-theoretic setting consisting of the polymorphic lambda calculus and a logic for relational parametricity. Key elements of algebraic specification are internalised in the syntax, e.g., data types viz. algebras are inhabitants of existential type, the latter providing essential data abstraction. For data types with only first-order operations, this setting automatically resolves certain issues of specification refinement, such as observational equivalence, stability and input sorts. After establishing a correspondence at first order, thus implanting the idea of algebraic specification refinement into the type-theoretic setting, the scene is set for lifting the idea of algebraic specification refinement to any number of programming features. In this thesis we focus on the generalisations to higher-order functions and to polymorphism. A simulation relation between two data types is a relation between their data representations that is preserved by their respective sets of operations. Using simulation relations is a classical way of explaining data refinement and observational equivalence. This combines with specification refinement to form specification refinement up to observational equivalence. With higher-order operations, however, we encounter in the logic a phenomenon related to what happens on the semantic level, i.e., the standard notion of refinement relation in the form of logical relations does not compose and the correspondence with observational equivalence is lost. In the logic it turns out that the standard notion of simulation relation fails to take into account a certain aspect of the abstraction barrier provided by existential types. We remedy this by proposing an alternative notion of simulation relation that observes this abstraction barrier more closely. We do this in two related ways; one relates to syntactic models while the other relates to a non-syntactic PER-model more apt for interpretive investigations. In algebraic specification, there is a universal proof method for specification refinement up to observational equivalence. This method can be imported soundly into the type-theoretic setting by asserting certain axioms. At first order, showing soundness for these axioms is straight-forward w.r.t. the standard parametric PER model for the logic. At higher order there are two problems. First, these axioms seemingly do not hold in the standard model. Secondly, the axioms speak in terms of simulation relations. At higher order, it is pertinent to have versions of the axioms featuring the abstraction barrier-observing simulation relations above, and to prove soundness for these poses an additional challenge. We show that the pure higher-order aspect of this problem can be solved by giving a setoid-based semantics. For the remaining task, we continue working from the observation that standard definitions do not observe abstraction barriers closely enough. Hence, we propose an alternative interpretation into the PER-model for data types that captures the abstraction barrier provided by existential types. The main contribution of this thesis is thus in generalising a prominent account of specification refinement to higher order and polymorphism via type theory incorporating relational parametricity. We also shed light on short-comings in the logic, as well as in the standard semantics, regarding the abstraction barrier provided by existential types. Two central contributions, namely abstraction barrier-observing simulation relations and abstraction barrier-observing semantics for data types, are the result of observing these short-comings. Finally, the work in this thesis also lays a foundation on which to adapt specification refinement to an object-oriented setting, because the theoretical concepts underlying object orientation can be seen as extensions of those for abstract data types.