Types, Abstraction, and Parametric Polymorphism

— for Domains

John C. Reynolds ^{1}

Department of Computer Science Carnegie Mellon University

MFPS XX — May 2004 (corrected May 27, 2004)

\begin{matrix}c \\ ◯ \end{matrix}2004 John C. Reynolds john.reynolds@cs.cmu.edu

1Research partially supported by NSF Grant CCR-0204242.

The Syntax of Types and Contexts

Let T be a finite set of type variables. Then Θ_{T}, the set of types over T, is the least family of sets such that

• If τ ^{∈} T, then τ ^{∈} Θ_{T}.

• If θ, θ′ ^{∈} Θ_{T}, then θ → θ′ ^{∈} Θ_{T}.

• If θ ^{∈} Θ_{T ∪{τ}}, then ∀τ. θ ^{∈} Θ_{T}. Also, Π_{T} is the set of contexts over T, which are functions

π = [ v_{1}: θ_{1} | … | v_{n}: θ_{n}]

from a finite set {v_{1}, …, v_{n}} of ordinary variables to Θ_{T}.

The Semantics of Types and Contexts

We assume that Dom is the set of domains, which are certain complete partial orders with least elements. Suppose T is a finite set of type variables, and

D ^{∈} Dom^{T}

is a domain assignment. Then

D^{#} ^{∈} Dom^{(Θ_{T} ∪Π_{T})}

is the extension of D to types and type assignments over T, such that

\begin{aligned}D^{#}(τ) & = & D(τ) \\ D^{#}(θ → θ′) & = & D^{#}(θ) ⇒ D^{#}(θ′) \\ D^{#}(∀τ. θ) & ⊂ & ∏_{d^{∈}Dom}[ D | τ: d]^{#}(θ) \\ D^{#}(π) & = & ∏_{v^{∈}dom π} D^{#}(π(v)), \end{aligned}

where

• d ⇒ d′ denotes the domain of continuous functions from d to d′ (ordered pointwise),

• ∏_{d^{∈}S} denotes a Cartesian product indexed by S (ordered componentwise).

Polymorphic Extensionality

Since D^{#}(∀τ. θ) is a subset of ∏_{d^{∈}Dom}[ D | τ: d]^{#}(θ) =

{ p | dom p = Dom and ∀d ^{∈} Dom. p[d] ^{∈} [ D | τ: d]^{#}(θ) }, polymorphic functions are extensional, i.e., for all p, p′ ^{∈} D^{#}(∀τ. θ),

(∀d ^{∈} Dom. p[d] = p′[d]) implies p = p′.

Polymorphic Application

We also assume that polymorphic application is strict, i.e., ⊥[d] = ⊥.

Complications we are Ignoring

• The meanings of types may be entities (such as retractions of a universal domain) that denote domains.

• Products and Lifting

• Coproducts and Predomains

The Syntax of Terms

\frac{π ^{∈} Π_{T} v ^{∈} dom π}{π ⊢_{T} v : π(v)}

\frac{π ⊢_{T} e_{1} : θ → θ′ π ⊢_{T} e_{2} : θ}{π ⊢_{T} e_{1}e_{2} : θ′}

\frac{[ π | v: θ] ⊢_{T} e : θ′}{π ⊢_{T} λv: θ. e : θ → θ′}

\frac{π ⊢_{T} e : ∀τ. θ θ′ ^{∈} Θ_{T}}{π ⊢_{T} e[θ′] : (θ/τ → θ′)}

\frac{π ⊢_{T ∪\{τ\}} e : θ π ^{∈} Π_{T}}{π ⊢_{T} Λτ. e : ∀τ. θ}

\frac{π ⊢_{T} e : θ → θ}{π ⊢_{T} Y_{θ}e : θ}

The Semantics of Terms

When π ⊢_{T} e : θ and D ^{∈} Dom^{T},

[[e]]_{T}^{π,θ}D ^{∈} D^{#}(π) ⇒ D^{#}(θ)

is defined by

\frac{π ^{∈} Π_{T} v ^{∈} dom π}{π ⊢_{T} v : π(v)}  [[v]]_{T}^{π,π(v)}Dη = η(v)

\frac{π ⊢_{T} e_{1} : θ → θ′ π ⊢_{T} e_{2} : θ}{π ⊢_{T} e_{1}e_{2} : θ′}

\begin{matrix}[[e_{1}e_{2}]]_{T}^{π,θ′}Dη = \\ ([[e_{1}]]_{T}^{π,θ→θ′}Dη)([[e_{2}]]_{T}^{π,θ}Dη) \end{matrix}

\frac{[ π | v: θ] ⊢_{T} e : θ′}{π ⊢_{T} λv: θ. e : θ → θ′}  \begin{matrix}[[λv: θ. e]]_{T}^{π,θ→θ′}Dη = \\ λx ^{∈} D^{#}(θ). [[e]]_{T}^{[π|v:θ],θ′}D[ η | v: x] \end{matrix}
\frac{π ⊢_{T} e : ∀τ. θ θ′ ^{∈} Θ_{T}}{π ⊢_{T} e[θ′] : (θ/τ → θ′)} \begin{matrix}[[e[θ′]]]_{T}^{π,(θ/τ→θ′)}Dη = \\ [[e]]_{T}^{π,∀τ. θ}Dη[D^{#}(θ′)] \end{matrix}
\frac{π ⊢_{T ∪\{τ\}} e : θ π ^{∈} Π_{T}}{π ⊢_{T} Λτ. e : ∀τ. θ} \begin{matrix}[[Λτ. e]]_{T}^{π,∀τ. θ}Dη = \\ λd ^{∈} Dom. [[e]]_{T ∪\{τ\}}^{π,θ}[ D | τ: d]η \end{matrix}
\frac{π ⊢_{T} e : θ → θ}{π ⊢_{T} Y_{θ}e : θ}  [[Y_{θ}e]]_{T}^{π,θ}Dη = Y_{D^{#}(θ)}[[e]]_{T}^{π,θ→θ}Dη

More Simply

\frac{π ^{∈} Π_{T} v ^{∈} dom π}{π ⊢_{T} v : π(v)}  [[v]]Dη = η(v)

\frac{π ⊢_{T} e_{1} : θ → θ′ π ⊢_{T} e_{2} : θ}{π ⊢_{T} e_{1}e_{2} : θ′}

[[e_{1}e_{2}]]Dη = ([[e_{1}]]Dη)([[e_{2}]]Dη)

\frac{[ π | v: θ] ⊢_{T} e : θ′}{π ⊢_{T} λv: θ. e : θ → θ′}  \begin{matrix}[[λv: θ. e]]Dη = \\ λx ^{∈} D^{#}(θ). [[e]]D[ η | v: x] \end{matrix}
\frac{π ⊢_{T} e : ∀τ. θ θ′ ^{∈} Θ_{T}}{π ⊢_{T} e[θ′] : (θ/τ → θ′)}  [[e[θ′]]]Dη = [[e]]Dη[D^{#}(θ′)]
\frac{π ⊢_{T ∪\{τ\}} e : θ π ^{∈} Π_{T}}{π ⊢_{T} Λτ. e : ∀τ. θ}  \begin{matrix}[[Λτ. e]]Dη = \\ λd ^{∈} Dom. [[e]][ D | τ: d]η \end{matrix}
\frac{π ⊢_{T} e : θ → θ}{π ⊢_{T} Y_{θ}e : θ}  [[Y_{θ}e]]Dη = Y_{D^{#}(θ)}[[e]]Dη

Complete Relations

A binary relation r between domains d_{1} and d_{2} is said to be complete iff

• ⟨⊥, ⊥⟩ ^{∈} r.

• If

x_{0} ⊑ x_{1} ⊑ x_{2} ⊑ ⋯
y_{0} ⊑ y_{1} ⊑ y_{2} ⊑ ⋯
⟨x_{0}, y_{0}⟩, ⟨x_{1}, y_{1}⟩, ⟨x_{2}, y_{2}⟩ ^{∈} r,

then

⟨⨆_{i=0}^{∞} x_{i}, ⨆_{i=0}^{∞} y_{i}⟩ ^{∈} r.

The Relational Semantics of Types and Contexts

Suppose T is a finite set of type variables, D_{1}, D_{2} ^{∈} Dom^{T}, and R is a function from T to relations such that, for all τ ^{∈} T,

R(τ) is a complete relation between D_{1}(τ) and D_{2}(τ).

Then R (called a relation assignment between D_{1} and D_{2}) can be extended to a function R^{#} on types and type assignments such that, for all τ ^{∈} Θ_{T} and π ^{∈} Π_{T},

R^{#}(τ) is a complete relation between D_{1}^{#}(τ) and D_{2}^{#}(τ),

R^{#}(π) is a complete relation between D_{1}^{#}(π) and D_{2}^{#}(π),

by the following definitions:

• R^{#}(τ) = R(τ).

• R^{#}(θ → θ′) = R^{#}(θ) ⟹^{r} R^{#}(θ′), where

⟨f_{1}, f_{2}⟩ ^{∈} r ⟹^{r} r′ iff

for all ⟨x_{1}, x_{2}⟩ ^{∈} r, ⟨f_{1}(x_{1}), f_{2}(x_{2})⟩ ^{∈} r′.

• ⟨p_{1}, p_{2}⟩ ^{∈} R^{#}(∀τ. θ) iff, for all domains d_{1} and d_{2}, and all complete relations r between d_{1} and d_{2},

⟨p_{1}[d_{1}], p_{2}[d_{2}]⟩ ^{∈} [ R | τ: r]^{#}(θ).

• ⟨η_{1}, η_{2}⟩ ^{∈} R^{#}(π) iff, for all v ^{∈} dom π,

⟨η_{1}(v), η_{2}(v)⟩ ^{∈} R^{#}(π(v)).

.

The Logical Relations (Abstraction) Theorem

If • D_{1}, D_{2} ^{∈} Dom^{T},

• R is a relation assignment between D_{1} and D_{2},

• π ⊢_{T} e : θ,

• ⟨η_{1}, η_{2}⟩ ^{∈} R^{#}π, then

⟨[[e]]_{T}^{π,θ}D_{1}η_{1}, [[e]]_{T}^{π,θ}D_{2}η_{2}⟩ ^{∈} R^{#}θ.

Parametricity

When p ^{∈} D^{#}(∀τ. θ) for some D ^{∈} Dom^{T}, we say that p is parametric iff for all domains d_{1} and d_{2}, and all complete relations r between d_{1} and d_{2},

⟨p[d_{1}], p[d_{2}]⟩ ^{∈} [ I_{D} | τ: r]^{#}(θ),

where I_{D} is the relation assignment that assigns the identity relation on D(τ) to each τ ^{∈} T.

Then we restrict the meaning of polymorphic types to include only parameteric polymorphic functions:

D^{#}(∀τ. θ) ⊆ { p ^{∈} ∏_{d^{∈}Dom}[ D | τ: d]^{#}(θ) | p is parametric },

to obtain:

The Identity Extension Lemma

For all θ ^{∈} Θ_{T}, π ^{∈} Π_{T}, and D ^{∈} Dom^{T},

I_{D}^{#}(θ) is the identity relation on D^{#}(θ),
I_{D}^{#}(π) is the identity relation on D^{#}(π).

Why Parametricity is Permissible

Suppose π ⊢_{T} e : ∀τ. θ, D ^{∈} Dom^{T}, and η ^{∈} D^{#}(π). By the identity extension lemma,

⟨η, η⟩ ^{∈} I_{D}^{#}(π).

Then the logical relations theorem gives

⟨[[e]]Dη, [[e]]Dη⟩ ^{∈} I_{D}^{#}(∀τ. θ).

Thus, by the definition of R^{#}(∀τ. θ), for all domains d_{1} and d_{2}, and all complete relations r between s_{1} and d_{2},

⟨([[e]]Dη)[d_{1}], ([[e]]Dη)[d_{2}]⟩ ^{∈} [ I_{D} | τ: r]^{#}(θ),

i.e., [[e]]Dη is parametric.

More Complications we are Ignoring

• Multinary relations

• Kripke relations

mT -Algebras

A (continuous) mT -algebra is one in which

• The carrier is a domain,

• The operations are continuous functions.

• Homomorphisms are strict continuous functions.

• The arities are endofunctors on the category of domains.

A signature is a finite list T_{1}, … T_{k}, of (covariant) endofunctors on the category of domains. Each T_{i} is called the arity of the operator σ_{i}. When T_{i}(x) = x^{n}, σ_{i} is said to be n-ary.

A mT -algebra A consists of:

• A domain |A| called the carrier,

• For each operator σ_{i}, an operation σ_{i}^{A}, which is a continuous function from T_{i}|A| to |A|.

When A and B are mT -algebras with the same signature, a homomorphism from A to B is a strict continuous function ψ from |A| to |B| such that, for each σ_{i},

[figure: T_{i}|A|; T_{i}|B|; |A|; |B|; T_{i}ψ; ψ; σ_{i}^{A}; σ_{i}^{B}]

Expressible And Relationally Consistent Functors

A functor T is expressible iff

• There is a type T(τ) ^{∈} Θ_{{τ}} such that [ τ: d]^{#}(T(τ)) = T d.

• There is a term T^{τ,τ′}(v) satisfying

[ v: τ → τ′] ⊢_{{τ,τ′}} T^{τ,τ′}(v) : T(τ) → T(τ′), such that, when f ^{∈} d ⇒ d′,

[[T^{τ,τ′}(v)]][ τ: d | τ′: d′][ v: f ] = T f.

An expressible functor T is relationally consistent iff, when ψ ^{∈} d → d′ is viewed as a relation,

[ τ: ψ]^{#}(T(τ)) = T ψ.

Constructing a Weakly Initial mT -Algebra

Given a signature T_{1}, …, T_{k}, let

P =^{def} ∀τ. (T_{1}(τ) → τ) → ⋯ → (T_{k}(τ) → τ) → τ
satisfying P ^{∈} Θ_{{}}
M =^{def} λp: P. p[τ]f_{1} ⋯ f_{k}

satisfying [ f_{1}: T_{1}(τ) → τ | … | f_{k}: T_{k}(τ) → τ ] ⊢_{{τ}} M : P → τ

H_{i} =^{def} λq: T_{i}(P). Λτ. λf_{1}: T_{1}(τ) → τ. · · · λf_{k}: T_{k}(τ) → τ. f_{i}(T_{i}^{P,τ}(M)q)
satisfying [ ] ⊢_{{}} H_{i} : T_{i}(P) → P.

Then, for each operator, by reduction:

M(H_{i}(q)) ⇝ (λp. p[τ]f_{1} ⋯ f_{k})(Λτ. λf_{1}. · · · λf_{k}. f_{i}(T_{i}^{P,τ}(M)q))
⇝ (Λτ. λf_{1}. · · · λf_{k}. f_{i}(T_{i}^{P,τ}(M)q))[τ]f_{1} ⋯ f_{k}
⇝^{∗} f_{i}(T_{i}^{P,τ}(M)q),

i.e.,

[figure: T_{i}(P); T_{i}(τ); P; τ; T_{i}^{P,τ}(M); M; H_{i}; f_{i}]

commutes syntactically.

Constructing a Weakly Initial mT -Algebra (continued)

Thus, we may define the mT -algebra N such that

\begin{aligned}|N| & = & [ ]^{#}P \\ σ_{i}^{N} & = & [[H_{i}]][ ][ ] ^{∈} T_{i}|N| ⇒ |N|. \end{aligned}

Moreover, for any mT -algebra A with the same signature, we may define the function

ϕ_{A} = [[M]][ τ: |A|][ f_{1}: σ_{1}^{A} | … | f_{k}: σ_{k}^{A}]

which satisfies

ϕ_{A}(σ_{i}^{N}) = [[M(H_{i}(q))]][ τ: |A|][f_{1}: σ_{1}^{A} | ⋯ | f_{k}: σ_{k}^{A} | q: q]
= [[f_{i}(T_{i}^{P,τ}(M)q)]][ τ: |A|][f_{1}: σ_{1}^{A} | ⋯ | f_{k}: σ_{k}^{A} | q: q]
= σ_{i}(T_{i}(ϕ_{A})(q)),

i.e.,

[figure: T_{i}|N|; T_{i}|A|; |N|; |A|; T_{i}ϕ_{A}; ϕ_{A}; σ_{i}^{N}; σ_{i}^{A}]

Moreover, since polymorphic application is strict,

ϕ_{A}(⊥) = [[M(p)]][ τ: |A|][f_{1}: σ_{1}^{A} | ⋯ | f_{k}: σ_{k}^{A} | p: ⊥]
= [[p[τ]f_{1} ⋯ f_{k}]][ τ: |A|][f_{1}: σ_{1}^{A} | ⋯ | f_{k}: σ_{k}^{A} | p: ⊥]
= ⊥.

Thus, ϕ_{A} is a homomorphism from N to A, and since A is any mT -algebra with signature T_{1}, …, T_{n}, N is weakly initial.

Strengthening the Weakly Initial Algebra

Henceforth, we assume the T_{i} are relationally consistent. Suppose ψ is a homomorphism from A to B. Since

[figure: T_{i}|A|; T_{i}|B|; |A|; |B|; T_{i}ψ; ψ; σ_{i}^{A}; σ_{i}^{B}]

commutes, if we view ψ as a complete relation then

∀⟨y_{1}, y_{2}⟩ ^{∈} T_{i}ψ. ⟨σ_{i}^{A}y_{1}, σ_{i}^{B}y_{2}⟩ ^{∈} ψ.

Then, since T is relationally consistent,

∀⟨y_{1}, y_{2}⟩ ^{∈} [ τ: ψ]^{#}(T_{i}(τ)). ⟨σ_{i}^{A}y_{1}, σ_{i}^{B}y_{2}⟩ ^{∈} ψ,

so that

⟨σ_{i}^{A}, σ_{i}^{B}⟩ ^{∈} [ τ: ψ]^{#}(T_{i}(τ) → τ).

When p ^{∈} |N| = [ ]^{#}(∀τ. (T_{1}(τ) → τ) → ⋯ → (T_{k}(τ) → τ) → τ), parametricity gives

⟨p[|A|], p[|B|]⟩ ^{∈} [ τ: ψ]^{#}((T_{1}(τ) → τ) → ⋯ → (T_{k}(τ) → τ) → τ),

so that

⟨p[|A|]σ_{1}^{A} ⋯ σ_{k}^{A}, p[|B|]σ_{1}^{B} ⋯ σ_{k}^{B}⟩ ^{∈} [ τ: ψ]^{#}(τ) = ψ,

or, since ψ is a function,

[figure: |A|; |B|; |N|; ψ; ϕ_{A} = λp. p[|A|]σ_{1}^{A} ⋯ σ_{k}^{A}; ϕ_{B} = λp. p[|B|]σ_{1}^{B} ⋯ σ_{k}^{B}]

Strengthening the Algebra (continued)

As a special case, when ψ is a homomorphism from N to A:

[figure: |N|; |A|; |N|; ψ; ϕ_{N}; ϕ_{A}]  (1)

For any d ^{∈} Dom and f_{1} ^{∈} T_{1}d ⇒ d, …, f_{k} ^{∈} T_{k}d ⇒ d, we can take A to be the algebra with carrier |A| = d and operations σ_{i}^{A} = f_{i}. Then taking ψ = ϕ_{A} in (1), we have

[figure: |N|; d; |N|; ϕ_{A}; ϕ_{N}; ϕ_{A}]

where ϕ_{A} = λp. p[A]σ_{1}^{A} ⋯ σ_{k}^{A} = λp. p[d]f_{1} ⋯ f_{k}. Thus

ϕ_{N}(p)[d]f_{1} ⋯ f_{k} = p[d]f_{1} ⋯ f_{k},

so by ordinary extensionality

ϕ_{N}(p)[d] = p[d],

and by polymorphic extensionality

ϕ_{N}(p) = p.

Then (1) gives ψ = ϕ_{A}, so that N is an initial mT -algebra.

The Separated Sum

We write • (d_{1} + d_{2})_{⊥} for the separated sum of d_{1} and d_{2},

• ι_{1} ^{∈} d_{1} ⇒ (d_{1} + d_{2})_{⊥} and ι_{2} ^{∈} d_{2} ⇒ (d_{1} + d_{2})_{⊥} for the

associated injections, Then, for any continuous functions f_{1} ^{∈} d_{1} ⇒ d and f_{2} ^{∈} d_{2} ⇒ d, there is exactly one strict continuous function [f_{1}, f_{2}] such that

[figure: d_{1}; (d_{1} + d_{2})_{⊥}; d_{2}; d; ι_{1}; ι_{2}; f_{1}; f_{2}; [f_{1}, f_{2}]]

It is easy to see that (− + −)_{⊥} can be extended to a functor, and generalized to k arguments.

T -Algebras

Let T be an endofunctor on the category of domains and strict continuous functions. Then a T -algebra A consists of:

• A domain |A| called the carrier,

• A single operation σ^{A}, which is a strict continuous function

from T |A| to |A|. When A and B are T -algebras, a homomorphism from A to B is a strict continuous function ψ from |A| to |B| such that

[figure: T |A|; T |B|; |A|; |B|; T ψ; ψ; σ^{A}; σ^{B}]

From mT -Algebras to T -Algebras

We can map mT -algebras into T -algebras as follows:

• The signature T_{1}, …, T_{k} is mapped into the endofunctor T (x) = (T_{1}(x) + ⋯ + T_{k}(x))_{⊥}.

• Carriers |A| are left unchanged.

• The operations σ_{1}^{A}, …, σ_{k}^{A} are mapped into [σ_{1}^{A}, …, σ_{k}^{A}].

• Homomorphisms are left unchanged. It can be shown that this mapping carries initial algebras into initial algebras.

Initial T -Algebras are Isomorphisms

[figure: T |N|; T (T |N|); T |N|; |N|; T |N|; |N|; T ϕ_{T |N|}; T σ^{N}; ϕ_{T |N|}; σ^{N}; σ^{N}; T σ^{N}; σ^{N}]

• Since the right square commutes, σ^{N} is a homomorphism.

• By tne initiality of N, ϕ_{T |N|} ; σ^{N} = I_{|N|}.

• Since the left square commutes, σ^{N};ϕ_{T |N|} = T ϕ_{T |N|};T σ^{N} = T (ϕ_{T |N|};σ^{N}) = T I_{|N|} = I_{T |N|}.

An Algebraic Polymorphic Domain

Thus we find that the meaning of ∀τ. (τ → τ) → τ → τ is the initial mT -algebra with one constant and one unary operator.

[figure: ≥0; ≥1; ≥2; =0; =1; =2; ∞; ^{. . . . . . . . . . . .}]

An Algebraic Polymorphic Domain

Thus we find that the meaning of ∀τ. (τ → τ) → τ → τ is the initial mT -algebra with one constant and one unary operator.

[figure: Λτ. λf. λx. ⊥; Λτ. λf. λx. f(⊥); Λτ. λf. λx. f(f(⊥)); Λτ. λf. λx. x; Λτ. λf. λx. f(x); Λτ. λf. λx. f(f(x)); Λτ. λf. λx. f(f(f(⋯))); ^{. . . . . . . . . . .}]

The General (One-Sorted) Case

The meaning of the polymorphic type

∀τ. (\underbrace{τ → ⋯ τ →}_{n_{1} times} τ) → ⋯ → (\underbrace{τ → ⋯ τ →}_{n_{k} times} τ) → τ

is the initial mT -algebra with k operators of arities n_{1}, ⋯, n_{k}.

Instances

∀τ. τ  ∘
O = ∀τ. τ → τ  \begin{matrix}∘ \\ ∘ \end{matrix}
∀τ. τ → τ → τ  [figure: ∘; ∘; ∘]
∀τ. (τ → τ) → τ  ∘ ∘ ∘ ∞^{...}

∀τ. (τ → τ) → (τ → τ) → τ  [figure: ∘; ∘; ∘; ∘; ∘; ∘; ∘; ⋮; ⋮; ⋮; ⋮; ⋮; ⋮; ⋮; ⋮]

Another Example

The domain of type

∀τ. (((τ → O) → O) → τ) → τ

is the initial T -algebra for

Tτ = ((τ → O) → O)_{⊥},

where O = ∀τ. τ → τ denotes the domain

\begin{matrix}∘ \\ ∘ \end{matrix}

The initial algebra is:

∘ ∘ ∘ ∘ ∘ ∘ ∘ ∘ ∘⋮⋮