On the Equivalence of Data Representations

John C. Mitchell

Computer Science Department Stanford University Stanford, California 94305

1 Introduction

One goal of the mathematical theory of computation outlined in John McCarthy’s influential papers [McC61, McC63] is to provide methods for proving equations between procedures, and other computational processes. While equality is straightforward for natural numbers, strings, or first-order functions on these sets, equality is not as easily characterized for higherorder functions or user-defined types. This chapter is concerned with equivalence of data representations, which might also be called implementations of abstract data types. For example, we might be interested in two representations of lists, where each “representation” includes both the way that lists themselves are stored in memory and the implementations of the basic operations on lists. We assume that lists are only manipulated by a designated set of operations, such as nil, cons, and cdr, and consider two lists equal if they cannot be distinguished by these operations. A very natural way to show that two representations are equivalent is to find a relation that is preserved by corresponding list operations. We explore this idea using relations between semantic interpretations of a simple, illustrative programming language. We prove that the existence of a certain kind of relation is sufficient to guarantee equivalence of data representations, and necessary if all the operations are first-order. This justifies a method for proving the equivalence of data representations that could be incorporated into a formal logic.

We begin by considering equivalence for data representations that are provided as part of the semantics of the language (“by the compiler”) and then extend the analysis to data representations defined within a simple function calculus. Although some of the development could be carried out without assuming each expression has a unique type, both the informal discussion and the technical development are simplified by working with a typed language.

The closest precurser to this chapter is [Rey83], with the earliest directly related work appearing in [Mil71, Hoa72]. This chapter is in part based on the conference abstract [Mit86], which used a more complicated language and a more cumbersome technical setting. The form of semantics and relation used here are based on joint work with Andre Scedrov, reported in [AMSW91], reformulated for the specific purpose of this paper and with as much category theory removed as possible. Some other studies that are related to the general method used here, but not specifically concerned with data representations, are [BTC88, MM85].

2 Observable Values and Equivalence

We may define equivalence for any type of value by identifying a set of observable values. For concreteness, we will use the natural numbers as observables. There is no loss of generality in sticking to the natural numbers, since virtually any other set with a print representation for each element, and equality decidable from print representations, would give us the same form of equivalence. In particular, assuming that natural number equality is definable by a function of type nat × nat → bool, we would get exactly the same equivalence relation if we used booleans instead of natural numbers. Having selected some set of observable values, we concentrate on programs that produce observables. To make this decision into a definition, we say that an expression M is a program if M is closed (has no free variables) and the type of M is the type nat of natural numbers. In other words, a program is any expression that can be evaluated by itself, without requiring additional values for undeclared variables, and any result of evaluation is observable.

We now define equivalence using the notion of program context. A context C[ ] is an expression with a “hole,” indicated by empty square brackets. We place an expression or program phrase in a context merely by inserting the expression into the place marked by empty square brackets, without renaming to avoid capture of free variables. For example, if we place the variable x in context λx: nat. [ ] + 3, we obtain the closed lambda expression λx: nat. x + 3. We say expressions M and N (of the same type) are observationally equivalent if, for every context C[ ] such that both C[M] and C[N] are programs, we have C[M] = C[N]. In writing this, we assume for simplicity that a divergent program has a semantic value (such as ∞), so that C[M] = C[N] means C[M] halts iff C[N] does, and if they both halt they produce the same observable value. We will usually abbreviate observational equivalence to equivalence, except when making a comparison with other forms of equivalence.

It is easy to see that observational equivalence is the maximal equivalence relation that is both a congruence relation on expressions and the identity relation on the natural numbers (or other chosen observables). Specifically, if we equate two expressions M and N that are not observationally equivalent, this forces us to equate two distinct natural numbers, C[M] and C[N]. For this reason, observational equivalence is the strongest “natural” form of equivalence between program constituents.

3 Function Equivalence

The main topic of this chapter is equivalence of data representations, which consist of one or more types and functions. Since this includes function equivalence as a special case, we begin with a discussion of function equivalence. This gives us an opportunity to make some observations that apply generally to functions and other kinds of computable values, and also to point out some of the difficulties associated with equivalence of higher-order functions.

Although the definition of observational equivalence in Section 2 is compelling, the definition is not directly useful in practical situations. If we are given two function expressions, M and N, the definition says they are equivalent if every program containing M has the same observable behavior as the program obtained by replacing M with N. However, to prove M and N equivalent directly, we would have to consider all programs that contain one function expression or the other. This includes programs that are far more complicated than either M or N. We are also led to think about program texts rather than properties of the functions defined by M or N.

A sufficient condition for function equivalence is extensional equality, namely, for every possible argument, each function has the same value. For first-order functions on observables, extensional equality coincides with observational equivalence. However, the two may differ at higher types. The reason is that extensional equality of function expressions M and N depends on the domain we ascribe to each. For higher-order functions, we may choose a domain that contains arbitrary functions (as in oracle computation), computable functions (and there are various definitions of higher-order computability), or other classes of functions that contain the computable ones but that might have more convenient mathematical characterizations (such as continuous functions over one of various kinds of ordered structures). Since these three choices give different notions of extensional equality, they cannot all coincide with observational equivalence.

One approach to higher-order function equivalence is to construct a semantic model in which extensional equality coincides with observational equivalence. This has been pursued to some depth in the literature. A model with this property is said to be fully abstract [Mil77, Plo77, Sto88]. Except for syntactic constructions, which usually are not very informative, fully abstract models are generally difficult to come by. In fact, under certain assumptions about the desired form of model, some languages provably do not have fully abstract models. (See [Sto88] for examples and general discussion.)

In this chapter, we will not attempt to characterize observational equivalence for higher-order functions. Instead, we characterize equivalence of data representations in a way that approximates observational equivalence in general, but is only exact when all the functions on the given data type are first-order. This seems the best we could hope for without introducing some of the more specialized and complex techniques used to construct fully abstract models of particular programming languages.

4 Typed Lambda Calculus

4.1 Syntax

We begin with a simple typed lambda calculus, adding data-type declarations in a later section. Although simple typed lambda calculus has no mechanism for declaring types, we may consider the effect of changing the interpretation of basic types. This leads to a theorem with a useful corollary for languages with data-type declarations.

The types of the language we will call λ^{1,×,→} are given by the grammar,

τ :: = a | τ × τ | τ → τ,

where a may be any type constant. It will be technically convenient to assume we have a type constant 1 for the one-element type. In words, τ_{1} × τ_{2} is the cartesian product of τ_{1} and τ_{2}, and τ_{1} → τ_{2} is the type of functions from τ_{1} to τ_{2}.

A signature for typed lambda calculus is a set of type constants and a set of term constants, with each term constant given a unique type. The type of a term constant may only contain the type constants of the signature.

The terms (or expressions) are outlined by the following grammar. More precisely, the terms of the language are all expressions generated by this grammar that are type correct:

M :: = c | x | ⟨M, M⟩ | Proj_{i}M | λx: τ.M | MM.

Here c may be any term constant of the signature and x a term variable. In words, ⟨M_{1}, M_{2}⟩ is the pair whose first and second components are selected by applying Proj_{1} and Proj_{2}. Pairs have their standard cartesian product types. The expression λx: τ.M defines a function from type τ to τ′, where τ′ is the type of function body M under the assumption that variable x has type τ. For example, λx : int.x + 3 would have type int → int. Function application M_{1}M_{2} is written as juxtaposition.

The type of a term with free variables depends on the context in which it occurs, since the term variables themselves do not have any fixed type. (We could assume that each term variable has a fixed type, but this would lead to technical problems when we add type declarations.) A typing context Γ is a set Γ = {x_{1} : σ_{1},…, x_{k} : σ_{k}} of pairs associating at most one type to each variable. We write Γ ▷ M : σ to indicate that term M has type σ in context Γ. Precise typing rules are given in the Appendix.

4.2 Semantics of Simple Typed Lambda Calculus

There are several ways of defining models of typed lambda calculus, notably Henkin models and the more general framework of cartesian closed categories [Bar84, LS86, MS89, Mit90]. We will use a style of model that does not appear elsewhere in the literature (as far as the author knows) but lies somewhere between Henkin models and cartesian closed categories. The reason for choosing this form of model is so that various constructions that do not produce Henkin models yield models. In particular, we want the family of relations between two models to be a model so that we can prove properties of the meaning of a term in the structure of relations. This may be done using cartesian closed categories, since our definition of model is equivalent to cartesian closed category, but the categorical approach requires extra machinery (the global section functor into Set) and would exclude the reader unfamiliar with category theory. A general categorical treatment of models and relations is given in [AMSW91].

A semantic structure, or model, will consist of a family of sets, each the set of values of some type. In a Henkin model, cartesian product types are interpreted as sets of ordered pairs, function types as a set of functions, and so on. To obtain a more general class of structures, we will only require certain operations that allow us to manipulate elements of cartesian product type as if they were actually pairs, and similarly for other types.

A λ^{→}-structure A consists of the following parts:

(i) a set U^{A}, called the universe of A, including a distinguished element

1^{A} ∈ U^{A} and, for each A, B ∈ U^{A}, elements A ×^{A} B and A →^{A} B;

(ii) for each type (member of the universe) A ∈ U^{A}, a set [A] of elements of A and for every A, B ∈ U^{A}, an application function Apply^{A,B} : [A →^{A} B] ×[A] → [B] so that each element of a function type A →^{A} B determines a function from A to B;

(iii) for each A ∈ U^{A}, a chosen identity element Id^{A} ∈ [A →^{A} A], representing the identity function, i.e., Apply Id x = x for every x ∈ [A],

and for every A, B, C ∈ U^{A}, f ∈ [A →^{A} B] and g ∈ [B →^{A} C], a specific

element (g ∘ f) ∈ A →^{A} C, called the composition of f and g, with the property that Apply (g ∘ f) x = Apply g (Apply f x) for every x ∈ [A].

These must satisfy the three conditions below. For notational convenience, we omit the square brackets and write a ∈ A instead of a ∈ [A] to indicate that a is an element of type A:

(iv) for each A ∈ U^{A}, the type A →^{A} 1 has one element;

(v) for all A, B, C ∈ U^{A}, there is a bijective correspondence,

[A →^{A} B] ×[A →^{A} C] ≅ [A →^{A} (B ×^{A} C)],

with the property that the map from right to left is given by com-

position with projections Proj_{1}^{A,B} ∈ (A ×^{A} B) →^{A} A and Proj_{2}^{A,B} ∈

(A ×^{A} B) →^{A} B. If f ∈ A →^{A} B and g ∈ A →^{A} C, we write ⟨f, g⟩ for the

corresponding element of A →^{A} (B ×^{A} C);

(vi) for all A, B, C ∈ U^{A}, there is a bijective correspondence,

[(A ×^{A} B) →^{A} C] ≅ [A →^{A} (B →^{A} C)],

with the map from right to left sending f to

App^{B,C} ∘ ⟨f ∘ Proj_{1}^{A,B}, Proj_{2}^{A,B}⟩

for some fixed App^{B,C} ∈ ((B →^{A} C) ×^{A} B) →^{A} C.

Although identity and composition are not determined by application in an

arbitrary structure, they are in the special case that A ×^{A} B is the ordinary cartesian product of A and B, A →^{A} B is a set of functions from A to B, and Apply ⟨f, x⟩ = f(x). It is a general result of category theory that once we choose identity and composition, the interpretation of product and function types is uniquely determined (up to bijective correspondence).

An interpretation I of a signature into a structure A is a map from type constants to U^{A} and term constants to elements of U^{A} such that I(c) is an element of the right type (explained below). The map from type constants to U^{A} gives us a straightforward interpretation I[[σ]] of type expression σ. The map from term constants to elements of U^{A} must map a constant c: τ to an element of I[[1 → τ]]. It follows that if c is a term constant of type τ, then I determines an element of I[[τ]] by application.

The meaning of a term under an interpretation I is defined inductively. The meaning of a term Γ ▷ M : σ, which is typed under assumption Γ = {x_{1} : σ_{1},…, x_{k}: σ_{k}}, will be an element of I[[σ_{1} ×… × σ_{k} → σ]]. A minor change of notation will make this easier to define. Below, we will write a typing context {x_{1} :σ_{1},…, x_{k}:σ_{k}} in the form x̄:σ̄, where x̄ = x_{1},…, x_{k} and σ̄ = σ_{1},…, σ_{k}. We will also overload notation and write σ̄ for the type σ_{1} ×… × σ_{k}, with × associated to the right. If σ̄ is the empty sequence, then the corresponding type is σ̄ = 1. In addition, for every type σ̄ and integer i < k, we will write Projσ̄ ; i,k for the composition of projection functions, Projσ̄ ; i,k ∈ I[[σ̄ → σ_{i}]], giving the ith component of any sequence, ⟨x_{1}, ⟨x_{2},…, x_{k}⟩⟩ ∈ I[[σ̄]]. The meaning I[[x̄: σ̄ ▷ M : τ]] of a well-typed term is now defined by the following inductive clauses:

I[[x̄: σ̄ ▷ x_{i} : σ_{i}]]  = Projσ̄ ; i,k
I[[x̄: σ̄ ▷ c: τ]]  = I(c) ∘ Oσ̄, where Oσ̄ is the unique

element of I[[σ̄ → 1]]

I[[x̄: σ̄ ▷ Proj_{1}^{σ,τ} M : σ]] = Proj_{1}^{σ,τ} ∘ I[[x̄: σ̄ ▷ M : σ × τ]]
I[[x̄: σ̄ ▷ Proj_{2}^{σ,τ} M : τ]] = Proj_{2}^{σ,τ} ∘ I[[x̄: σ̄ ▷ M : σ × τ]]
I[[x̄: σ̄ ▷ ⟨M, N⟩: ρ × τ]] = the unique p ∈ I[[σ̄ → ρ × τ]] such

that Proj_{1}^{σ,τ} ∘ p = I[[x̄: σ̄ ▷ M : σ]] and Proj_{2}^{σ,τ} ∘ p = I[[x̄: σ̄ ▷ N : τ]]

I[[x̄: σ̄ ▷ MN : τ]]  = App^{σ,τ} ∘

⟨I[[x̄: σ̄ ▷ M : σ → τ]], I[[x̄: σ̄ ▷ N : σ]]⟩

I[[x̄: σ̄ ▷ λy : ρ.M : ρ → τ]] = the unique f ∈ I[[σ̄ → ρ → τ]] such
that ∀d ∈ I[[σ̄ → ρ]], App ∘ ⟨f, d⟩
= I[[x̄: σ̄, y : ρ ▷ M : τ]] ∘ ⟨Idσ̄, d⟩

5 Data Representations Determined by the Compiler

5.1 An Example: Integer Multisets

Two compilers or interpreters for a programming language would generally be considered equivalent if every program produces identical results on either one. We will examine implementation equivalence by considering alternative interpretations of multisets of natural numbers. Let Σ be the signature with base types nat (for natural numbers) and ms (for multisets), and term constants for arithmetic and multiset operations:

0, 1 : nat
+ : nat → nat → nat
empty : ms
insert : nat → ms → ms
count : ms → nat → nat

Informally, empty is the empty multiset, insert adds an element to a multiset, and count returns the multiplicity of a multiset element.

Since we consider natural numbers the “observable output,” we will assume that each model interprets nat as the standard natural numbers. For the purposes of this discussion, we define an implementation for Σ to be an interpretation I such that I(nat) = N and I(0), I(1), I(+) are standard, but the interpretation of ms and operations empty, insert, count are arbitrary. The set N may be either the standard natural numbers, if we are not concerned with nonterminating expressions, or N ∪ {∞} as mentioned earlier. However, we must use the same set in all the interpretations we wish to compare.

We say that implementations I and J for Σ are observationally equivalent if, for any program M : nat, we have

I[[M : nat]] = J [[M : nat]],

that is, the meaning of M : nat in I is the same as the meaning of M : nat in J. The rest of this section is devoted to characterizing observational equivalence of implementations.

A first guess might be that I and J are observationally equivalent iff there exists some kind of mapping between multisorted first-order structures,

⟨N , I(ms), 0, 1, +, I(empty), I(insert), I(count)⟩

and

⟨N , J (ms), 0, 1, +, J (empty), J (insert), J (count)⟩,

such as a homomorphism. This is partly correct, since a first-order homomorphism determines the kind of relation discussed in Section 5.2 below, and therefore guarantees equivalent results for any program. However, there are two reasons why homomorphisms are not an exact characterization. The first has to do with the fact that elements of I(ms) and J (ms) that are not definable by terms are irrelevant. For example, let I be an implementation of multisets and let J be derived from I by adding some “nonstandard” multiset a with the property,

insert x a = a for all x.

Then I and J will be observationally equivalent, since the multiset a is not definable by any expression. However, there can be no homomorphism h from J to I, since there is no reasonable choice for h(a).

A second reason why homomorphisms are unsatisfactory is that an implementation may choose to represent indistinguishable multisets, produced by different orders of insertion, as either the same or different data structures. For example, an implementation may be structured so that the result of inserting 1, 2, and 3 into the empty multiset is precisely the same data structure as the result of inserting 1, 2, and 3 into the empty multiset, but the results of inserting 4, 5, 6 and 6, 5, 4 are different. If a second implementation does just the opposite, then there cannot be a homomorphism from one implementation to the other, even though the two implementations may be indistinguishable.

5.2 Relations for Simply Typed Structures

The discussion in the previous section suggests that we should try to characterize equivalence of implementations using relations rather than homomorphisms or other kinds of functions. In this section, we will define a form of relation between structures that serves this purpose.

A typed relation between structures A and B is a family of relations between the sets of U^{A} and U^{B}. With application and other operations inherited from A and B, the collection of all relations becomes a structure. We define the relational structure Rel(A, B) by:

• The universe U^{Rel(A,B)} is the set of all triples ⟨R, A, B⟩ with A ∈ U^{A} and B ∈ U^{B} and R ⊆ [A] ×[B] a binary relation on the cartesian product of their elements.

• The set [⟨R, A, B⟩] of elements of ⟨R, A, B⟩ is the set R of ordered pairs. Application is determined coordinatewise by Apply ⟨f, g⟩ ⟨x, y⟩ = ⟨Apply f x, Apply g y⟩.

• The distinguished element 1^{Rel(A,B)} is the triple ⟨id, 1^{A}, 1^{B}⟩ where

id ⊆ 1^{A} × 1^{B} is the identity relation. We define ×^{Rel} and →^{Rel} by

⟨R, A, B⟩ ×^{Rel} ⟨R′, A′, B′⟩ = ⟨R × R′, A ×^{A} A′, B ×^{B} B′⟩,

⟨R, A, B⟩ →^{Rel} ⟨R′, A′, B′⟩ = ⟨R → R′, A →^{A} A′, B →^{B} B′⟩,

with relations R × R′ and R → R′ as follows:

⟨a, a′⟩ R × R′ ⟨b, b′⟩ iff a R b and a′ R′ b′,
f R → R′ g  iff (Apply^{A,B} f a) R′ (Apply^{A′,B′} g b)

whenever a R b.

• Composition of ⟨f, g⟩ ∈ ⟨R, A, B⟩ →^{Rel} ⟨R′, A′, B′⟩ and

⟨f′, g′⟩ ∈ ⟨R′, A′, B′⟩ →^{Rel} ⟨R′′, A′′, B′′⟩ is defined by

⟨f′, g′⟩ ∘ ⟨f, g⟩ = ⟨f′ ∘ f, g′ ∘ g⟩,

and distinguished elements are defined by pairing. For example, Id^{⟨R,A,B⟩} = ⟨Id^{A}, Id^{B}⟩.

We claim below that Rel(A, B) is a structure.

The structure Rel(A, B) gives us a way of defining relations between interpretations into A and B. If I is an interpretation of some signature into structure A, and J is an interpretation of the same signature into B, then an interpretation K of this signature into Rel(A, B) gives us a relation K[[τ]] for each type τ. We say K is compatible with I and J if, for each type constant a, we have K(a) ⊆ I(a) × J (a) and, for each term constant c of type τ, the interpretations I(c) and J (c) are related by K[[1 → τ]]. We will see below that a compatible interpretation K gives us a relation K[[τ]] between I[[τ]] and J [[τ]] for each type τ. This relation has the same properties as a logical relation between the I and J. (See [Sta85, Mit90].) One advantage of the present framework, as opposed to previous approaches to logical relations, is that we can see that relations at functional and product type are uniquely determined, and not the result of some arbitrary decision. This follows from Lemma 1 and the categorical fact mentioned earlier that product and function types are uniquely determined.

The following lemma, adapted from [AMSW91], implies the Basic Lemma of logical relations (also called the “Fundamental Theorem”) [Sta85, Mit90].

Lemma 1 For any λ^{1,×,→} structures A and B, Rel(A, B) is a λ^{1,×,→} structure. If I is an interpretation of some signature into A, and J is an interpretation of the same signature into B, then for any compatible interpretation K into Rel(A, B), we have K[[τ]] ⊆ I[[τ]] × J [[τ]] for each type τ and

K[[x̄: σ̄ ▷ M : σ]] = ⟨I[[x̄: σ̄ ▷ M : σ]], J [[x̄: σ̄ ▷ M : σ]]⟩ ∈ K[[σ̄ → σ]]

for each term x̄: σ̄ ▷ M : σ.

Proof Sketch. It is straightforward to check that Rel(A, B) is a structure. The remaining claims are verified by induction on types and terms.

5.3 Equivalence of Implementations

We may show that interpretations I (into A) and J (into B) for the signature with natural number multisets are observationally equivalent (with respect to the natural numbers) iff there is a compatible interpretation K into Rel(A, B) such that K(nat) is the identity relation on the natural numbers. This generalizes to any other data type, or collection of related data types, as long as all functions are first-order and we have a closed term naming each natural number. If we have higher-order functions, then the existence of a relation (or compatible interpretation into Rel(A, B)) is sufficient but not necessary. The general situation is summarized in the following theorem about any signature giving a collection of possibly interdependent types and operations.

Theorem 1 Let Σ be some signature with type constant nat and let I and J be interpretations of Σ into structures A and B, respectively, with I(nat) = J (nat) = N. If there is a compatible interpretation K of Σ into Rel(A, B), with K(nat) the identity relation on natural numbers, then I and J are observationally equivalent. Conversely, if I and J are observationally equivalent, Σ provides a closed term for each element of N, and Σ only contains first-order functions, then there is a compatible interpretation K of Σ into Rel(A, B), with K(nat) the identity relation.

Proof. The first part of the theorem follows directly from Lemma 1. For the proof of the second part, we must construct a compatible interpretation K. For each type constant s, we let K(s) ⊆ I(s) × J (s) be the relation containing pair ⟨a, b⟩ iff there is a closed term M of type s whose meaning under I is a (or, to be precise, the constant function from 1^{A} to I[[s]] whose value is a), and whose meaning under J is b. We must show that for any function symbol f : s_{1} ×… × s_{k} → s from Σ, if ⟨a_{i}, b_{i}⟩ ∈ K(s_{i}) for i = 1,…, k, then ⟨f^{I}(a_{1},…, a_{k}), f^{J} (b_{1},…, b_{k})⟩ ∈ K(s); but this follows easily from the choice of K(s). Since Σ provides a closed term for each element of N, it is easy to see that K(nat) is the identity relation.

6 Data-type Declarations

6.1 A Lambda Calculus with Type Declarations

In this section and the remainder of the chapter, we will study equivalence of data-type representations when written in a simple illustrative language. The first step is to extend the simple lambda calculus λ^{1,×,→} to a language λabstype with abstract data-type declarations. The declaration form, abstype t with x: σ is ⟨τ, M⟩ in N, gives names t and x to the type τ and operation M, with scope N. Since we have arbitrary pairing, there is no loss of generality in assuming only one operation. For example, we might declare and use a data type with one constant and one unary operation by writing

abstype t with x: t ×(t → t) is ⟨τ, M⟩ in N,

where within the scope N, the constant is given by Proj_{1}x and unary operation by Proj_{2}x. There are several typing constraints associated with this construct, which is explained in detail in [MP88]. In abstype t with x: σ is ⟨τ, M⟩ in N, the type of M must be the result [τ/t]σ of substituting τ for t in σ, N must be well-typed under the assumption that x has type σ, and t may not occur in the type of any free variable of N other than x. This means that the only operations on type t in N are those provided by x. The type variable t also must not be free in the type of N. This is an important scoping restriction in extensions of the language, which plays a minor technical role here. Note that while many studies of data types have been limited to first-order functions over some carrier, the operations associated with data types in this language may be higher-order.

To define λabstype more precisely, we begin by extending the type expressions of λ^{1,×,→} with type variables, so that type expressions have the form,

τ :: = a | t | τ × τ | τ → τ,

with a any type constant and t any type variable. We continue to assume that 1 is among the type constants.

A signature for λabstype is again a set of type constants and typed term constants, with a variable-free type designated for each term constant. The terms, which now include abstype, are summarized by the grammar,

M :: = c | x | ⟨M, M⟩ | Proj_{i}M | λx: τ.M | MM |

                abstype t with x: σ is ⟨τ, M⟩ in N,

with the additional typing rule for abstype given in the Appendix. We will call an expression ⟨τ, M⟩ a data representation, since this is a concrete representation of an abstract data type.

6.2 Meaning in λ^{1,×,→} Structure

We will consider two semantic interpretations for λabstype, a simpler one in this section and a more detailed semantics incorporating explicit dependence on free type variables in the next. In the first semantics, we use λ^{1,×,→} structures, with the meaning of a type depending on an assignment of semantic types to type variables.

An interpretation I of a λabstype signature into a λ^{1,×,→} structure A is a map from type constants to the universe of A and from term constants and types of A to elements of the appropriate type. If A is a structure, then an A type environment is a mapping,

η : Type Variables ⟶ U^{A}.

The meaning I[[σ]]η of any type expression σ in type environment η is defined as follows:

\begin{aligned}I[[t]]η & = & η(t) \\ I[[a]]η & = & I(a) \\ I[[σ × τ]]η & = & I[[σ]]η ×^{A} I[[τ]]η \\ I[[σ → τ]]η & = & I[[σ]]η →^{A} I[[τ]]η \end{aligned}

The meaning of a term Γ ▷ M : σ in type environment η is defined by induction as before, except that we must remember to look up the value of each type variable in the type environment. Since all cases other than abstype are completely routine, we give only a few examples:

I[[x̄: σ̄ ▷ x_{i} : σ_{i}]]η = Proj_{i,k}^{I[[σ̄]]η}
I[[x̄: σ̄ ▷ c: τ]]  = I(c) ∘ O^{I[[σ̄]]η}, where O^{I[[σ̄]]η}

is the unique element of I[[σ̄ → 1]]η

I[[x̄: σ̄ ▷ MN : τ]]η = App^{I[[σ]]η,I[[τ]]η}

∘⟨[[x̄: σ̄ ▷ M : σ → τ]]η, I[[x̄: σ̄ ▷ N : σ]]η⟩

The new case is the meaning of an abstype declaration. In words, the meaning of abstype t with x : σ is ⟨τ, M⟩ in N is obtained by composing the meaning of N, considered as a function of x, with the meaning of M, where the meaning of N is taken in a type environment that gives type variable t the meaning of τ:

I[[x̄: σ̄ ▷ abstype t with x: σ is ⟨τ, M⟩ in N : ρ]]η
= I[[x̄: σ̄, x: σ ▷ N : ρ]]η′ ∘ ⟨id, [[x̄: σ̄ ▷ M : [τ/t]σ]]η⟩,
where η′ = η[t ↦ I[[τ]]η].

An equation that holds in this semantics is

abstype t with x: σ is ⟨τ, M⟩ in N = [M/x][τ/t]N,

which will be useful in reducing observational equivalence for some special uses of abstype to the earlier analysis of observational equivalence for interpretations of λ^{1,×,→}. One aspect of this equation that deserves mention is the typing of the substitution instance [M/x][τ/t]N. If N is well-typed assuming x: σ, then it follows (see [Mit90], for example), that [τ/t]N will be well-typed under the assumption that x: [τ/t]σ. Since [τ/t]σ is precisely the type of M, the substitution instance [M/x][τ/t]N is well-typed.

6.3 Observational Equivalence

According to our general definition of observational equivalence, a pair ⟨τ, M⟩ implementing a type t with operation x: σ is equivalent to another such pair, ⟨ρ, N⟩, if for any natural number context C[ ] such that both C[⟨τ, M⟩] and C[⟨ρ, N⟩] are well-formed programs (closed expressions of type nat), we have C[⟨τ, M⟩] = C[⟨ρ, N⟩]. It is clear from the grammar for the language that any such context C[ ] must have the form,

C : : = … abstype t with x: σ is [ ] in P … By the previous analysis involving relations, we would expect to show C[⟨τ, M⟩] = C[⟨ρ, N⟩] by establishing that for all relevant values of the free type and term variables in P, ⟨τ, M⟩ and ⟨ρ, N⟩, the interpretation of

abstype t with x : σ is ⟨τ, M⟩ in P is related to abstype t with x :

σ is ⟨ρ, N⟩ in P. Since this is considerably simplified if either ⟨τ, M⟩ and ⟨ρ, N⟩ are closed, or we know the values of their free variables, we will consider these special cases first. These can be addressed using the semantics given above, while the more general situation requires the more complex semantics given in Section 7.

6.4 A Single Closed Data Representation

The simplest form of program context with a hole requiring a data representation is

            C[ ] : : = abstype t with x: σ is [ ] in P,

where in order for C[⟨τ, M⟩] to be a program (closed nat expression), τ and M must be closed and P may only have t and x free. Since an abstype declaration within P could be eliminated by substitution, we may assume without loss of generality that P does not contain abstype. We will say that data representations ⟨τ, M⟩ and ⟨ρ, N⟩ are top-level observationally equivalence with respect to I and J if I[[C[⟨τ, M⟩]]] = J [[C[⟨ρ, N⟩]]] for all contexts of the form indicated above. In practical situations, we are probably most interested in the case where I = J, since this corresponds to rewriting a data representation without changing the compiler or interpreter. However, if we consider sequences of nested declarations, we are naturally led to compare data representations with respect to difference interpretations.

Using extensions of interpretations I and J, we may reduce top-level equivalent with respect to I and J to observational equivalence of λ^{1,→,×} interpretations. If I is an interpretation for signature Σ not containing type constant a or term constant f, then we can use ⟨τ, M⟩ to define an extension I′ of I to signature Σ′ = Σ ∪ {a, f : [a/t]σ} with

I[[abstype t with x: σ is ⟨τ, M⟩ in P]] = I′[[[f/x][a/t]P]]

for any expression P with t and x: σ free. The interpretation I′ is defined from I by letting I′(a) = I[[τ]] and I′(f) = I[[M]]. To establish notation, let us write I′ = I[ a ↦ I[[τ]], f ↦ I[[M]] ]. If J is an another interpretation for Σ, and ⟨ρ, N⟩ is another implementation for type t with operation x : σ, we may define an extension J′ similarly. By construction, ⟨τ, M⟩ and ⟨ρ, N⟩ are top-level observationally equivalent with respect to I and J iff extended interpretations I′ and J′ are observationally equivalent in the sense described in Section 4. This gives us the following corollary to Theorem 1.

Corollary 1 Let I and J be interpretations of signature Σ into A and B (respectively) and let ⟨τ, M⟩ and ⟨ρ, N⟩ be closed data representations for type t with x:σ. Then ⟨τ, M⟩ is top-level observationally equivalent to ⟨ρ, N⟩ with respect to I and J if there is an interpretation K of Σ′ = Σ ∪ {a, f : [a/t]σ} into Rel(A, B) that is compatible with I′ = I[a ↦ I[[τ]], f ↦ I[[M]]] and J′ = J [a ↦ J [[τ]], f ↦ J [[M]]] and such that K(nat) is the identity relation. If σ is a cartesian product of first-order function types, signature Σ provides a closed term for each element of N, and Σ only contains firstorder functions, then the converse also holds.

6.5 Sequences of Data Representations

The characterization of observational equivalence above generalizes easily to representations of several related data types. These often arise in programming, as in defining types of matrices and vectors over some ring. If we want a function to multiply a matrix by a vector, and define matrices and vectors as separate data types, there is no natural place to define the multiplication operation. This problem is solved by defining both as part of the same abstract data type (which has two types). While this is easily done in the language presented in [MP88], we cannot do this here without extending the language.

The more general form of abstract data type declaration is

abstype t_{1},…, t_{k} with x: σ is ⟨τ_{1},…, τ_{k}, M⟩ in P

where the type of M must be the result [τ_{1},…, τ_{k}/t_{1},…, t_{k}]σ of substituting each τ_{i} for t_{i} in σ. (In general, σ will contain all of the type variables t_{1},…, t_{k}.) It is easy to see that Corollary 1 extends to this form of datatype declaration and “multisorted” data representation ⟨τ_{1},…, τ_{k}, M⟩, since Theorem 1 applies to any λ^{1,×,→} signature with any number of type constants.

Another situation that arises quite often in practice is that a program will begin with a sequence of data-type declarations, each referring to one or more of the previous declarations. This results in a program of the form,

     abstype t_{1} with x_{1} : σ_{1} is ⟨τ_{1}, M_{1}⟩ in
            abstype t_{2} with x_{2} : σ_{2} is ⟨τ_{2}, M_{2}⟩ in

…

                   abstype t_{k} with x_{k} : σ_{k} is ⟨τ_{k}, M_{k}⟩ in

P

                   end
            end
     end,

where we have used end’s and indentation to indicate the scope of each declaration. Two sequences of data representations, ⟨τ_{1}, M_{1}⟩,…, ⟨τ_{k}, M_{k}⟩ and ⟨ρ_{1}, N_{1}⟩,…, ⟨ρ_{k}, N_{k}⟩, are top-level observationally equivalent if any program C[⟨τ_{1}, M_{1}⟩,…, ⟨τ_{k}, M_{k}⟩] of the form above has the same observable value as the program C[⟨ρ_{1}, N_{1}⟩,…, ⟨ρ_{k}, N_{k}⟩] with ⟨ρ_{i}, N_{i}⟩ in place of ⟨τ_{i}, M_{i}⟩. However, since each program is equivalent to one of the form,

abstype t_{1},…, t_{k} with x: σ_{1} ×… × σ_{k}
is ⟨τ_{1},…, τ_{k}, ⟨M_{1},…, M_{k}⟩⟩ in P,

observational equivalence for sequences of data representations reduces to observational equivalence for data representations with more than one type.

In addition, we may consider incremental changes in sequences of data representations. Suppose we have two sequences of data representations, τ̄ = ⟨τ_{1}, M_{1}⟩,…, ⟨τ_{k}, M_{k}⟩ and ρ̄ = ⟨τ_{1}, M_{1}⟩,…, ⟨τ_{k}, M_{k}⟩. Given the development so far, it is easy to establish that if τ̄ is observationally equivalent to ρ̄ and τ̄, ⟨τ_{k+1}, M_{k+1}⟩ is observationally equivalent to τ̄, ⟨ρ_{k+1}, N_{k+1}⟩, then τ̄, ⟨τ_{k+1}, M_{k+1}⟩ is observationally equivalent to ρ̄, ⟨ρ_{k+1}, N_{k+1}⟩.

7 Data Representations with Free Variables

7.1 Structures and Interpretations

The final problem is to give a sufficient condition for observational equivalence of data representations that may contain free type and term variables. To construct relations that illustrate the dependence on type variables explicitly, we will add explicit functions on types to structures. The interpretation of a type expression with n free variables will be an n-ary function from U^{A} to U^{A}. With each such function, we associate a set of elements also parameterized by n-tuples of types to serve as the meanings of terms. The meaning of a term x̄: σ̄ ▷ M : σ with free type variables t_{1},…, t_{n} will be a function that maps an n-tuple of values for t_{1},…, t_{n} to an element of σ̄ → σ.

With the extended form of structure, we can also extend the language to include type and term constants with type parameters. Some intuitive examples are the parameterized type list(t) of lists of type t and nil(t), the empty list of type list(t). To be precise, a signature consists of a set of type constants, each with a specific arity, and a set of term constants, each with a specified arity (number of type parameters) and a type depending on the same number of type parameters. Type expressions now have the form,

τ :: = a(t_{1},…, t_{n}) | t | τ × τ | τ → τ,

and terms have the form,

M :: = c(t_{1},…, t_{n}) | x | ⟨M, M⟩ | Proj_{i}M | λx: τ.M | MM |

            abstype t with x: σ is ⟨τ, M⟩ in N,

with precise typing rules again given in the Appendix.

A λabstype-structure A consists of the following parts:

(i) A λ^{1,×,→} structure A_{0}, consisting of universe U_{0}^{A}, distinguished el-

ement 1^{A} ∈ U_{0}^{A}, elements A ×^{A} B and A →^{A} B for each A, B ∈ U_{0}^{A}, and so on as in Section 4.

(ii) For each positive integer n, a collection U_{n}^{A} of n-ary functions from U_{0}^{A} to U_{0}^{A}, including the constant function mapping any n-tuple to 1^{A}, all n-ary projection functions, and such that if F and G are in

U_{n}^{A}, then so are the functions mapping n-tuple ū to F (ū) ×^{A} G(ū)

and F (ū) →^{A} G(ū). For notational simplicity, we write F ×^{A} G for the

function mapping ū to F (ū) ×^{A} G(ū), and similarly, F →^{A} G.

(iii) For each function F ∈ U_{n}^{A}, a set [F] of functions f with f(ū) ∈ [F (ū)].

The following conditions must be satisfied. Essentially, conditions (iv) and (v) say that each U_{n}^{A} is a λ^{1,×,→} structure. Condition (vi) gives us a way of treating any function of n type parameters as a function of n + m type parameters, and condition (vii) provides a semantic version of substitution of types for type variables in both types and terms. This is used to interpret abstype expressions.

(iv) For each F ∈ U_{n}^{A}, the parameterized identity Id^{F} given by Id^{F} (ū) =

Id^{F (ū)} must be in [F →^{A} F] and for each F, G, H ∈ U_{n}^{A}, f ∈ [F →^{A} G]

and g ∈ [G →^{A} H], the composition g ∘ f given by

(g ∘ f)(ū) = g(ū) ∘ f(ū)

must be in [F →^{A} H].

(v) For each n and F ∈ U_{n}^{A}, there is exactly one element in [F →^{A} λū.1^{A}] and for all F, G, H ∈ U_{n}^{A}, there must be bijective correspondences,

([F →^{A} G]) ×([F →^{A} H]) ≅ [F →^{A} (G ×^{A} H)],

[(F ×^{A} G) →^{A} H] ≅ [F →^{A} (G →^{A} H)],

with the maps from right to left determined by composition with

parameterized projections Proj_{1}^{F,G} ∈ [F ×^{A} G →^{A} F], Proj_{2}^{F,G} ∈ [F ×^{A}

G →^{A} G], and application App^{F,G} ∈ [(F →^{A} G) ×^{A} F →^{A} G].

(vi) If F ∈ U_{n}^{A} and G is an (n + m)-ary function on types that is identical to F except for m vacuous additional arguments, then G ∈ U_{n+m}^{A}. Similarly, if f ∈ [F] and function g of (n + m) arguments is identical to f except for m vacuous additional arguments, then g ∈ [G].

(vii) If F ∈ U_{n}^{A}, G ∈ U_{n+1}^{A} and g ∈ [G], then the composition G_{F} defined by G_{F} (ū) = G(ū, F (ū)) is in U_{n}^{A} and the composition g_{F} defined by g_{F} (ū) = g(ū, F (ū)) is in [G_{F}].

An interpretation I of a signature into a structure A is a map sending each type constant of arity n into U_{n}^{A} and each term constant c depending on n type parameters to an element of some [F] for appropriate F ∈ U_{n}^{A}. If a type constant a(t_{1},…, t_{n}) depends on n type parameters, then by condition (vi) we may also regard I(a) as a function of m + n type parameters. We write I(a)_{m+n} to indicate an appropriate element of U_{m+n}^{A}. Similarly, if c is a term constant depending on n type parameters with I(c) ∈ [F] for F ∈ U_{n}^{A}, then by condition (vi) there is a corresponding interpretation I(c)_{n+m} ∈ [G] for any G ∈ U_{m+n}^{A} depending vacuously on additional type parameters.

We interpret a type expression with n free variables, t_{1},…, t_{n} as a function in U_{n}^{A}. The definition of function I[[τ]]^{(t_{1},...,t_{n})} ∈ U_{n}^{A} may be given by a straightforward inductive definition. This gives the same result as defining I[[τ]]^{(t_{1},...,t_{n})} ∈ U_{n}^{A} to be the function,

⟨η(t_{1}),…, η(t_{n})⟩ ↦ I[[τ]]η,

where I[[τ]]η is the element of U^{A} determined as in Section 6, except for the addition of parameterized type constants discussed above. It is easy to verify inductively that I[[τ]]^{(t_{1},...,t_{n})} ∈ U_{n}^{A}.

We give meanings to terms without abstype similarly. If t_{1},…, t_{n} is a list containing all type variables in x̄: σ̄ ▷ M : τ, then the meaning,

I[[x̄: σ̄ ▷ M : τ]]^{(t_{1},...,t_{n})},

of this term with respect to these free variables is the function,

⟨η(t_{1}),…, η(t_{n})⟩ ↦ I[[x̄: σ̄ ▷ M : τ]]η,

where I[[x̄: σ̄ ▷ M: τ]]η is the element of I[[σ̄ → τ]]η determined as in Section 6. The only case that might be confusing is a term constant, since the form of interpretation has changed. For any c : τ and t_{1},…, t_{n} containing all type variables in τ, we let

I[[x̄: σ̄ ▷ c: τ]] = I(c)_{n} ∘ O^{I[[σ̄]]^{(t_{1},...,tn)}}, where O^{I[[σ̄]]^{(t_{1},...,tn)}} is the
unique element of I[[σ̄ → 1]]^{(t_{1},...,t_{n})}.

This gives us a function from types to values for any term not containing

abstype.

For abstype, we define the meaning of a term in a way that makes use of condition (vii) of the definition of structure. Note that this condition has not been used for other terms. To define I[[x̄: σ̄ ▷ abstype t with x: σ is ⟨τ, M⟩ in N : ρ]], let

\begin{aligned}F & = & I[[τ]]^{(t_{1},...,t_{n})} & ∈ & U_{n}^{A}, \\ G & = & I[[σ̄ × σ]]^{(t_{1},...,t_{n},t)} & ∈ & U_{n+1}^{A}, \\ g & = & I[[x̄: σ̄, x: σ ▷ N : ρ]] & ∈ & [G]. \end{aligned}

Then in the notation of condition (vii), we have

I[[x̄: σ̄ ▷ abstype t with x: σ is ⟨τ, M⟩ in N : ρ]]^{(t_{1},...,t_{n})}
= g_{F} ∘ ⟨Id^{H}, I[[x̄: σ̄ ▷ M : [τ/t]σ]]^{(t_{1},...,t_{n})}⟩,

where H(t_{1},…, t_{n}) = I[[σ̄]]^{(t_{1},...,t_{n})}. It is not hard to show by induction on terms that the meaning I[[x̄ : σ̄ ▷ M : τ]]^{(t_{1},...,t_{n})} of any term, considered as a function of its free type variables, is an element of the similarly parameterized meaning I[[σ̄ → τ]]^{(t_{1},...,t_{n})} of its type.

7.2 Relations

We may define a structure of relations between any pair of λabstype structures in a manner analogous to relational λ^{1,×,→} structures. Specifically, for λabstype structures A and B, we define Rel(A, B) as follows:

• For the required λ^{1,×,→} structure, we take Rel(A_{0}, B_{0}) with universe U_{0}^{Rel(A,B)} = U^{Rel(A_{0},B_{0})}.

• For each positive integer n, let U_{n}^{Rel(A,B)} be the set of all n-ary functions F from U_{0}^{Rel(A,B)} to U_{0}^{Rel(A,B)} for which there exist functions F_{A} ∈ U_{n}^{A} and F_{B} ∈ U_{n}^{B} such that if

F (⟨R_{1}, A_{1}, B_{1}⟩,…, ⟨R_{n}, A_{n}, B_{n}⟩) = ⟨R, A, B⟩

then A = F_{A}(A_{1},…, A_{n}) and B = F_{B}(B_{1},…, B_{n}). Note that F_{A} and F_{B} are uniquely determined by F.

• For all F ∈ U_{n}^{Rel(A,B)}, let [F] contain all functions f given by pairs f_{A} ∈ [F_{A}] and f_{B} ∈ [F_{B}] such that

f(⟨R_{1}, A_{1}, B_{1}⟩,…, ⟨R_{n}, A_{n}, B_{n}⟩)
= ⟨f_{A}(A_{1},…, A_{n}), f_{B}(B_{1},…, B_{n})⟩
∈ [F (⟨R_{1}, A_{1}, B_{1}⟩,…, ⟨R_{n}, A_{n}, B_{n}⟩)].

We define compatible interpretation into Rel(A, B) as in Section 4. In the following generalization of Lemma 1, we show that Rel(A, B) is a structure and describe the meaning of each term.

Theorem 2 For any λabstype structures A and B, Rel(A, B) is a λabstype structure. Let I be an interpretation of some signature into A, let J be an interpretation of the same signature into B, and let K be a compatible interpretation into Rel(A, B). For any type τ over type variables t_{1},…, t_{n}, K[[τ]]^{(t_{1},...,t_{n})} is a function with

\begin{matrix}K[[τ]]^{(t_{1},...,t_{n})}(⟨R_{1}, A_{1}, B_{1}⟩,…, ⟨R_{n}, A_{n}, B_{n}⟩) \\ ⊆ I[[τ]]^{(t_{1},...,t_{n})}(A_{1},…, A_{n}) × J [[τ]]^{(t_{1},...,t_{n})}(B_{1},…, B_{n}). \end{matrix}

In addition, for each λabstype term x̄: σ̄ ▷ M : σ, the meaning K[[x̄: σ̄ ▷ M : σ]]^{(t_{1},...,t_{n})} is determined by the pair I[[x̄: σ̄ ▷ M : σ]]^{(t_{1},...,t_{n})}, J [[x̄: σ̄ ▷ M : σ]]^{(t_{1},...,t_{n})} and is an element of K[[σ̄ → σ]]^{(t_{1},...,t_{n})}.

Proof Sketch. We show that Rel(A, B) is a structure by checking each condition of the definition in turn. Generally, these reduce to properties of relations on λ^{1,×,→} structures. The remaining claims are verified by induction on types and terms.

7.3 Equivalence of Data Representations

Using relational λabstype structures, we can give a sufficient condition for general observational equivalence that is analogous to the one given earlier for top-level equivalence of closed data representations. Suppose x̄: σ̄ ▷ M : [τ/t]σ and x̄: σ̄ ▷ N : [ρ/t]σ are well-typed terms so that we could consider placing ⟨τ, M⟩ or ⟨ρ, N⟩ in a context of the form,

C : : = … abstype t with x: σ is [ ] in P …,

requiring a data representation for type t with operations x:σ. Ignoring free variables in ⟨τ, M⟩ and ⟨ρ, N⟩, we would say that if there are relations on the interpretations of τ and ρ preserved by the meanings of operations M and N, then ⟨τ, M⟩ and ⟨ρ, N⟩ are observationally equivalent. In stating this as a theorem, the relation between types is represented by an interpretation of a fresh type constant into U^{Rel(A,B)}. Taking the free type variables of τ and ρ into account, we will demonstrate the equivalence of two data representations by choosing a relation between the meanings of τ and ρ for each set of values for the free type variables. This is reflected in the following condition as an interpretation of a parameterized type constant a(t_{1},…, t_{n}) into U_{n}^{Rel(A,B)}. We state the following as a corollary of Theorem 2 since the proof is almost immediate.

Corollary 2 Let I and J be interpretations of λabstype signature Σ into A and B (respectively) and let x̄:σ̄▷M:[τ/t]σ and x̄:σ̄▷N:[ρ/t]σ be well-typed terms such that ⟨τ, M⟩ and ⟨ρ, N⟩ are data representations for type t with x: σ. Assume all free type variables in τ,M,ρ, and N are among t_{1},…, t_{n}. Then ⟨τ, M⟩ is observationally equivalent to ⟨ρ, N⟩ with respect to I and J if there is an interpretation K of Σ′ = Σ ∪ {a(t_{1},…, t_{n}), f(t_{1},…, t_{n}) : [a(t_{1},…, t_{n})/t](σ̄ → σ)} into Rel(A, B) that is compatible with

\begin{aligned}I[ & a(t_{1},…, t_{n}) ↦ I[[τ]]^{(t_{1},...,t_{n})}, \\ & f(t_{1},…, t_{n}) ↦ I[[M]]^{(t_{1},...,t_{n})} ] \end{aligned}

and the analogous extension of J, and such that K(nat) is the identity relation.

This corollary gives a method for proving equivalence of data representations. In the simpler cases considered earlier, the method was to define a relation or family of relations and show that these are preserved by the given operations. The most direct formalization would use secondor higher-order logic. Since the corollary above involves a relation parameterized by types, the straightforward formalization in a logic for proving equivalence would require predicate symbols with type or sort parameters. We have not investigated the exact properties required of such a formal system.

A shortcoming of this corollary is that the relation between σ and τ that must be preserved by M and N only depends on a set of free type variables, not the free term variables of M and N. Since relations parameterized by terms requires a substantially different mathematical framework, we leave this refinement to further research.

Appendix: Typing Rules

We define the set of well-formed terms of each type using axioms and inference rules. Recall that Γ ▷ M : τ may be read, “in context Γ, the term M has type τ.” The typing axiom for an ordinary term constant is

(cst) ∅ ▷ c: σ,

where we assume that c:σ is given by the signature. For term constant with type paramenters (in second version of λabstype), we have the axiom,

(cst) ∅ ▷ c(t_{1},…, t_{n}) : σ,

for c(t_{1},…, t_{n}) : σ given by the signature. The typing axiom for variables is

(var) x: σ ▷ x: σ.

The structural rule,

(add var)  \frac{Γ ▷ M : σ}{Γ, x: τ ▷ M : σ} ,

allows us to add variables to the typing context. The remaining rules each pertain to one form of term.

(→ Intro)  \frac{Γ, x: σ ▷ M : τ}{Γ ▷ (λx: σ.M) : σ → τ} .

(→ Elim)  \frac{Γ ▷ M : σ → τ, Γ ▷ N : σ}{Γ ▷ MN : τ} .

(× Intro)  \frac{M : σ, N : τ}{⟨M, N⟩: σ × τ} .

(× Elim)  \frac{M : σ × τ}{Proj_{1}^{σ,τ} M : σ, Proj_{2}^{σ,τ} M : τ} .

(abstype) \frac{Γ, x: σ ▷ N : ρ, Γ ▷ M : [τ/t]σ}{Γ ▷ (abstype t with x: σ is ⟨τ, M⟩ in N) : ρ} t not in Γ, ρ.

Bibliography

[AMSW91] S. Abramsky, J. Mitchell, A. Scedrov, and P. Wadler. Relators. Manuscript, 1991.

[Bar84] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984.

[BTC88] V. Breazu-Tannen and T. Coquand. Extensional models of polymorphism. Theoretical Computer Science, 59:85–114, 1988.

[Hoa72] C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271–281, 1972.

[LS86] J. Lambek and P.J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge, U.K, 1986.

[McC61] John McCarthy. A basis for mathematical theory of computation. In Proc. Western Joint Computer Conf, pages 225– 238, May 1961. Later version in P. Braffort and D. Hirschberg (eds.), Computer Programming and Formal Systems, North-Holland, Amsterdam, pages 33–70, 1963.

[McC63] John McCarthy. Towards a mathematical theory of computation. In Proc. IFIP Congress 62, pages 21–28, Amsterdam, 1963. North-Holland.

[Mil71] R. Milner. An algebraic definition of simulation between programs. Technical Report CS 205, Stanford University, 1971.

[Mil77] R. Milner. Fully abstract models of typed lambda calculi. Theoretical Computer Science, 4(1), 1977.

[Mit86] J.C. Mitchell. Representation independence and data abstraction. In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 263–276, January 1986.

[Mit90] J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, pages 365–458. North-Holland, Amsterdam, [MM85] J.C. Mitchell and A.R. Meyer. Second-order logical relations.

In Logics of Programs, pages 225–236, Berlin, June 1985. Springer-Verlag LNCS 193.

[MP88] J.C. Mitchell and G.D. Plotkin. Abstract types have existential types. ACM Trans. on Programming Languages and Systems, 10(3):470–502, 1988. Preliminary version appeared in Proc. 12th ACM Symp. on Principles of Programming Languages, 1985.

[MS89] J.C. Mitchell and P.J. Scott. Typed lambda calculus and cartesian closed categories. In Proc. Conf. Computer Science and Logic June 14-20, 1987, Univ. Colorado Boulder, volume 92 of Contemporary Mathematics, pages 301–316. Amer. Math. Society, 1989.

[Plo77] G.D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[Rey83] J.C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing ’83, pages 513–523. North-Holland, Amsterdam, 1983.

[Sta85] R. Statman. Logical relations and the typed lambda calculus. Information and Control, 65:85–97, 1985.

[Sto88] A. Stoughton. Fully Abstract Models of Programming Languages. Pitman, London, and John Wiley and Sons, New York,