Types, prefixes, and relations under prefixes 

Get Complete Project Material File(s) Now! »

Properties of relations under prefixes

Instantiation in ML consists of applying a substitution: given a type scheme σ = ∀ (α¯) , its instances are of the form θ(τ ) for a substitution θ whose domain is included in α¯. This definition of ML instantiation implies some useful properties, which we expect to hold in MLF too.
In Section 2.1, we establish a few properties based on the observation of the skele-tons. In ML, a type σ and its instances have comparable structures, that is, comparable skeletons. More precisely, the skeleton of the instance θ(τ ) corresponds to the skeleton of σ where quantified variables α¯ are substituted by θ. Hence, the skeleton of θ(τ ) is the skeleton of σ, except on occurrences corresponding to quantified variables. In MLF, we define a partial order 6/ on occurrences (or, equivalently, on skeletons) that captures the idea that only quantified variables can be instantiated. This result is stated as Prop-erty 2.1.3.ii, which concerns the instance relation. Conversely, the abstraction relation is, intuitively, a reversible relation. Hence, we expect it to keep skeletons unchanged; this is stated by Property 2.1.3.i. Another property of the ML instance relation con-cerns free variables: if α is free in σ, then α is free in all instances of σ (and more precisely, α appears at least at the same occurrences). Such a result also holds in MLF, as stated by Lemma 2.1.4, which can be first read by taking Q1 = ∅. A straightforward result in ML states that monotypes have no instances (except themselves). This is also true in MLF, up to equivalence, as stated by Lemma 2.1.6.
In some implementations of ML, such as OCaml, some type variables become aliases during unification. For example, the unification of α → α and β → β might create an alias from α to β, which we write (α = β) (1). Then each time a type variable is encountered, the implementation calls a function repr which finds its representative. To pursue the example, the representative of α is β and the representative of β is β.
Such a mechanism plays quite an important role in the efficiency of unification in ML. However, it is seldom formalized. In MLF, the alias from α to β appears directly in the prefix, in the form (1). In Section 2.2, we define the representative of a variable, according to a given prefix, and establish a few properties. The representative of α in Q is written Q[α], and the bound of the representative (which, intuitively, is the bound meant for α), is written Q(α).
Section 2.3 provides different ways to transform derivations of equivalence, abstrac-tion, or instance judgments, the goal being to force some invariants. A first set of straightforward restrictions defines restricted derivations; another independent restric-tion, which concerns only the context rule R-Context-R, defines thrifty derivations. Property 2.3.3 shows that derivations that are restricted and thrifty are as expressive as normal derivations. Such restrictions are useful to discard pathological cases, which would shamelessly obfuscate some proofs.
In Section 2.4 we study contexts, which represent types with a hole [ ]. We use them in Section 2.5 to define a set of rules that replaces context rules by explicit contexts. More precisely, context rules such as R-Context-R, R-Context-Flexible or R-Context-Rigid are removed, and all other rules mention explicitly a context C. As expected, these new relations are as expressive as the original relations. Another independent set of rules is introduced, that defines the relations −@α¯ and vα¯ . These relations are similar to −@ and v, but seriously restrict rules A-Hyp and I-Hyp. In order to preserve the expressiveness, we introduce new rules, namely A-Up’, A-Alias’, I-Up’, and I-Alias’. The derivations with −@α¯ and vα¯ make the transformations on binders more explicit than with −@ and v. More precisely, whereas the latter only consider unification of binders (rules A-Hyp and I-Hyp), the former distinguish local unification of binders (rules A-Alias’ and I-Alias’), extrusion of binders (rules A-Up’ and I-Up’), and unification of binders with the prefix (rules A-Hyp’ and I-Hyp’).
In Section 2.6, we define atomic relations. Atomic relations can decompose an abstraction derivation or an instance derivation into a sequence of atomic and effective transformations. We use atomic decomposition to show some confluence results; indeed, once a derivation is decomposed into a sequence of transformations, confluence can be proved by considering all possible pairs of transformations.
The main result of Section 2.7 is Property 2.7.7.i, which shows that the equivalence relation is the symmetric kernel of the instance relation. This result is proved by associating a three-variable polynomial to each type, and by showing that the instance relation strictly decreases the polynomials if and only if it is irreversible (that is, when it is not an equivalence). Polynomials are also used to show that the relation −@ considered as an order on types (under a given prefix) is well-founded. Such a result is used in the following section to show confluence between −@ and v. Indeed, the main result of Section 2.8 is the Diamond Lemma (Lemma 2.8.4), which states the confluence of −@ and v under an unconstrained prefix.

Projections and instantiation

Skeletons, projections and occurrences were defined formally in section 1.3. We have seen that a skeleton is a tree composed of type variables, type constructors g n (such as the arrow →), and ⊥. Intuitively, only the leaves labeled with ⊥ can be instantiated. This is captured by the following definition, which introduces the notation 6/. Then, we immediately show that this relation is actually a partial order on skeletons.
Definition 2.1.1 We define a relation on skeletons, written 6/, as follows: t1 6/ t2 holds if and only if dom(t1) ⊆ dom(t2) and for all u ∈ dom(t1), we have t1 /u 6= t2/u implies t1/u = ⊥.
The definition immediately applies to projections since they are isomorphic to skeletons (see Section 1.3.2). By extension, we write σ1 6/ σ2 to mean σ1/ 6/ σ2/.
Properties 2.1.2
The relation 6/ is a partial order.
If t1 6/ t2 holds, then for any substitution θ, we have θ(t1) 6/ θ(t2).
If t1 6/ t2 holds, then for any skeleton t, we have t[t1 /α] 6/ t[t2/α].
These properties are direct consequences of Definition 2.1.1.
See details in the Appendix (page 233).
As a consequence of Property 2.1.2.i, if we have σ1 6/ σ2 and σ2 6/ σ1 , then σ1/ = σ2/ (that is, proj(σ1 ) = proj(σ2 )). However, this does not imply σ1 = σ2 in general, as shown by example 1.3.1. Actually, it does not imply σ1 ≡ σ2 either, since types contain more information than skeletons.
Projections, instantiation and free variables
Projections are stable under abstraction, but not (in general) under instantiation. This is stated more precisely by the following lemma:
Properties 2.1.3
If (Q) σ1 −@ σ2 , then (∀ (Q) σ1)/ = (∀ (Q) σ2 )/.
If (Q) σ1 v σ2 , then ∀ (Q) σ1 6/ ∀ (Q) σ2 .
Proof: Property i : It is shown by induction on the derivation of (Q) σ1 −@ σ2.
Case A-Equiv: By Property 1.5.4.i (page 50).
Case R-Trans: By induction hypothesis.
Case A-Hyp: By hypothesis, we have (α = σ1 ) ∈ Q and σ2 is α. We have ∀ (Q) σ2 = ∀ (Q) α ≡ ∀ (Q) σ1 by Eq-Var?. Consequently, ∀ (Q) σ1 ≡ ∀ (Q) σ2 holds. We get the expected result by Property 1.5.4.i (page 50).
Case R-Context-R: We have σ1 = ∀ (α σ) σ10 and σ2 = ∀ (α σ) σ20. Besides, the premise is (Q, α σ) σ10 −@ σ20. Hence, by induction hypothesis, we have (∀ (Q, α σ)
σ10)/ = (∀ (Q, α σ) σ20)/, which is the expected result.
Case R-Context-Rigid: Like for the case R-Context-L in the proof of Prop-erty 1.5.4.i (page 50).
Property ii : It is shown by induction on the derivation of (Q) σ1 v σ2 .
Case I-Abstract: By Property i.
Case R-Trans: By induction hypothesis and transitivity of 6/ (Property 2.1.2.i).
Case I-Bot: We have σ = ⊥, thus (∀ (Q) σ1 )/ = ⊥/. We get the expected result by observing that ⊥ 6/ (∀ (Q) σ2 ) always holds.
Case R-Context-Flexible: We have σ1 = ∀ (α ≥ σ10) σ (1) and σ2 = ∀ (α ≥ σ20)
(2). The premise is (Q) σ10 v σ20. By induction hypothesis, we know that (∀ (Q) σ10)/ 6
(∀ (Q) σ20)/, that is ΘQ(proj(σ10))/ 6 ΘQ(proj(σ20))/ (3) by Property 1.3.3.i (page 40). We have
(∀ (Q) σ1)/= (∀ (Q) ∀ (α ≥ σ10) σ)/ from (1)
Finally, we have shown ∀ (Q) σ1/ 6/ ∀ (Q) σ2/, which is the expected result.
Case I-Hyp is similar to case A-Hyp above.
◦ Case I-Rigid: ∀ (α ≥ σ) σ0 and ∀ (α = σ) σ0 have the same projection.
Considering an instance (Q) σ1 v σ2 , we need to track occurrences of variables bound in Q but free in σ1. The following lemma states that, in general, such variables also occur in σ2 , at the same occurrence. We require (α σ) to be in the prefix, because the instance relation is only defined under a prefix that binds all free variables of the judgment. Additionally, we require σ not to be equivalent to a monotype, otherwise it could be equivalently substituted by Rule Eq-Mono, and the result would not hold. As a counterexample, take (Q, α = τ ) α v τ (where α cannot be free in τ ).
Lemma 2.1.4 Assume σ is not in T . If (Q, α σ, Q1 ) σ1 ♦ σ2 and (∀ (Q1 ) σ1 )/u = α hold, then (∀ (Q1) σ2 )/u = α. As a consequence, if α ∈ ftv(∀ (Q1 ) σ1), then α ∈ ftv(∀ (Q1 ) σ2 ).
The proof is by induction on the derivation. See the details in Appendix (page 234).
By Definition 1.5.7, a type σ is in T if its normal form has no quantifiers. Like in ML, this means that monotypes cannot be instantiated. Monotypes play an important role in MLF, since they can be inferred (like in ML), whereas polymorphic types can only be propagated. Throughout the proofs, we need to characterize monotypes, variables, or ⊥. Definition 1.5.7 uses normal forms. The following properties use projection.
Properties 2.1.5
σ ∈ T iff for all u ∈ dom(σ) we have σ/u 6= ⊥.
We have σ/ = α iff σ ≡ α.
We have σ/ = ⊥ iff σ ≡ ⊥.
See proof in the Appendix (page 235).
The following lemma is essential: it shows that any instance of a monotype τ is only equivalent to τ , even under a prefix. In particular, assume σ is some polymorphic type scheme. If we have (α = σ) α v σ0, then σ0 must be α (when put in normal form). In other words, even if α is rigidly bound to a polytype σ in the prefix, there is no way to take an instance of it other than α itself. This is also why we say that the information (α = σ) is hidden in the prefix: we can propagate the variable α, bound to σ, but we cannot use its polymorphism. Decidability of type inference relies on this result.
Lemma 2.1.6 If σ1 ∈ T and (Q) σ1 ♦ σ2 hold, then we have (Q) σ1 ≡ σ2.
Proof: By induction on the derivation of (Q) σ1 ♦ σ2 .
Case A-Equiv: By hypothesis, (Q) σ1 ≡ σ2 holds, which is the expected result.
Case R-Trans By induction hypothesis, Property 1.5.11.x (page 54) and R-Trans.
Case A-Hyp and I-Hyp: We have (Q) σ1 v α1 (that is, σ2 is α1 ), and the premise is (α1 σ1) ∈ Q (1). By hypothesis, σ1 ∈ T , thus σ1 ≡ τ (2) for some monotype τ by Property 1.5.11.ii (page 54). By Property 1.5.3.v (page 49) and (2), we get (Q) σ1 ≡
(3). By (2), Eq-Mono, and (1), we get (Q) τ ≡ α1 (4). Hence, (Q) σ1 ≡ α1 holds by R-Trans, (3), and (4). This is the expected result.
Case R-Context-R We have σ1 = ∀ (α σ) σ10 and σ2 = ∀ (α σ) σ20. The premise is (Q, α σ) σ10 ♦ σ20 (5). By hypothesis we have ∀ (α σ) σ10 ∈ T . By Property 2.1.5.i,
we must have σ10 ∈ T . Hence (Q, α σ) σ10 ≡ σ20 holds by induction hypothesis on (5). Consequently, (Q) ∀ (α σ) σ10 ≡ ∀ (α σ) σ20 holds by R-Context-R and this is the expected result.
Case R-Context-Rigid and R-Context-Flexible: We have σ1 = ∀ (α σ) σ0 and σ2 = ∀ (α σ0) σ0 . The premise is (Q) σ ♦ σ0 (6). If α ∈/ ftv(σ0 ), then σ1 ≡ σ2 by Eq-Free, which is the expected result. Otherwise, we necessarily have σ and σ0 in T by Property 2.1.5.i. Hence, (Q) σ ≡ σ0 holds by induction hypothesis on (6). Consequently, (Q) σ1 ≡ σ2 holds by R-Context-L.
Case I-Bot implies σ1 = ⊥, which is a contradiction with the hypothesis σ1 ∈ T , by Property 2.1.5.i.
Case I-Rigid: we have σ1 = ∀ (α ≥ σ) σ0 and σ2 = ∀ (α = σ) σ0. If α ∈/ ftv(σ0), then σ1 ≡ σ2. Otherwise, we necessarily have σ and σ0 in T by Property 2.1.5.i. Con-sequently, σ ≡ τ for some monotype τ . Hence σ1 ≡ σ0[τ /α] (7) holds by Eq-Mono? as well as σ0[τ /α] ≡ σ2 (8). We get the expected result by R-Trans, (7), (8).
Types in MLF are not recursive, thus a type cannot be strictly included in itself. As a consequence, an instance of a given polytype cannot be a strict subterm.
Properties 2.1.7
If σ • / 6/ σ • u/, then u is .
If we have either (Q) σ v α or (Q) α v σ and if α ∈ ftv(σ), then σ ≡ α.
Proof: Property i: We have σ • / 6/ σ • u/. By definition, this implies σ/u 6/ σ/uu. Hence uu, that is u2, is in dom(σ). By immediate induction, we show that ui is in dom(σ) for all natural number i. By definition, dom(σ) is dom(proj(σ)), where proj(σ) is a skeleton (that is, a tree). By construction, dom(proj(σ)) is a finite set of occurrences. .
Property ii: By hypothesis, we have (Q) σ v α (1), or (Q) α v σ (2), and α ∈ ftv(σ), that is, there exists u such that σ/u = α. If u is , then we get the expected result by Property 2.1.5.ii. Otherwise, we have u 6= (3) and (∀ (Q) σ) • u/ = (∀ (Q) α) • / (4) by definition of occurrences. If (1) holds, we get ∀ (Q) σ/ 6/ ∀ (Q) α/ by Property 2.1.3.ii. Hence, we get (∀ (Q) σ) • / 6/ (∀ (Q) σ) • u/ by (4), and we conclude by Property i that u is . Otherwise, (2) holds, and we get (Q) α ≡ σ by Lemma 2.1.6. Hence,
∀ (Q) α/ = ∀ (Q) σ/ (5) holds by Property 1.5.4.i (page 50). By (5) and (4), we get (∀ (Q) σ) • u/ = (∀ (Q) σ) • /. This leads to u = by Property i. In both cases, we have u = , which is a contradiction with (3).

Table of contents :

Abstract / Résumé
Introduction 
Conventions 3
I Types 
1 Types, prefixes, and relations under prefixes 
1.1 Syntax of types
1.2 Préxes
1.3 Occurrences
1.3.1 Skeletons
1.3.2 Projections
1.3.3 Free type variables and unbound type variables
1.3.4 Renamings and substitutions
1.4 Relations under prex
1.5 Type equivalence
1.5.1 Rearrangements
1.5.2 Occurrences and equivalence
1.5.3 Canonical forms for types
1.6 The abstraction relation
1.7 The instance relation
1.8 Examples
2 Properties of relations under préxes 
2.1 Projections and instantiation
2.2 Canonical representatives and bounds in a préx
2.3 Restricted and thrifty derivations
2.4 Contexts
2.5 Local abstraction and instance rules
2.5.1 Context-based rules
2.5.2 Alternative abstraction and alternative instance
2.6 Atomic instances
2.6.1 Definitions
2.6.2 Equivalence between relations
2.7 Equivalence vs instantiation
2.7.1 Polynomials
2.7.2 Weight
2.7.3 Abstraction is well-founded
2.8 Conuence
3 Relations between préxes 
3.1 Substitutions
3.2 Préx instance
3.3 Domains of péxes
3.4 Rules for préx equivalence, abstraction, and instance
3.5 Splitting préxes
3.6 Préxes and Instantiation
4 Unification 
4.1 Definition
4.2 Auxiliary algorithms
4.3 Unication algorithm
4.4 Soundness of the algorithm
4.5 Termination of the algorithm
4.6 Completeness of the algorithm
II The programming language 
5 Syntax and semantics 
5.1 Syntax
5.2 Static semantics
5.2.1 ML as a subset of MLF
5.2.2 Examples of typings
5.3 Syntax-directed presentation
5.4 Dynamic semantics
6 Type Safety 
6.1 Standard Properties
6.1.1 Renaming and substitutions
6.1.2 Strengthening and weakening typing judgments
6.1.3 Substitutivity
6.2 Equivalence between the syntax-directed system and the original system
6.3 Type safety
7 Type inference 
7.1 Type inference algorithm
7.2 Soundness of the algorithm
7.3 Completeness of the algorithm
7.4 Decidability of type inference
8 Type annotations 
8.1 MLF without type annotations
8.2 Introduction to type annotations
8.3 Annotation primitives
III Expressiveness of MLF 
9 Encoding System F into MLF 
9.1 Definition of System F
9.2 Encoding types and typing environments
9.3 Encoding expressions
10 Shallow MLF 
10.1 Denition and characterization
10.2 Expressiveness of Shallow MLF
10.3 Comparison with System F
10.3.1 Introduction
10.3.2 Preliminary results about System F
10.3.3 Encoding shallow types into System F
10.3.4 Encoding Shallow F into System F
10.4 Discussion
11 Language extensions 
11.1 Tuples, Records
11.2 References
11.3 Propagating type annotations
12 MLF in practice 
12.1 Some standard encodings
12.2 Existential Types
12.3 When are annotations needed ?
12.4 A detailed example
12.5 Discussion
Conclusion 
Bibliography 
IV Appendix
A Proofs (Technical details)
Indexes 
Index of rules
Index of notations

GET THE COMPLETE PROJECT