Reynolds presents a fable in which two professors define the complex numbers in different ways (<a,b> for a+bi vs. <r,t> for r(cos(t)+isin(t))) and define the primitive operations (and prove the basic properties of these operations). Then, the two professors classes get switched, but there is no confusion because the two professors always work at the proper level of abstraction using the basic properties of the complex numbers and the primitive operations without referencing the definition. The moral is that: "Type structure is a syntactic discipline for enforcing levels of abstraction." Instead of talking about "the" complex numbers, we should talk about a type "Complex" which can be realized in different but related ways. In particular, we should not think of "Complex" as denoting a specific subset of a universe (such as D-infinity), and unions and intersections with sets of other types should not be well-defined.

The algebraic view of types interprets types as the initial algebra with the signature given by the primitive operations. So, the only terms in the language are those expressible from the primitive operations, and in every algebra of the variety there is a unique member corresponding to the term. Furthermore, these denotations are preserved under homomorphisms. This is a first-order notion. Homomorphic functions do not induce higher order homomorphic functions. In order to generalize this view of types to higher-order types, we instead look at relations.

The types of the typed lambda calculus are generated from constant types (including Bool) and type variables by products and exponents. A finite number of ordinary variables may be given types [think: context] by a type assignment pi. Ordinary expressions are generated from ordinary constants (which must have a closed type) and variables (typed by the given type assignment) by application, abstraction (with explicit types), products, projections, and "if-then-else" constructs.

To specify semantics, we start with a mapping from constant types to sets (where Bool maps to {true,false}). A set assignment S maps the type variables to sets. Any set assignment can be extended to a mapping S# from types to sets by sending constant types to their sets (always the same ones independent of S), type variables to their image under S, exponents to function spaces, and products to cartesian products. S also induces a map S#* sending each type assignment to the appropriate finite product of sets.

Since the ordinary constants do not depend on the type variables, an ordinary constant k of type omega must denote something in S#(omega) which is the same set independent of S. Assume we fix the element which each such k denotes. Now, we inductively define (in the obvious way) a semantic function mu_(pi,omega)(e,S,eta) (written: mu_(pi,omega) [[e]] S eta) for expressions e of type omega (with type assignment pi), S set-assignments, and eta in S#*(pi). Notice that S is an explicit argument of the semantic function. We will use this fact to compare the denotations under different set assignments.

If we start with a relation assignment R:S1->S2 (from a set assignment S1 to a set assignment S2) mapping each type variable t to a subset of S1(t)xS2(t), then we can extend R to R# mapping all types omega to a subset of S1(omega)xS2(omega). We send constant types to the identity relation. For exponents, f in S1(a->b) is related to g in S2(a->b) iff whenever x in S1(a) is related to y in S2(a) implies f(x) in S1(a) is related to g(y) in S2(b). For products, pairs are related if components are related. R further extends to R#* giving relations on environments.

The Identity Extension Lemma states that if omega is a type and R is a relation assignment sending all type variables in omega to the identity relation, then R#(omega) is the identity relation. The Abstraction Theorem states that if R:S1->S2 and e is an expression, and eta1 and eta2 are R-related environments, then mu [[e]] S1 eta1 is related to mu [[e]] S2 eta2. The proof of the Abstraction Theorem uses the Identity Extension Lemma to show that constants (which must have type omega with no type variables) are related since they are always interpreted as the same object and R#(omega) is the identity relation.

We can define type substitution and show that set assignments and relation assignments have the obvious substitution properties: S#(w'/t->w) = [S|t:S#w](w'), R#(w'/t->w) = [R|t:R#w](w'). For a type assignment pi and type variable t, let pi-t be the type assignment pi restricted to those variables v where t does not occur (free) in pi(v). Given these tools, we can extend the language to include pure type definitions of the form "lettype t = w in e" where t is a type variable, w is a type, and e is an ordinary expression of type w' under type assignment pi-t. This expression "lettype t = w in e" is of type (w'/t->w) under type assignment pi. (Later, once we have type variable binders, we can view this as "(Lambda t.e)[w]".) Semantically, we interpret the expression as follows: mu_{pi,(w'/t->w)} [[lettype t = w in e]] S eta = mu_{pi-t,w'} [[e]] [S|t=S#(w)] eta|dom(pi-t). The condition that t not appear in the type of any free variable of e (i.e., e is typed under type assignment pi-t) is necessary to make this interpretation well-defined.

The Abstraction Theorem easily holds for this extension. The Abstraction Theorem and Identity Extension Lemma imply the Pure Type Definition Theorem which states that (under the appropriate conditions as above) mu_(pi,(w'/t->w1)) [[lettype t = w1 in e]] S eta is [IA|t:r]-related to mu_(pi,(w'/t->w2)) [[lettype t = w2 in e]] S eta for any relation r between S#(w1) and S#(w2). That is, we can "implement" the type t as w1 or w2 and get related results.

We can extend pure type definitions to general type definitions which define primitive operators on the type. Since we already allow abstraction on ordinary variables, this extension is trivial. For example (with one primitive operator), the expression "lettype t = w with vp:wp = ep in e" is syntactic sugar for "(lettype t = w in lambda vp:wp . e)(ep)" (where t is a type variable; w, w', and wp are types; pi is a type assignment; vp is an ordinary variable; e is of type w' under type assignment [pi-t|vp:wp]; ep is of type (wp/t->w) under type assignment pi). The General Type Definition Theorem states that whenever e1 and e2 are [IA|t:r]-related ordinary expressions of type (wp/t->w1) and (wp/t->w2) respectively, where r is a relation between S#(w1) and S#(w2), then "lettype t = w1 with vp:wp = e1 in e" is [IA|t:r]-related to "lettype t = w2 with vp:wp = e2 in e".

Note, as a special case, if w' does not depend on the type variable t, then [IA|t:r]#(w') is the identity relation (by the Identity Extension Lemma) independent of r. In this case, "lettype t = wi with vp:wp = ei in e" is independent of i.

We can also define domain-theoretic semantics by interpreting types as domains (complete partial orderings), exponent types as the set of continuous functions ordered pointwise, the type Bool as the three element domain {bottom<=true,false}, and the conditional "if-then-else" with the undefined case. Furthermore, we can add a fixed point operator to the language and interpret it using least fixed points. The Abstraction Theorem (with general relations) fails. The Abstraction Theorem does hold if we restrict ourselves to complete relations. A complete subset of a domain includes bottom and is closed under sups of directed sets. A complete relation between domains s1 and s2 is a complete subset of the domain s1 x s2. Identity relations are complete and completeness is preserved by forming r->r' and r x r', so this restriction to complete relations makes sense. (Other similar types of restrictions are required if we take domains to be complete lattices.) [Nonempty] ideals (downward closed sets) are complete subsets.

The relation semantics on domains given above can be modified to "order-relation" semantics in which we use the order relation <=s on s x s instead of the identity relation on s x s (note that <=s is a complete relation). The Abstraction Theorem holds true for order-relation semantics.

The abstraction properties of types using domain-theoretic semantics can be characterized by a "representation" theorem. This reduces to the Abstraction Theorem using order-relation semantics.

A representation between domains s1 and s2 is <phi,psi> with phi:s1->s2, psi:s2->s1 continuous and phi o psi <= 1_s1 and 1_s2 <= psi o phi (note this is an adjunction phi -| psi between the poset categories s1 and s2--but we also have phi and psi continous, not just monotone). There is a category REP of domains and representations between them. We can form exponent and product representations which allows us to extend a representation assignment on type variables (relative to domain assignments S1 and S2) to a map sending all types to representations (sending constant types to the identity representation).

Every representation <phi,psi> between s1 and s2 induces a relation _<phi,psi>_ between s1 and s2 by <x1,x2> iff x1 <= psi(x2) (iff phi(x1) <= x2). The map sending representations to relations in this way sends each identity representation to the corresponding order relation and respects products and exponents. This allows us to infer the Representation Theorem from the Abstraction Theorem. The Representation Theorem states that if P is a representation assignment between domain assignments S1 and S2, e is an expression of type w under type assignment pi, and eta1 and eta2 are _P#*(pi)_-related environments, then mu [[e]] S1 eta1 is _P*(w)_-related to mu [[e]] S2 eta2.

We can introduce polymorphic functions into the language by allowing binding of type variables. "(Lambda t . e)[w]" should have the same meaning as "lettype t = w in e". The rules for forming ordinary expressions are extended to include "Lambda t.e" is an expression of type "delta[forall] t.w" under type assignment pi whenever e is an expression of type w under type assignment pi-t and the rule giving "e[w]" of type (w'/t->w) under type assignment pi whenever "e" is an expression of type "delta t.w'" under type assignment pi. Notice that we do not allow the free ordinary variables in e to depend on the type variable t if we form "Lambda t.e".

Strachey distinguished between "parametric" and "ad hoc" polymorphism. A parametric polymorphic function "behaves the same way for all types" where an ad hoc polymorphic function may have "unrelated meanings for different types." The polymorphic lambda calculus is intended to only represent parametric polymorphic functions since it does not allow branching on types.

Domain-theoretic models of the polymorphic lambda-calculus can be constructed, but they include ad hoc polymorphic functions. Reynolds conjectured that set-theoretic models which only include parametric polymorphic functions exist [though he later showed set-theoretic models do not exist]. In this paper, he gives criteria such a model should satisfy. Intuitively, we would like to interpret the type "delta t.w" as the set of all "parametric" class functions from SET (the class of all sets) to elements of the appropriate type (i.e., p in S#(delta t.w) implies p(s) in [S|t:s]#(w)). Of course, this is not a set. The hope was that the restriction to parametric functions will make the class isomorphic to a set. The semantic function on ordinary expressions is extended in the obvious way to interpret "Lambda t.e" and "e[w]".

In order to formulate the Abstraction Theorem in this context, we must extend the notion of relation semantics. For the Abstraction Theorem to hold, we need to define R#(delta t.w) to be the relation which holds between p1 and p2 iff for every sets s1 and s2 and relation r between s1 and s2, we have p1(s1) is [R|t:r]#(w)-related to p2(s2). If we consider the special case when s1=s2 and r is the identity relation, then we see that <p1,p2> in IA#(delta t.w) implies p1=p2. However, we do not automatically have that <p,p> is in IA#(delta t.w). That is, the Identity Extension Lemma does not follow automatically. The solution is to use parametricity. To have <p,p> in IA#(delta t.w), we need <p(s1),p(s2)> in [IA|t:r]#(w) for every s1, s2, r. So, we can define parametricity to be this condition. This gives us the Identity Extension Lemma, so that for any environment eta for a type assignment pi, we have <eta,eta> in IA#*(pi). The Abstraction Theorem then gives <mu [[e]] S eta s1,mu [[e]] S eta s2> is in [IA|t:r]#(w). That is, mu [[Lambda t.e]] S eta' is parametric, hence well-defined. (In other words, this definition of parametricity is "permissible".) "The abstraction theorem guarantees that, in an environment in which all polymorphic functions are parametric, the meaning of any ordinary expression will be parametric."

For types w without any type variable bindings, S#(delta t.w) is isomorphic to a set. In particular, S#(delta t.(t^n1 -> t) x . . . x (t^nk -> t) -> t) is isomorphic to the initial one-sorted algebra with k operators with arity n1, ..., nk. So, S#(delta t.t) is empty; S#(delta t.t->t) is a singleton; S#(delta t.t x t -> t) has two members (e.g., truth values); S#(delta t.t^n -> t) has n members; S#(delta t.(t->t) x t -> t) is isomorphic to the naturals.

In greater generality, suppose we have S#(delta t1,...,tN.(w1 x ... x wm x w1' x . . . x wn' -> t)) where each wi = t_l_i or <product of type variables> -> t_l_i and each wj' = tj' or <product of type variables> -> tj' and tj' is not any of t1, . . ., tN. This can be described using a multisorted free algebra with generators determined by the wi's. An explanation is given in the paper, but the examples make the idea clear: S#(delta t.(a->t)->t) is isomorphic to S#(a) because the free algebra generated by k:a->t starting with S1#(a)=S#(a) gives [at sort t] S2#(t) = S#(a). S#(delta t.(a->t) x (b->t) -> t) is isomorphic to the disjoint union S#(a)+S#(b) because this is the free algebra at sort t [S2#(t)] generated by k:a->t and k':b->t starting with S1#(a)=S#(a) and S1#(b)=S#(b). The most interesting example given (suggested by an encoding of lists devised by Bohm) is S#(delta t.(a x t -> t) x t -> t) which is isomorphic to the set of lists over a because this is the free algebra at sort t generated by cons:a x t -> t and nil:t starting from S1#(a)=S#(a) and S1#(t)=empty.

This led Reynolds to conjecture that whenever w contains no type variable bindings, then S#(delta t.w) is isomorphic to the set of closed beta-nf's of type w.

In order to improve his chances of finding a set-theoretic model, Reynolds considered a more general abstraction theorem which would allow him to consider other definitions for parametricity. One generalization simply considers multinary (I-ary for an index set I) relations instead of binary relations. That is, we consider Rel(S)=Power(Prod_I(S)) where S:I->SET. A further generalization considers families of relations ordered as in Kripke semantics. That is, we start with a fixed poset W (of "alternative worlds") and define a Kripke relation among Si (for i over an index set I) to be a monotone function f:W->Rel(S) where Rel(S) is ordered by inclusion. The identity Kripke relation on S, IK(S), is the constant map to the identity relation on S. Following the same pattern as before, we start with a Kripke relation assignment on type variables and extend it to all types by sending type constants to the identity Kripke relation, by defining exponents and products of Kripke relations, and by handling type variable bindings. In particular, given two Kripke relations k and k', define k->k' so that f is in (k->k')w (for w in W) iff <fi(xi)>_i is in k'w' whenever w'>=w and <xi>_i is in kw' (i.e., iff f maps related values to related values at all later times). Products are defined componentwise at each world w. In order to handle type variable bindings, we suppose K#(omega) is defined for any Kripke relation assignment K already. Suppose K is a Kripke relation assignment among set assignments <Si>_i. Then, K#(delta t.omega) is a Kripke relation on <Si#(delta t.omega)>_i defined so that P is in K#(delta t.omega)w (for w in W) iff for any s:I->SET and Kripke relation k among s, <Pi(si)>_i is in [K|t:k]#(omega)w.

The Generalized Abstraction Theorem follows: For any Kripke relation assignment K among set assignments <Si>_i, expression e (of type omega), world w, and <eta_i>_i family of K-related environments in world w, we have <mu [[e]] Si eta_i>_i is K-related in world w (i.e., is in K#(omega)w). Also, we have the Generalized Identity Extension Lemma if we define parametric p (taking sets s to members of [S|t:s]#(omega)) to be those which forall s:I->SET and Kripke relations k among s and all worlds w, <p(si)>_i is in [IA|t:k]#(omega)w. This definition is permissible by the Generalized Abstraction Theorem.

Girard introduced the polymorphic lambda calculus to extend the Curry-Howard correspondence to include quantifiers over propositional variables. The "forall" quantifier (over propositional variables) corresponds to Reynolds "delta". Girard also included an "exists" quantifier (over propositional variables).

Existential types can be used to define abstract types with primitive operations (hiding the implementation). Given an expression e = <<w,ep:exists t wp>> [note: read this as a 4-tuple <w,ep,t,wp>] of type "exists t.wp" we think of the expression "abstract t,vp = e in e'" (where w is a type and e' is an expression of type w' with t not free in the type w') as (Lambda t.lambda vp.e')[wp][ep]. That is, e' is an expression using an abstract type t and primitive operation vp with implementation as type wp and expression ep hidden inside e.

Semantically, there is no real difference between including and excluding existential types, since we can define them in terms of universal types. In particular, "exists t.w" should have the same interpretation as "delta t'.((delta t.w->t')->t')" (where t' is distinct from t and any free type variable in w). We can use this to extend set assigments, relation assigments, and Kripke relation assignments to include existential types. The new constructions are interpreted as follows: <<w,ep:exists t.wp>> is interpreted as Lambda t'.lambda v:(delta t.wp->t').v[w]ep (where t' is fresh) and "abstract t,vp=e in e'" is interpreted as e[w'](Lambda t.lambda vp:wp.e') where e has type "exists t.wp" and e' has type w'.

Possible future work listed includes exploring connections with category theory, searching for parametric domain models (so that a recursion operator can be included), including subtypes and implicit conversions, and applying the theory to imperative Algol-like languages.