This is a copy of the abstract and slides for an invited talk at the Workshop on Intersection Types and Related Systems, Geneva, Switzerland, July 15, 2000 (with minor corrections).

An Intrinsic Semantics of Intersection Types^{∗}

John C. Reynolds Department of Computer Science Carnegie Mellon University

July 28, 2000

∗This research was supported in part by National Science Foundation Grant CCR-9804014. It was also partly supported by the Danish National Research Foundation, during visits to the BRICS Centre at Aarhus University in 1999 and 2000.

Abstract

Most models of intersection types, such as filter models, are extrinsic semantics, i.e., terms have the same meaning as in a typeless model, and the type of a term denotes a property of its meaning. In contrast, the usual denotational semantics of a real programming languages is an intrinsic semantics, in which only well-typed terms have meanings, which are defined by induction on the proof of their typing.

We will illustrate this distinction by relating the two kinds of semantics for the functional sublanguage of the programming language Forsythe.

Outline of the Talk

1. Intersection types in Forsythe

2. An intrinsic semantics of the functional sublanguage 3. An untyped semantics

4. A logical relations theorem

5. The bracketing conjecture

6. Consequences of the bracketing conjecture

The Evolution of Types in Forsythe

θ ::= δ | prod(ι: θ, …, ι: θ) | θ → θ

where the primitive types δ are

[figure: realvar; intvar; int; real; boolvar; bool; comm]

Adding Acceptors and Completions

[figure: realvar; realacc; intacc; intvar; int; real; boolacc; boolvar; bool; comm; compl]

Conditional Variables

If p is a boolean expression, n is an integer variable, and x is a real variable, one can write

if p then n else x

on either side of an assignment command. This is an

int(eger accepting), real (producing) var(iable), where

[figure: realvar; realacc; intacc; (int, real) var; intvar; int; real]

Forsythe with Intersection Types

θ ::= δ | ι: θ | θ → θ | ns | θ & θ

where the primitive types δ are

[figure: value; real; bool; int; comm; compl]

Some Abbreviations

intvar ≡ int & intacc
(int, real) var ≡ real & intacc
intacc ≡ int → comm
prod(ι_{1}: θ_{1}, …, ι_{n}: θ_{n}) ≡ ι_{1}: θ_{1} & ⋯ & ι_{n}: θ_{n}
realarray ≡ (int → realvar) & len: int

Subtyping Rules

\overline{θ ≤ ns}  \overline{θ & θ′ ≤ θ}  \overline{θ & θ′ ≤ θ′}

\frac{θ ≤ θ′ θ ≤ θ′′}{θ ≤ θ′ & θ′′}

\frac{δ ≤_{prim} δ′}{δ ≤ δ′}  \frac{θ ≤ θ′}{ι: θ ≤ ι: θ′}  \frac{θ′_{1} ≤ θ_{1} θ_{2} ≤ θ′_{2}}{θ_{1} → θ_{2} ≤ θ′_{1} → θ′_{2}}

\overline{ι: θ & ι: θ′ ≤ ι: (θ & θ′)} \overline{(θ → θ′) & (θ → θ′′) ≤ θ → (θ′ & θ′′)}

\overline{ns ≤ ι: ns}  \overline{ns ≤ θ → ns}

Some Consequences

[figure: partno: intvar & cost: realvar; partno: int & cost: real; partno: int; cost: real]

[figure: int → real; int → int; real → real; (int → int) & (real → real)]

Merging

\frac{π ⊢ p′ : θ}{π ⊢ (p, ι ≡ p′) : (ι: θ)}

\frac{π ⊢ p : θ}{π ⊢ (p, ι ≡ p′) : θ} when θ does not have the form ι: ⋯

\frac{[ π | ι: θ] ⊢ p′ : θ′}{π ⊢ (p, λι. p′) : θ → θ′}

\frac{π ⊢ p : θ}{π ⊢ (p, λι. p′) : θ} when θ does not have the form ⋯ → ⋯

For example, ⊢ (partno ≡ 711, cost ≡ 3.97) : partno: int & cost: real x: realvar, y: realvar ⊢

(len ≡ 2, λk. if k = 0 then x else y) :

len: int & (int → realvar)

n: int ⊢ (n, next ≡ n + 1) : int & next: int n: intvar ⊢ (n, λk. n := n + k) : int & (int → comm)

Intrinsic versus Extrinsic Semantics

In an intrinsic semantics:

• Only terms that satisfy typing judgements possess meanings.

• Terms that satisfy several typing judgements possess several meanings.

• Meanings are assigned to typing judgements, by structural induction on the proofs of these judgements.

[[π ⊢ λx. x : int → int]]η = the identity function on integers. [[π ⊢ λx. x : real → real]]η = the identity function on reals.

In an extrinsic semantics:

• All terms possess meanings.

• Meanings are independent of typing judgements.

• Types describe properties of meanings. [[λx. x]]η = the identity function on the universal domain. π ⊢ λx. x : int → int means that, when n is an integer, (λx. x) n is an integer.

The Intrinsic Semantics of Intersection Types

1. The category K is Cartesian closed.

2. There is a subcategory S of K such that every finite diagram in S has a limit in S that is also a limit in K.

3. There is a functor ⟹_{S}: S^{op} × S to S that is a restriction of the exponentiation functor ⟹_{K}: K^{op} × K to K. For each object k of S, the functor k ⟹_{S} − preserves limits in S.

For Forsythe:

K and S are subcategories of a functor category CPO^{Σ}. For the functional sublanguage of Forsythe (without comm or compl):

1. K: Algebraic lattices and continuous functions.

2. S: Algebraic lattices and strict continuous functions that respect greatest lower bounds.

The Semantic Functor

The semantic functor [[−]], from the preordered set of types (viewed as a category) to the category S, satisfies

1. [[int]], [[real]], [[bool]], and [[value]] are the flat lattices of integers, reals, booleans, and values.

[[int ≤ real]], [[real ≤ value]], and [[bool ≤ value]] are (doubly strict) identity injections.

2.  \begin{aligned}[[θ_{1} → θ_{2}]] & = & [[θ_{1}]] ⇒ [[θ_{2}]] \\ [[θ_{1} → θ_{2} ≤ θ′_{1} → θ′_{2}]] & = & [[θ′_{1} ≤ θ_{1}]] ⇒ [[θ_{2} ≤ θ′_{2}]] \\ [[θ_{1} → θ_{2} ≤ θ′_{1} → θ′_{2}]]f & = & [[θ′_{1} ≤ θ_{1}]] ; f ; [[θ_{2} ≤ θ′_{2}]]. \end{aligned}

3.  \begin{aligned}[[ι: θ]] & = & [[θ]] \\ [[ι: θ ≤ ι: θ′]] & = & [[θ ≤ θ′]]. \end{aligned}

4. [[ns]] is a terminal object:

[[ns]] = {⊥}.

[[θ ≤ ns]] is the unique function from [[θ]] to {⊥}.

The Semantic Function

When π ⊢ e : θ,

[[π ⊢ e : θ]] ^{∈} [[π]]^{∗} ⟶_{K} [[θ]] where [[π]]^{∗} =^{def} \begin{matrix}∏ & S \\ v^{∈}dom π \end{matrix}[[πv]].

The Intersection Operator

5. [[θ & θ′]], along with [[θ & θ′ ≤ θ]] and [[θ & θ′ ≤ θ′]], is a limit in S of [[θ]], [[θ′]], and their common supertypes:

[figure: [[θ′′_{1}]]; [[θ′′_{2}]]; ⋯; [[θ′′_{n}]]; [[θ]]; [[θ′]]; [[θ & θ′]]; [[π]]^{∗}; [[θ & θ′ ≤ θ]]; [[θ & θ′ ≤ θ′]]; [[π ⊢ e : θ]]; [[π ⊢ e : θ′]]]

[[θ & θ′]] = {⟨x, x′⟩ | x ^{∈} [[θ]] and x′ ^{∈} [[θ′]] and

∀θ′′. (θ ≤ θ′′ and θ′ ≤ θ′′) implies [[θ ≤ θ′′]]x = [[θ′ ≤ θ′′]]x′ } [[θ & θ′ ≤ θ]]⟨x, x′⟩ = x [[θ & θ′ ≤ θ′]]⟨x, x′⟩ = x′.

A Special Case

[[ns]]

[[a: int]]

[[b: real]]

[[a: int & b: real]]

[figure]

[[a: int ≤ ns]]

[figure]

[[b: real ≤ ns]]

[figure]

[[a: int & b: real ≤ a: int]]

[figure]

[[a: int & b: real ≤ b: real]]

[[a: int & b: real]] = {⟨x, x′⟩ | x ^{∈} [[a: int]] and x′ ^{∈} [[b: real]] and

[[a: int ≤ ns]]x = [[b: real ≤ ns]]x′}

= {⟨x, x′⟩ | x ^{∈} [[int]] and x′ ^{∈} [[real]]}
= [[int]] × [[real]]

The Opposite Extreme

[figure: ^{[[value]]}; [[int]]; [[bool]]; [[int & bool]]; [[int ≤ value]]; [[bool ≤ value]]; [[int & bool ; ≤ int]]; [[int & bool ; ≤ bool]]]

[[int & bool]] = {⟨x, x′⟩ | x ^{∈} [[int]] and x′ ^{∈} [[bool]] and

[[int ≤ value]]x = [[bool ≤ value]]x′}

= {⟨x, x′⟩ | x ^{∈} [[int]] and x′ ^{∈} [[bool]] and x = x′}
≃ [[int]] ∩ [[bool]]

Some Semantic Equations

When v ^{∈} dom π:

\overline{π ⊢ v : πv}  [[π ⊢ v : πv]]η = ηv
\frac{π ⊢ p : θ}{π ⊢ (ι ≡ p) : (ι: θ)}  [[π ⊢ (ι ≡ p) : (ι: θ)]] = [[π ⊢ p : θ]]

When θ does not have the form ι: ⋯:

\frac{π ⊢ p : θ}{π ⊢ (p, ι ≡ p′) : θ}  [[π ⊢ (p, ι ≡ p′) : θ]] = [[π ⊢ p : θ]]
\frac{π ⊢ p′ : θ}{π ⊢ (p, ι ≡ p′) : (ι: θ)} [[π ⊢ (p, ι ≡ p′) : (ι: θ)]] = [[π ⊢ p′ : θ]]
\frac{π ⊢ p : θ π ⊢ p : θ′}{π ⊢ p : θ & θ′} \begin{matrix}[[π ⊢ p : θ & θ′]]η \\ = ⟨[[π ⊢ p : θ]]η, [[π ⊢ p : θ′]]η⟩ \end{matrix}

A Derivation

Let π be x: int, y: real.

π ⊢ x : int  [[π ⊢ x : int]]η = ηx
π ⊢ (a ≡ x) : a: int  [[π ⊢ (a ≡ x) : a: int]]η = ηx
π ⊢ (a ≡ x, b ≡ y) : a: int [[π ⊢ (a ≡ x, b ≡ y) : a: int]]η = ηx
π ⊢ y : real  [[π ⊢ y : real]]η = ηy
π ⊢ (a ≡ x, b ≡ y) : b: real [[π ⊢ (a ≡ x, b ≡ y) : b: real]]η = ηy

π ⊢ (a ≡ x, b ≡ y) : a: int & b: real [[π ⊢ (a ≡ x, b ≡ y) : a: int & b: real]]η = ⟨ηx, ηy⟩

An Untyped Semantics

[[p]] ^{∈} U^{Var} ⟹_{K} U,

where U satisfies the isomorphism

[figure: Values_{⊥,⊤} × U^{I} × (U ⟹_{K} U); U.; Φ; Ψ]

Some embedding-projection pairs

[figure: _{Values_{⊥,⊤}}; U; Φ_{p}; Ψ_{p}]  \begin{matrix}Φ_{p}x = Φ⟨x, ⊥, ⊥⟩ \\ Ψ_{p}u = (Ψu)_{1} \end{matrix}
[figure: U^{I}; U; Φ_{r}; Ψ_{r}]  \begin{matrix}Φ_{r}r = Φ⟨⊥, r, ⊥⟩ \\ Ψ_{r}u = (Ψu)_{2} \end{matrix}
[figure: U ⟹_{K} U; U; Φ_{f}; Ψ_{f}]  \begin{matrix}Φ_{f}f = Φ⟨⊥, ⊥, f⟩ \\ Ψ_{f}u = (Ψu)_{3} \end{matrix}
[figure: U; U; Φ_{ι}; Ψ_{ι}]  \begin{matrix}Φ_{ι}x = Φ_{r}[ ⊥ | ι: x] \\ Ψ_{ι}u = Ψ_{r}u ι \end{matrix}

Untyped Semantic Equations

[[v]]ε = ε v
[[c]]ε = Φ_{p} v_{c}
[[ι ≡ p]]ε = Φ_{ι}([[p]]ε)
[[p.ι]]ε = Ψ_{ι}([[p]]ε)
[[λv. p]]ε = Φ_{f}(λu ^{∈} U. [[p]][ ε | v: u])
[[p p′]]ε = Ψ_{f}([[p]]ε)([[p′]]ε)
[[p, ι ≡ p′]]ε = Φ⟨Ψ_{p}([[p]]ε), [ Ψ_{r}([[p]]ε) | ι: [[p′]]ε], Ψ_{f}([[p]]ε)⟩
[[p, λv. p′]]ε = Φ⟨Ψ_{p}([[p]]ε), Ψ_{r}([[p]]ε), Ψ_{f}([[λv. p′]]ε)⟩
[[μv. p]]ε = Y_{U}(λu ^{∈} U. [[p]][ ε | v: u])

[[if p then p′ else p′′]]ε

= \{ \begin{matrix}[[p′]]ε & when Ψ_{p}([[p]]ε) = true \\ [[p′′]]ε & when Ψ_{p}([[p]]ε) = false \\ ⊤ & when Ψ_{p}([[p]]ε) = ⊤ \\ ⊥ & otherwise \end{matrix}

Logical Relations

ρ[θ] ⊆ [[θ]] × U

⟨x, y⟩ ^{∈} ρ[int] iff x = Ψ_{p}y ^{∈} [[int]]

(similarly for real, bool, value)

⟨x, y⟩ ^{∈} ρ[ι: θ] iff ⟨x, Ψ_{ι}y⟩ ^{∈} ρ[θ]
⟨f, g⟩ ^{∈} ρ[θ → θ′] iff ∀⟨x, y⟩ ^{∈} ρ[θ]. ⟨f x, Ψ_{f}g y⟩ ^{∈} ρ[θ′]
⟨⟨x, x′⟩, y⟩ ^{∈} ρ[θ & θ′] iff ⟨x, y⟩ ^{∈} ρ[θ] and ⟨x′, y⟩ ^{∈} ρ[θ′]

Lemma

The relations ρ[θ] are complete, i.e. 1. ⟨⊥, ⊥⟩, ⟨⊤, ⊤⟩ ^{∈} ρ[θ].

2. If x_{0} ⊑ x_{1} ⊑ ⋯ and y_{0} ⊑ y_{1} ⊑ ⋯ are increasing sequences

such that each ⟨x_{i}, y_{i}⟩ ^{∈} ρ[θ], then

⟨⨆_{i} x_{i}, ⨆_{i} y_{i}⟩ ^{∈} ρ[θ].

Lemma

If θ ≤ θ′ and ⟨x, y⟩ ^{∈} ρ[θ] then ⟨[[θ ≤ θ′]]x, y⟩ ^{∈} ρ[θ′].

The Logical Relations Theorem

Suppose

π ⊢ p : θ
∀v ^{∈} dom π. η v ^{∈} [[π v]]
ε ^{∈} U^{Var}
∀v ^{∈} dom π. ⟨η v, ε v⟩ ^{∈} ρ[π v].

Then

⟨[[π ⊢ p : θ]]η, [[p]]ε⟩ ^{∈} ρ[θ].

Convexity

If y ⊑ y′ ⊑ y′′ and ⟨x, y⟩, ⟨x, y′′⟩ ^{∈} ρ[θ] then ⟨x, y′⟩ ^{∈} ρ[θ].

The Bracketing Conjecture

For all types θ,

ϕ[θ] ⊆ ρ[θ] ⊆ ψ[θ]^{†},

where

[figure: [[θ]]; U; ϕ[θ]; ψ[θ]]

are embedding-retraction pairs:

ϕ[int]x = Φ_{p}x
ψ[int]y = if Ψ_{p}x ^{∈} [[int]] then Ψ_{p}x else ⊥

(similarly for real, bool, value)

ϕ[ι: θ]x = Φ_{ι}(ϕ[θ]x)
ψ[ι: θ]y = ψ[θ](Ψ_{ι}y)
ϕ[θ → θ′]f = Φ_{f}(ψ[θ] ; f ; ϕ[θ′])
ψ[θ → θ′]g = ϕ[θ] ; Φ_{f}g ; ψ[θ′]
ϕ[θ & θ′]⟨x, x′⟩ = ??
ψ[θ & θ′]y = ??.

(This conjecture is known to hold in the absence of intersection.)

Expressing Implicit Conversions

Suppose θ ≤ θ′. Then, by the bracketing conjecture,

\begin{aligned}⟨x, ϕ[θ]x⟩ & ∈ & ρ[θ] \\ ⟨[[θ ≤ θ′]]x, ϕ[θ]x⟩ & ∈ & ρ[θ′] \\ [[θ ≤ θ′]]x & = & ψ[θ′](ϕ[θ]x). \end{aligned}

Typed Meanings as a Function of Untyped Meanings

Suppose

π ⊢ p : θ
∀v ^{∈} dom π. η v ^{∈} [[π v]].

By the bracketing conjecture,

∀v ^{∈} dom π. ⟨η v, ϕ[π v](η v)⟩ ^{∈} ρ[π v].

By the logical relations theorem,

⟨[[π ⊢ p : θ]]η, [[p]](λv. ϕ[π v](η v))⟩ ^{∈} ρ[θ].

By the bracketing conjecture,

[[π ⊢ p : θ]]η = ψ[θ]([[p]](λv. ϕ[π v](η v))).

(This implies that the intrinsic typed semantics is coherent.)

An Extrinsic PER Semantics

Let

σ[θ] =^{def} ρ[θ]^{†} ; ρ[θ] ⊆ U × U.

Obviously, σ[θ] is symmetric. Moreover, since ψ[θ] is a function, ψ[θ]^{†} ; ψ[θ] ⊆ Id_{[[θ]]}, so that the bracketing conjecture gives

\begin{aligned}σ[θ] ; σ[θ] & = & ρ[θ]^{†} ; ρ[θ] ; ρ[θ]^{†} ; ρ[θ] \\ & ⊆ & ρ[θ]^{†} ; ψ[θ]^{†} ; ψ[θ] ; ρ[θ] ⊆ ρ[θ]^{†} ; ρ[θ] = σ[θ]. \end{aligned}

Thus σ[θ] is transitive, and thus a partial equivalence relation. • ⟨y, y⟩ ^{∈} σ[θ] means that y represents some value of type θ.

• ⟨y, y′⟩ ^{∈} σ[θ] means that y and y′ represent the same value of type θ.

An Inductive Definition

⟨y, y′⟩ ^{∈} σ[int] iff Ψ_{p}y = Ψ_{p}y′ ^{∈} [[int]]

(similarly for real, bool, value)

⟨y, y′⟩ ^{∈} σ[ι: θ] iff ⟨Ψ_{ι}y, Ψ_{ι}y′⟩ ^{∈} σ[θ]
⟨g, g′⟩ ^{∈} σ[θ → θ′] iff ∀⟨y, y′⟩ ^{∈} σ[θ]. ⟨Ψ_{f}g y, Ψ_{f}g′ y′⟩ ^{∈} σ[θ′]
⟨y, y′⟩ ^{∈} σ[θ & θ′] iff ⟨y, y′⟩ ^{∈} σ[θ] and ⟨y, y′⟩ ^{∈} σ[θ′]

The Typeless Semantics Respects the PER Semantics

Suppose ε, ε′ ^{∈} U^{Var} satisfy

∀v ^{∈} dom π. ⟨ε v, ε′ v⟩ ^{∈} σ[π v] = ρ[π v]^{†} ; ρ[π v]. Then there is an η ^{∈} [[π]]^{∗} such that

∀v ^{∈} dom π. ⟨η v, ε v⟩, ⟨η v, ε′ v⟩ ^{∈} ρ[π v].

Thus, by the logical relations theorem,

⟨[[π ⊢ p : θ]]η, [[p]]ε⟩, ⟨[[π ⊢ p : θ]]η, [[p]]ε′⟩ ^{∈} ρ[θ],

so that

⟨[[p]]ε, [[p]]ε′⟩ ^{∈} σ[θ].