A Polymorphic Lambda-Calculus with Sized Higher-Order Types
Andreas M. Abel · 2006
ion. LEQ-λ ∆, X : pκ ` F ≤ F′ : κ′ ∆ ` λXF ≤ λXF′ : pκ → κ′ Application. There are two kinds of congruence rules for application: one kind states that if functions F and F′ are in the subtyping relation, so are their values F G and F′ G at a certain argument G. LEQ-APP ∆ ` F ≤ F′ : pκ → κ′ p−1∆ ` G : κ ∆ ` F G ≤ F′ G : κ′ The other kind of rules concern the opposite case: If F is a function and two arguments G and G′ are in a subtyping relation, so are the values F G and F G′ of the function at these arguments. However, such a relation can only exist if F is either covariant or contravariant. LEQ-APP+ ∆ ` F : +κ → κ′ ∆ ` G ≤ G′ : κ ∆ ` F G ≤ F G′ : κ′ LEQ-APP− ∆ ` F : −κ → κ ′ −∆ ` G′ ≤ G : κ ∆ ` F G ≤ F G′ : κ′ What about a comparable rule for non-variant constructors? It is derivable: ∆ ` F : ◦κ → κ′ ◦−1∆ ` G ≤ G′ : κ ◦−1∆ ` G′ ≤ G : κ ◦−1∆ ` G = G′ : κ ∆ ` F G = F G′ : κ′ ∆ ` F G ≤ F G′ : κ′ Successor and infinity. LEQ-S-R ∆ ` a : ord ∆ ` a ≤ s a : ord LEQ-∞ ∆ ` a : ord ∆ ` a ≤ ∞ : ord Lemma 2.14 (Validity II) If D :: ∆ ` F ≤ F′ : κ then ∆ ` F : κ and ∆ ` F′ : κ. Proof. By induction on D, using validity of equality (Lemma 2.12) in case of LEQ-REFL. 2.3 Semantics and Soundness In this section we give a semantics to kinds and constructors and show soundness of kinding, constructor equality and subtyping. 30 CHAPTER 2. SIZED HIGHER-ORDER SUBTYPING 2.3.1 Interpretation of Kinds Constructors F of kind κ will be interpreted as operators F which live in the denotation [[κ]] of their kinds. Each kind will be interpreted as a poset (partially ordered set) ([[κ]],v), which is even a complete lattice in each case. Interpretation of base kind ∗. For the moment, we assume a complete lattice [[∗]] of countable sets A ∈ [[∗]] ordered by inclusion, with a maximal set >∗ ∈ [[∗]] such that A ⊆ >∗ for all A ∈ [[∗]]. Later, we will let [[∗]] be the collection of all saturated sets ⊆ SN where >∗ = SN is the set of strongly normalizing terms. So, let [[∗]] : complete lattice of sets A v∗ A′ :⇐⇒ A ⊆ A′ d∗ A := ⋂A (where A ⊆ [[∗]]). By assumption, the poset ([[∗]],v∗) is closed under infima, i. e., for a non-empty subset A ⊆ [[∗]] the infimum d∗ A ∈ [[∗]] exists and is equal to the intersection ⋂ A. Intersection can be extended to empty collections by letting d∗ ∅ = >∗. Once empty intersections are defined, we can define arbitrary suprema by ⊔∗ A := d∗{B ∈ [[∗]] | B w∗ A for all A ∈ A}. Note that we do not require that the supremum is the union of sets; it might actually be something bigger. On the set [[∗]] we assume a binary operation “→” (function space construction) such that A → B v∗ A′ → B′ if A′ v∗ A and B v∗ B′. Interpretation of base kind ord. Constructors “a” of kind ord denote settheoretic ordinals in our semantics. We choose an initial segment [0;>ord] =: [[ord]] of the ordinals for the interpretation of ord. At the moment we leave it open which ordinal >ord denotes; we will fill it in later. [[ord]] := >ord + 1 α vord α′ :⇐⇒ α ≤ α′ Notation. We introduce a notation F vpκ F ′ for polarized inclusion and the notion F vp F ′ ∈ [[κ]] which expresses polarized inclusion for two operators F ,F ′ plus the fact that both are in the set [[κ]]. F v+κ F ′ :⇐⇒ F v F ′ F v−κ F ′ :⇐⇒ F ′ v F F v◦κ F ′ :⇐⇒ F v F ′ and F ′ v F F vp F ′ ∈ [[κ]] :⇐⇒ F ,F ′ ∈ [[κ]] and F vpκ F ′ F v F ′ ∈ [[κ]] :⇐⇒ F v+ F ′ ∈ [[κ]] 2.3. SEMANTICS AND SOUNDNESS 31 Interpretation of function kinds. Semantically, a constructor F of kind pκ → κ′ is a covariant (p = +), contravariant (p = −) or non-variant (p = ◦) operator. We define the posets ([[κ]],v) for higher kinds by induction on κ. [[pκ → κ′]] := {F ∈ [[κ]]→ [[κ′]] | F (G) v F (G ′) ∈ [[κ′]] for all G vp G ′ ∈ [[κ]]} F vpκ→κ F ′ :⇐⇒ F (G) vκ F ′(G) for all G ∈ [[κ]] Lemma 2.15 (Partial order) For each kind κ, the relation v denotes a partial order on [[κ]]. Proof. By induction on κ. For base kinds κ0 ∈ {∗, ord} reflexivity, transitivity and antisymmetry hold by definition. To prove transitivity for higher kinds, assumeκ = pκ1 → κ2 andF1 v F2 ∈ [[κ]],F2 v F3 ∈ [[κ]], and an arbitrary G ∈ [[κ1]]. Since by ind. hyp. G v1 G, we have F1(G) v F2(G) ∈ [[κ2]] and F2(G) v F3(G) ∈ [[κ2]] by definition. By induction hypothesis F1(G) v2 F3(G), and since G was arbitraryF1 vpκ1→κ2 F3. Reflexivity and antisymmetry are proven analogously. Pointwise infima, upper bounds and suprema. For higher kinds, we define inductively pointwise infimum and maximal element as follows. dpκ→κ′ F ∈ [[κ]]→ [[κ′]] for F ⊆ [[pκ → κ′]] ( dpκ→κ′ F)(G) := dκ′{F (G) | F ∈ F} >pκ→κ ∈ [[pκ → κ′]] >pκ→κ(G) := >κ A simple proof by induction on κ shows that > is really the maximal element of [[κ]] for any kindκ. Extending the observations for kind ∗, we can now define empty infima and arbitrary suprema for all kinds. dκ ∅ := > ⊔κ F := dκ{H ∈ [[κ]] | H w F for all F ∈ F} Lemma 2.16 (Supremum is pointwise) ( ⊔pκ→κ′ F)(G) = ⊔κ′{F (G) | F ∈ F}. The posets [[κ]] now are equipped with everything required for complete lattices. Lemma 2.17 (Complete lattice) For all kinds κ, the triple ([[κ]], dκ ,⊔κ) forms a complete lattice. Proof. We only need to show that dκ F ∈ [[κ]] is the well-defined greatest lower bound for F ⊆ [[κ]] by induction on κ. For base kinds, there is nothing to prove. 32 CHAPTER 2. SIZED HIGHER-ORDER SUBTYPING 1. Well-definedness: Show dpκ→κ′ F ∈ [[pκ → κ′]]. Assume G vp G ′ ∈ [[κ]]. Then F (G) v F (G ′) ∈ [[κ′]] for all F ∈ F. Since the infimum is welldefined at kind κ′ by induction hypothesis, this entails ( dpκ→κ′ F)(G) = dκ′{F (G) | F ∈ F} vκ vκ dκ′{F (G ′) | F ∈ F} = (dpκ→κ′ F)(G ′). 2. Lower bound: Show dpκ→κ′ F vpκ→κ F for all F ∈ F. Assume G ∈ [[κ]] arbitrary. Since by induction hypothesis, dκ′ is a lower bound, ( dpκ→κ′ F)(G) = dκ′{F (G) | F ∈ F} vκ F (G) for any F ∈ F. 3. Greatest lower bound: Let H v F ∈ [[pκ → κ′]] for all F ∈ F. Show H vpκ→κ dpκ→κ′ F. For G ∈ [[κ]] arbitrary, H(G) vκ F (G) for any F ∈ F by assumption. Since by induction hypothesis dκ′ is a greatest lower bound, H(G) vκ dκ′{F (G) | F ∈ F} = (dpκ→κ′ F)(G). 2.3.2 Semantics of Constructors In the following we develop a semantics of constructors through their derivations of well-kindedness. This indirect path is necessary since the constructors are domain-free. E. g., it is not determined which function is denoted by the constructor λXX; it could be the identity function on [[κ]] for any kind κ. In joint work with Ralph Matthes I have investigated polarized kinding and semantics of Church-style constructors [AM04]. There, λX :+κ.X denotes exactly one set-theoretic function: the identity on [[κ]]. The following development resembles closely the cited work, however, we take the detour via derivations here. Sound valuations. Let θ be a mapping from constructor variables to sets. We say θ ∈ [[∆]] if θ(X) ∈ [[κ]] for all (X : pκ) ∈ ∆. A partial order on valuations is established as follows: θ v θ′ ∈ [[∆]] :⇐⇒ θ(X) vp θ′(X) ∈ [[κ]] for all (X : pκ) ∈ ∆ We use v− for w and v◦ for =, and v+ as synonym for v. It is clear that θ vq θ′ ∈ [[∆]] iff θ(X) vpq θ′(X) ∈ [[κ]] for all (X : pκ) ∈ ∆. 2.3. SEMANTICS AND SOUNDNESS 33 Lemma 2.18 If θ v θ′ ∈ [[∆]], then θ vp θ′ ∈ [[p−1∆]]. Proof. By cases on p. Interesting is only case p = ◦. Assume X : qκ ∈ [[◦−1∆]], which is only possible if q = ◦ and X : ◦κ ∈ [[∆]]. We have to show θ(X) v◦◦ θ′(X) ∈ [[κ]] which follows from the premise of the lemma. Remark 2.19 The opposite implication does not hold in case p = ◦. Denotation of constructors. If D :: ∆ ` F : κ and θ is a function from type variables to sets, we define the set [[D]]θ by recursion on D as follows. Case D = X : pκ ∈ ∆ p ≤ + ∆ ` X : κ We define [[D]]θ = θ(X). Case D = C :κ ∈ Σ ∆ ` C : κ In this case, we simply return the semantics of C, which is defined elsewhere: [[D]]θ = Sem(C). Case D = D′ ∆,X : pκ ` F : κ′ ∆ ` λXF : pκ → κ′ The semantics of D is a function over [[κ]], defined by [[D]]θ(G ∈ [[κ]]) := [[D]]θ[X 7→G]. Note that this is only possible if we know the domain of the function (κ, in this case). This is the reason why we define the semantics of derivations instead of constructors (where we would not have the domain available).