Subtyping with Singleton Types

David Aspinall

Department of Computer Science, University of Edinburgh, U.K.

                              e-mail: da@dcs.ed.ac.uk

Abstract. We give syntax and a PER-model semantics for a typed λ-calculus with subtypes and singleton types. The calculus may be seen as a minimal calculus of subtyping with a simple form of dependent types. The aim is to study singleton types and to take a canny step towards more complex dependent subtyping systems. Singleton types have applications in the use of type systems for specification and program extraction: given a program P we can form the very tight specification {P } which is met uniquely by P. Singletons integrate abbreviational definitions into a type system: the hypothesis x : {M} asserts x = M. The addition of singleton types is a nonconservative extension of familiar subtyping theories. In our system, more terms are typable and previously typable terms have more (non-dependent) types.

1 Introducing Singletons and Subtyping

Type systems for current programming languages provide only coarse distinctions amongst data values: Real, Bool, String, etc. Constructive type theories for program specification can provide very fine distinctions such as {x ∈ Nat | Prime(x)}, but often terms contain noncomputational parts, or else type-checking is undecidable. We want to study type systems in between where terms do not contain unnecessary codes and, ideally, type-checking is decidable. When types express requirements for data values more accurately, it can help to eliminate more run-time errors and to increase confidence in program transformations which are type-preserving.

Singleton types express the most stringent requirement imaginable. Suppose fac stands for the expression:

μf. λx. if x = 0 then 1 else x ∗ (f(x − 1))

Then {fac} is a specification of the factorial function, and

fac : {fac}

says that fac satisfies the specification {fac}. This is an instance of the principal assertion for singleton types, M : {M}. But syntactic identity is too stringent; we can write the factorial function in other ways and it would be useful if when fac′ is an implementation of the factorial function, we also have fac′ : {fac}. This suggests that we let {M} stand for the collection of terms equal to M in some theory of equality, so {M} denotes an equivalence class of terms, rather than a singleton set.

This paper appears in Proc. CSL’94, Kazimierz, Poland. Springer Lecture Notes in Computer Science,

Although we want types to be more expressive, this should not sacrifice the usability of the type system. More types can lead to more polymorphism: a term may possess several types, and the type system should recognize this and allow the programmer as much flexibility as possible. Subtyping systems provide flexibility by allowing a term of some type A to be used where one of a ‘larger’ type B is expected. The characteristic rule for subtyping is known as subsumption, which captures this kind of polymorphism:

\begin{matrix}M : A & A ≤ B \\ M : B \end{matrix}  (sub)

Subsumption at ground types suggests subtyping at higher types. For example, a function defined on Int may be used where one defined only on Nat is needed, because Nat ≤ Int means that every natural number will be a suitable argument. So we expect that Int → Int is a subtype of Nat → Int.

Subtyping leads to a stratified notion of equality. Because terms may have many types, the equality of two terms can be different at different types. Indeed, consider two different functions on integers:

(λx: Int. if x > 0 then x else 2 ∗ x) ≠ (λx: Int. x) : Int → Int

which have equal values at every natural:

(λx: Int. if x > 0 then x else 2 ∗ x) = (λx: Int. x) : Nat → Int

If in some context only arguments of type Nat are supplied, these functions are interchangeable; useful perhaps for program transformation during compilation.

This view of equality influences our treatment of singleton types. Because equality can vary at different types, we think of {M} as a family of equivalence classes indexed by a type. We attach a tag to the singleton, which denotes the type at which we “view” the term. The introduction rule for singletons is:

{M : A \atop M : \{M\}_{A}}  (\{\}-I)

In fact, the type tag can be important for another reason: the type A might affect the interpretation of M, as well as its equivalence class of terms (although this is not the case for the semantics we give later). Imagine a model in which the integers are constructed using pairs of naturals: the pair ⟨m, n⟩ codes the integer (m−n). Then the interpretation [[3: Int]] is quite different from [[3: Nat]], and the semantic types have different equality relations associated. (Of course, there is an obvious coercion from [[Nat]] to [[Int]].) To allow for typed interpretations we need to know the type given to a term in a singleton, but unless it is recorded somehow it cannot be determined from a typing derivation.

There is no typing elimination rule for singleton types, but we have a subtyping rule that says that a singleton type is a subtype of its type tag:

{M : A \atop \{M\}_{A} ≤ A}  (sub-\{\})

which allows us to deduce M : A from M : {N}_{A} via (sub).

For us, singleton types have a non-informative flavour. In other words, we have no term operators corresponding to singleton introduction and elimination. This contrasts with constructive type theories utilising propositions-as-types, where singletons might be treated akin to a propositional equality type and given a powerful elimination operator. In our approach, membership of singletons corresponds to definitional equality, which is usually decidable. A technical side-effect of non-informative types is that the meta-theory of our system is harder to deal with, because the rules are less syntax-directed.^{1} Notice that the presence of (sub) already means that the typing rules are not syntax-directed.

The theory of equality we choose to incorporate in singleton types is a natural typed equational theory for the terms. The typing assertion M : {N}_{A} asserts that M and N are equal at type A, so instead of axiomatizing a separate judgement form Γ ⊢ M = N : A, we use typing rules with the form Γ ⊢ M : {N}_{A} directly. The usual rule of β-equality is admissible. This formulation is nicer to deal with than one defined using a rule of untyped β-conversion.

The system λ_{≤} (“lambda-sub”)[Car88a] is formed by adding subtyping to the simplytyped λ-calculus. In the remainder of the paper we shall study the addition of singleton types to λ_{≤}; we call the resulting system λ_{≤{}} (“lambda-sub-singleton”). First, the next section outlines some uses for type systems with singleton types. Then in Section 3 we present the complete definition of λ_{≤{}} and in Section 4 we establish some of its meta-theoretic properties. Section 5 gives a PER semantics and shows soundness; Section 6 concludes.

2 Using Singleton Types

Singleton types as specifications. This work arose from a desire to understand the formal system of a specification language called ASL+ [SST92, Asp95]. ASL+ extends the algebraic specification language ASL [SW83] with constructs from type-theory (principally λ-abstraction) for parameterising specifications and programs. ASL consists of a collection of specification building operators (SBOs) which are used for putting together specifications; ASL-level specifications form the base types of the ASL+ λ-calculus.

1A set of rules is called syntax-directed if the last rule used in a derivation of any statement J is uniquely determined by the structure of J.

One of the extensions provided by ASL+ is the ability to express specifications of parameterised programs (like functor signatures in Extended ML [KST94]). To do this, we need dependent function spaces to specify a function which satisfies a specification that depends on its argument. Singletons turn a program into a very tight specification which we can use with other SBOs in the body of the function specification. A trivial example is an identity functor, which returns its argument:

     functor Id(X:S):S = X

In ASL+, this could be specified by ΠX: S. {X}. A less trivial example is SORT, which specifies a parameterised program that, given a program implementing an order relation Ord (a type t and an ordering le on t), returns a sorting function sort for sorting lists of elements of t according to le.

SORT =_{def} Π Ord:ORD . enrich {Ord} by

sign sort : t list → t list

axioms (some axioms specifying that sort(x) is a sorted copy of x with respect to le)

end

The important thing to notice here is the use of {Ord} to require that applications of programs satisfying SORT should be an extension of the actual parameter with a sorting function that operates on exactly the same type t.

Singleton types and subtyping. Adding singleton types to well-known subtyping systems such as λ_{≤} and its second-order variants is not a conservative extension. More typing statements become provable, both because more terms are typable and because terms have more (non-dependent) types.

We illustrate this with a simple example. Consider the identity function on real numbers:

id_{Real} =_{def} λx: Real. x

Suppose the fact that Int ≤ Real. Then in λ_{≤}:

                           id_{Real} : Real → Real
                                  : Int → Real
                                 : Int → Int

But the third typing is perfectly reasonable; the identity function on reals certainly maps integers to integers. It is provable in our system, via an extended rule for λ-introduction:

          Γ ⊢ Int ≤ Real Γ, x: Real ⊢ x : Real Γ, x: Int ⊢ x : Int
                         Γ ⊢ λx: Real. x : Int → Int

The second hypothesis ensures that the λ-abstraction can be typed. The third hypothesis allows the body to be given a more refined type based on the assumption that the argument type is more refined, according to the first hypothesis. Although a typing rule like this could be added to λ_{≤}, the types Real → Real and Int → Int are incomparable, so this would break the desirable property that every typable term has a minimal type. On the other hand, λ_{≤{}} does have the minimal type property, which we show in Section 4. Not surprisingly, the minimal types are singletons.

As well as more types for previously typable terms, it follows from the example that more (singleton-free) terms become typable when we add singleton types. Suppose

twice_{Int→Int} =_{def} λf: Int → Int. λx: Int. f(f(x)).

Then twice_{Int→Int}(id_{Real}) : Int → Int in λ_{≤{}}, but is untypable in λ_{≤}.

There are more complex cases than these. We can assign a type Πx: A. {M}_{B} to a function λx: A. M that is as informative as the function definition itself, so we can substitute the result of function applications during type-checking and do some amount of equational reasoning. Similarly, we can substitute the arguments supplied to a function into the body before type checking, which is shown next.

Singleton types as definitions. Simple definition by abbreviation is essential for the practical use of a type system in a programming language or proof assistant. If M is a large expression occuring inside N several times, we may write N as

x = M in N′

where N′ is the result of replacing occurrences of M in N with the variable x. If definitions are treated formally, they are introduced as a new concept that extends the type theory causing additional complication. With singleton types we get a form of definition in the system for free, and derive similar rules to those given in [HP91, SP94]. The typed definitions of Severi and Poll [SP94] have the form:

x = M: A in N

This is similar to a λ-abstraction over a singleton type in λ_{≤{}}, applied to the trivially appropriate argument:

(λx: {M}_{A}. N)M

which in turn can be compared with the usual “trick” for writing definitions in systems such as λ^{→} without using a special mechanism:

(λx: A. N)M

Severi and Poll point out three reasons for introducing definitions as a fresh concept:

1. The λ-abstraction λx: A. N might not be permitted in the type-system (if N is a type expression, for example).

2. β-reduction replaces all instances of x in N by M, whereas it is useful to be able to replace instances one-by-one when desired.

3. The information that x = M may lead to a typing for N that otherwise would not be possible.

If definitional bindings must be allowed in more places than λ-abstractions, then it seems necessary to introduce a new concept. For the second point, Severi and Poll introduce a new kind of reduction. A δ-reduction replaces a single instance of x with M. We can similarly introduce a new reduction relation (called Γ-reduction) in λ_{≤{}}:

x ⟶_{Γ} M  if  Γ(x) = {M}_{A}

It is indexed by a context Γ which contains typing assumptions for variables. When the type of a variable x is a singleton type {M}_{A}, then we consider x as being equal to M (at type A), so we may replace occurences of x by M. This reduction can be extended under λ and Π abstractions if certain care is taken; but we will not consider it further in this paper.

Without adding special constructs for definitions we gain the benefit of the third point, extended typing. Interestingly, because of the rules chosen for singleton types, it is not necessary for the term M to be “revealed” to the function body N to make use of the fact that x = M when typing N. The term (λx: A. N)M has exactly the same types as (λx: {M}_{A}. N)M, and moreover the two terms are provably equal in our equational theory.

3 The System λ_{≤{}}

The system λ_{≤{}} is the addition of singleton types to λ_{≤}. We do not restrict λ-introduction, so we get dependent product types in place of the usual arrow types. The combination of type-dependency, subtyping, and the non-informative aspect of the singleton constructor make fundamental properties like subject reduction more difficult to establish than usual.

Pre-types A, pre-terms M, and pre-contexts Γ are given by the grammar:

A : : = P | Πx: A. B | {M}_{A}
M : : = x | λx: A. M | MN
Γ : : = ⟨⟩ | Γ, x : A

There is a set of term variables Var, ranged over by x. There are no type variables, so we assume a set PrimTypes of primitive (or atomic) types, ranged over by P. Subtyping between primitive types is given by a relation, ≤_{Prim} on PrimTypes. Restricting ≤_{Prim} to atomic types ensures that subtyping retains a structural character; that is, two types related by the subtype relation will have a similar shape. Free and bound variables are defined as usual. We identify pre-types, pre-terms, and pre-contexts that are alpha-convertible, and reserve ≡ for this syntactic equivalence.

We write Γ ⊆ Γ′ if each x : A in Γ is also in Γ′. Beta-reduction is defined as usual over terms, and extended to types compatibly with the type-constructors. Notice that there is no application at the level of types; convertible types can only differ within corresponding singleton components.

We use the following judgement forms:

• context formation, Γ Context • type formation, Γ ⊢ A

• typing, Γ ⊢ M : A

• subtyping, Γ ⊢ A ≤ B A judgement is valid iff it is derived using the rules of Tables 1 and 2. We use Γ ⊢ J to range over valid judgements.

We also use an equality judgement as a derived form; Γ ⊢ M = N : A stands for Γ ⊢ M : {N}_{A} when we think of it as meaning equality between terms. Equality between types is written Γ ⊢ A = B which means both Γ ⊢ A ≤ B and Γ ⊢ B ≤ A are valid.

The four judgements are defined simultaneously, in contrast to non-dependent schemes where the subtype relation can be separated from the typing relation. Below we describe the rules related to singleton types; the other rules shown in the tables are mostly standard.

Singleton Types and Equality. Singleton types are formed by the rule (form-{}) and terms of singleton type are introduced by the equality rules, principally reflexivity (eq-refl), which is the singleton introduction rule ({}-I) shown before under a different guise. Symmetry and transitivity are derived using the subtyping rules shown below. We also have the usual rules for equality of λ-abstractions (eq-λ) and applications (eq-app). The rule (eq-λ) is more flexible than usual: it allows one to derive equalities between functions by examining only a restricted domain. (This rule is forced when one has untagged singletons and the usual equal domains equality, which was the inspiration for adding it). It leads to the admissibility of a correspondingly stronger typing rule, via (sub) and (sub-{}):

\begin{aligned}Γ ⊢ A′ ≤ A & Γ, x: A ⊢ M : B & Γ, x: A′ ⊢ M : B′ \\ & Γ ⊢ λx: A. M : Πx: A′. B′ \end{aligned}

which lets us give a more refined type for a function, given a more refined type for its argument. This was used in the id_{Real} example in Section 2.

One might wonder whether we can have deduction from arbitrary hypotheses of equations between terms, assumed via iterated subscripts in the syntax. For example, it holds that Γ, x: {M}_{{N}_{A}} ⊢ M = N : A. In fact, we have only a pure theory of equality since this judgement presupposes that Γ ⊢ M = N : A. This is because the rule (add-hyp) requires that types in contexts must be well-formed; Proposition 4.1 below establishes this formally.

⟨⟩ Context  (empty)
Γ ⊢ A x ∉ dom(Γ)

Γ, x: A Context

(add-hyp)

Γ Context ; Γ ⊢ P  (form-prim)
{Γ, x: A ⊢ B \atop Γ ⊢ Πx: A. B}  (form-Π)
{Γ ⊢ M : A \atop Γ ⊢ \{M\}_{A}}  (form-\{\})
Γ Context ; Γ ⊢ x : Γ(x)  (var)
{Γ, x: A ⊢ M : B \atop Γ ⊢ λx: A. M : Πx: A. B}  (λ)
\begin{matrix}Γ ⊢ M : Πx: A. B & Γ ⊢ N : A \\ Γ ⊢ MN : B[N/x] \end{matrix}  (app)
\begin{matrix}Γ ⊢ M : A & Γ ⊢ A ≤ B \\ Γ ⊢ M : B \end{matrix}  (sub)

Table 1: Rules for contexts, formation, and typing.

{Γ ⊢ M : A \atop Γ ⊢ M = M : A}  (eq-refl)
\begin{matrix}Γ ⊢ A′ ≤ A & Γ, x: A′ ⊢ M = M′ : B′ & Γ, x: A ⊢ M : B \\ Γ ⊢ λx: A. M = λx: A′. M′ : Πx: A′. B′ \end{matrix}  (eq-λ)
\begin{matrix}Γ ⊢ M = M′ : Πx: A. B & Γ ⊢ N = N′ : A \\ Γ ⊢ MN = M′N′ : B[N/x] \end{matrix}  (eq-app)

Note: Γ ⊢ M = N : A is short for Γ ⊢ M : {N}_{A}.

{Γ ⊢ A \atop Γ ⊢ A ≤ A}  (sub-refl)
\begin{matrix}Γ ⊢ A ≤ B & Γ ⊢ B ≤ C \\ Γ ⊢ A ≤ C \end{matrix}  (sub-trans)
Γ Context P ≤_{Prim} P′

Γ ⊢ P ≤ P′

(sub-prim)

\begin{aligned}Γ ⊢ A′ ≤ A & Γ, x: A′ ⊢ B ≤ B′ & Γ, x: A ⊢ B \\ & Γ ⊢ Πx: A. B ≤ Πx: A′. B′ \end{aligned}  (sub-Π)
{Γ ⊢ M : A \atop Γ ⊢ \{M\}_{A} ≤ A}  (sub-\{\})
\begin{matrix}Γ ⊢ M = N : A & Γ ⊢ A ≤ B \\ Γ ⊢ \{N\}_{A} ≤ \{M\}_{B} \end{matrix}  (sub-eq-sym)
{Γ ⊢ M : A \atop Γ ⊢ \{M\}_{A} ≤ \{M\}_{\{M\}_{A}}}  (sub-eq-iter)

Table 2: Rules for equality and subtyping.

Subtyping Singletons. Subtyping of singleton types is provided by three rules. First, we have the rule (sub-{}) shown earlier, which asserts that a singleton is a subtype of the type it is tagged with.

The rule (sub-eq-sym) combines two principles. The first is monotonicity of equality with respect to subtyping: if two terms are equal at a type, say M = N : A, and A ≤ B, then M = N : B also. We can express this via subtyping of singleton types. Generally, as we pass from subtype to supertype, the equivalence class of any particular term gets larger, so {N}_{A} ≤ {N}_{B} and M = N : B via subsumption. The second principle is symmetry of equality, and again we can express the typing rule by a subtyping one (an economy, since we want both). If M = N : A then the equivalence classes of M and N at A must be the same, in particular {N}_{A} ≤ {M}_{A}. These are combined to get the single rule (sub-eq-sym).

The third subtyping rule for singletons (sub-eq-iter) deals with the case when a singleton type is tagged with another singleton type. Observe that we can repeat the operation of taking singletons in the syntax, forming {M}_{A}, {M}_{{M}_{A}}, . . .. We shall consider these types as equal, because singleton types are already the smallest non-empty types we are interested in. And because {M}_{A} inherits equality from A, the equality on terms in {M}_{A} and {M}_{{M}_{A}} is the same. We have {M}_{{M}_{A}} ≤ {M}_{A} alread by (sub-{}), for the other inclusion we need (sub-eq-iter).

4 Basic meta theory of λ_{≤{}}

We state some basic properties of λ_{≤{}}, which lead to proofs of admissibility of rules such as subject β-reduction and β-equality. We then prove the existence of minimal types. Proofs are by straightforward inductions on typing derivations unless stated.

Proposition 4.1 (Contexts and Substitution) 1. Context formation. Suppose Γ Context, where Γ ≡ x_{1} : A_{1}, …, x_{n} : A_{n}. Then

(a) Γ ⊢ A_{i} for 1 ≤ i ≤ n.

(b) If Γ ⊢ J, then FV (J) ⊆ {x_{1}, …, x_{n}}.

2. Weakening. If Γ ⊢ J and Γ ⊆ Γ′ with Γ′ Context, then Γ′ ⊢ J.

3. Substitution. If Γ, x : A, Γ′ ⊢ J and Γ ⊢ N : A, then Γ′, Γ[N/x] ⊢ J[N/x].

4. Bound narrowing. If Γ, x : A, Γ′ ⊢ J and Γ ⊢ A′ ≤ A, then Γ, x : A′, Γ′ ⊢ J.

The next proposition shows some implications between judgements. It is a common practice in the presentation of type theories to simply require the consequences of these as premises in the rules to begin with (often implicitly). Here our rules have fewer premises and we show the implications afterward, but our approach does make some proofs on derivations slightly harder, because sometimes we cannot apply an induction hypothesis directly. This can be circumvented by considering term structure instead, or subderivations of the premises.

Proposition 4.2 (Implied Judgements) 1. If Γ ⊢ J then Γ Context.

2. If Γ ⊢ J and J ≡ M : A, A ≤ B or B ≤ A, then Γ ⊢ A.

3. If Γ ⊢ J and J ≡ M = N : A, N = M : A, {M}_{A} ≤ B or {M}_{B} ≤ A then Γ ⊢ M : A.

Generation principles are important for meta-theoretic analysis. They allow us to decompose a derived judgement into further derivable judgements concerning subterms from the first judgement. Typically a generation principle expresses the general way in which a judgement form may be constructed; for the context and type formation judgements, the generation principles are merely inversions of the rules. The following generation result for the subtyping judgement allows us to show generation for the typing judgement. It also reveals the “structural” nature of subtyping we mentioned before, except in the case of singletons: {M}_{A} can be a subtype of a type B which is not itself a singleton. There is a case according to each syntactic form on either side of the subtyping symbol.

Proposition 4.3 (Subtyping Generation) 1. If Γ ⊢ P ≤ B then B is also an atomic type, say P′, and P ≤_{Prim} P′.

2. If Γ ⊢ Πx: A. B ≤ C then for some A′,B′, we have C ≡ Πx: A′. B′, such that (a) Γ ⊢ A′ ≤ A, (b) Γ, x: A′ ⊢ B ≤ B′, and (c) Γ, x: A ⊢ B.

3. If Γ ⊢ {M}_{A} ≤ B, then Γ ⊢ M : B.

4. If Γ ⊢ A ≤ P′ where A is not a singleton, then A is also an atomic type, say P, and P ≤_{Prim} P′.

5. If Γ ⊢ C ≤ Πx: A′. B′ where C is not a singleton, then for some A,B, we have C ≡ Πx: A. B, such that (a) Γ ⊢ A′ ≤ A, (b) Γ, x: A′ ⊢ B ≤ B′, and (c) Γ, x: A ⊢ B.

6. If Γ ⊢ C ≤ {N}_{B} then for some A,M, we have C ≡ {M}_{A}.

Parts 3 and 6 of this proposition are rather weak, in particular nothing is said about the relation between types A and B. This will be rectified later.

The generation principle for the typing judgement Γ ⊢ M : A looks unusual, because we must account for the possibility that A is a singleton type.

Proposition 4.4 (Typing Generation) 1. If Γ ⊢ x : A, then Γ ⊢ {x}_{Γ(x)} ≤ A 2. If Γ ⊢ λx: A. M : C, then for some A′,B,B′, we have (a) Γ ⊢ A′ ≤ A, (b) Γ, x: A′ ⊢

M : B′, (c) Γ, x: A ⊢ M : B, and (d) Γ ⊢ {λx: A. M}_{Πx:A′.B′} ≤ C.

3. If Γ ⊢ MN : C, then for some A, B, we have that (a) Γ ⊢ M : Πx: A. B, (b) Γ ⊢ N : A, and (c) Γ ⊢ {MN}_{B[N/x]} ≤ C.

In specific instances, the consequence of typing generation can be further broken down using the subtyping generation principle, and so on.

Admissible equality rules. We mention a few important admissible rules of λ_{≤{}}. The symmetry and transitivity of equality

{Γ ⊢ M = N : A \atop Γ ⊢ N = M : A}  (eq-sym)

\begin{matrix}Γ ⊢ L = M : A & Γ ⊢ M = N : A \\ Γ ⊢ L = N : A \end{matrix}  (eq-trans)

are derived via (sub-eq-sym) and (sub-trans), using Proposition 4.2.

The usual rule for β-equality is (perhaps surprisingly) derivable. This is because λx: A. M can be given the tight dependent type Πx: A. {M}_{B} using ({}-I), and so together with (λ) and (app) we can derive:

\begin{matrix}Γ, x: A ⊢ M : B & Γ ⊢ N : A \\ Γ ⊢ (λx: A. M)N = M[N/x] : B[N/x] \end{matrix}  (eq-β)

This rule is used to show β subject reduction.

Removing Singletons. We mentioned that two parts of the subtyping generation principle (Proposition 4.3) are rather weak. If {M}_{A} ≤ B, we would like to find a relationship between the types A and B. When B is not a singleton type, we expect (from the rules) that A ≤ B. However, when B ≡ {N}_{C} for some N and C, we may have A ≤ C or vice-versa, because of rules (sub-eq-sym) and (sub-eq-iter). A generation lemma covering these cases is untidy to state, and difficult to prove directly because of the rule (sub-trans).

Here we define an operation (−)^{{}}, which derives a non-singleton type from a type by repeatedly taking the type tag of a singleton type. A proposition relates a type to its singleton-deleted form; this sufficiently strengthens the generation result to give us a tool to show the admissibility of subject reduction and the minimal type property.

Definition 4.5 (Singleton Removal)

P^{{}} = P_{(Πx: A. B)^{{}} = Πx: A. B}_{({M}_{A})^{{}} = A^{{}}} Proposition 4.6 (Singleton Removal Subtyping) 1. Γ ⊢ A ⟹ Γ ⊢ A ≤ A^{{}}

2. Γ ⊢ A ≤ B ⟹ Γ ⊢ A^{{}} ≤ B^{{}}

3. If B is not a singleton, then Γ ⊢ {M}_{A} ≤ B ⟹ Γ ⊢ A ≤ B Proof. Part 1 is proved by induction on the structure of types, part 2 by induction on the subtyping derivation, using 1 and Proposition 4.2; part 3 follows from 1 and 2 using the same proposition. ⊓ ⊔

Subject Reduction. We can now use the generation principles to show that β-subject reduction holds, for both typing and subtyping. The critical lemma is the case of a one-step outermost reduction. The syntactic proof of this is more involved than usual.

Theorem 4.7 (Subject Reduction) 1. If Γ ⊢ M : A and M ⟶_{β} M′, then Γ ⊢ M′ : A also.

2. If Γ ⊢ A ≤ B and A ⟶_{β} A′, then Γ ⊢ A′ ≤ B also.

3. If Γ ⊢ A ≤ B and B ⟶_{β} B′, then Γ ⊢ A ≤ B′ also. Proof. Simultaneously for a single reduction step, we use induction on the structure of terms and types. For terms, this involves Proposition 4.4 and the equality rules, plus Lemma 4.8 below. For types, we use Proposition 4.3 and Proposition 4.2. ⊓ ⊔

Lemma 4.8 (Outermost β-reduction) Γ ⊢ (λx: A. M) N : C implies Γ ⊢ M[N/x] : C. Proof. By two applications of typing generation (Proposition 4.4), there exist types A_{1}, B_{1}, A_{2}, B_{2} and B such that:

Γ ⊢ λx: A. M : Πx: A_{1}. B_{1}, Γ ⊢ N : A_{1}
Γ ⊢ {(λx: A. M) N}_{B_{1}[N/x]} ≤ C  (*)
Γ ⊢ A_{2} ≤ A, Γ, x: A ⊢ M : B, Γ, x: A_{2} ⊢ M : B_{2}
Γ ⊢ {λx: A. M}_{Πx:A_{2}.B_{2}} ≤ Πx: A_{1}. B_{1}

By Propositions 4.6 and 4.3 and the last of these, we have:

Γ ⊢ Πx: A_{2}. B_{2} ≤ Πx: A_{1}. B_{1},  Γ ⊢ A_{1} ≤ A_{2},  Γ, x: A_{1} ⊢ B_{2} ≤ B_{1}.

Now using (bnd-narrow) and (sub) we have Γ, x: A_{1} ⊢ M : B_{1}. So we can apply the admissible rule (eq-β),

\begin{matrix}Γ, x: A_{1} ⊢ M : B_{1} & Γ ⊢ N : A_{1} \\ Γ ⊢ (λx: A_{1}. M) N = M[N/x] : B_{1}[N/x] \end{matrix}

and by (eq-λ) and (eq-app):

\begin{aligned}Γ ⊢ A_{1} ≤ A & Γ, x: A_{1} ⊢ M = M : B_{1} & Γ, x: A ⊢ M : B & Γ ⊢ N : A_{1} \\ & Γ ⊢ (λx: A. M) N = (λx: A_{1}. M) N : B_{1}[N/x] \end{aligned}

By transitivity:

Γ ⊢ (λx: A. M) N = M[N/x] : B_{1}[N/x]  (†)

Finally, using Proposition 4.2, (sub-trans), and (sub-eq-sym), we can derive:

\begin{matrix}{Γ ⊢ P = Q : D \atop Γ ⊢ \{Q\}_{D} ≤ \{P \}_{D}} & Γ ⊢ \{P \}_{D} ≤ C \\ Γ ⊢ Q : C \end{matrix}

Let (†) and (*) be the premises, so P ≡ (λx: A. M) N, Q ≡ M[N/x], and D ≡ B_{1}[N/x]. Then Γ ⊢ M[N/x] : C as required. ⊓ ⊔

Minimal Types. If a term possesses several types, it is useful both theoretically and pragmatically if one type can always be found that is more general than the others; in subtyping systems, it is minimal. With untagged singletons, minimal types are a triviality: the minimal type for a term M is {M}! When type tags are added, the issue is not so obvious. Here we show a strengthening of typing generation to give minimal types.

The minimal type min_{Γ}(M), of a term M in a context Γ, has the form {M}_{A} for some A. We give a partial inductive definition of min_{Γ}(M) which is shown in the following lemma to be well defined on all Γ, M such that Γ ⊢ M : A for some A.

Definition 4.9 (Minimal Types)

min_{Γ}(x) = {x}_{Γ(x)}
min_{Γ}(λx: A. M) = {λx: A. M}_{Πx:A.min_{Γ,x:A}(M)}
min_{Γ}(MN) = {MN}_{B[N/x]} where (min_{Γ}(M))^{{}} ≡ Πx: A. B and Γ ⊢ N : A

Lemma 4.10 (Existence of Minimal Types) 1. Γ ⊢ M : A  ⟹  Γ ⊢ M : min_{Γ}(M)
2. Γ ⊢ M : A  ⟹  Γ ⊢ min_{Γ}(M) ≤ A

Proof. Simultaneously, by induction on the derivation of Γ ⊢ M : A. ⊓ ⊔

Minimal types are not unique, and the minimal types given by the simple definition of min_{Γ}(M) are not necessarily the simplest syntactically. For example, if Γ ≡ z: α, f: β → {z}_{α}, x: β then min_{Γ}(fx) ≡ {fx}_{{z}_{α}}. But Γ ⊢ fx : {z}_{α} too, and we can show that Γ ⊢ {z}_{α} ≤ {fx}_{{z}_{α}}.

5 A PER Interpretation of λ_{≤{}}

Subtyping calculi have two basic kinds of model. We may choose a typed value space where subsumption is modelled using coercion maps between types. In some sense this is the most general setting, but it requires some way of relating coercion maps to the syntax: either we forgo (sub) and introduce coercions explicitly into the syntax [CL91], or we reconstruct coercions by some translation process [BTCGS91]. Either route requires a coherence property of the interpretation, because of the possibility of different ways of deriving or expressing the analogue of a coercion-free statement, by permuting the positions of coercions. This property can be quite tricky to establish in a general form, and has yet to be demonstrated in a subtyping calculus more complex than F_{≤} (see [CG92]). Here we follow the alternative untyped approach, based on a global value space from which types are carved out. Coercion maps are unnecessary since subtyping amounts to inclusion between types, and the interpretation of a term does not depend on its type. The need for coherency properties can be avoided by defining the interpretation by induction on the structure of raw (coercion-free) terms rather than typing derivations.

The PER model. Recall that a partial equivalence relation (PER) on a set D is a symmetric and transitive relation R ⊆ D × D. The domain of R, dom(R), is the set {d | d R d}, but we often write d ∈ R instead of d ∈ dom(R). The equivalence class {d′ | d′ R d} of d in R is written [d]_{R}. Subtyping will be interpreted as inclusion of PERs, which is simply subset inclusion on D × D.

The construction is mostly standard (see e.g., [CL91, BL90]), but incorporates type-term dependency. We make use of a model of the untyped λ-calculus to interpret terms and to build PERs over.

Definition 5.1 (Lambda Model [HL80]) A lambda model is a triple, D = ⟨D, ·, [[ ]]⟩, where D is a set, · is a binary operation on D and for untyped lambda-terms M, the interpretation of M in an environment ρ: Var ⇀ D is [[M]]ρ ∈ D, such that:

[[x]]ρ = ρ(x)  (var)
[[MN]]ρ = [[M]]ρ · [[N]]ρ  (app)
[[λx. M]]ρ = [[λy. M[y/x]]]ρ  (α)
(∀d ∈ D. [[M]]ρ[x ↦ d] = [[N]]ρ[x ↦ d]) ⟹ [[λx. M]]ρ = [[λx. N]]ρ  (ξ)
(∀x ∈ FV (M). ρ(x) = ρ′(x)) ⟹ [[M]]ρ = [[M]]ρ′  (fv)
∀d ∈ D. [[λx. M]]ρ · d = [[M]]ρ[x ↦ d]  (β)

From the above axioms (except β), we also have:

[[M[N/x]]]ρ = [[M]]ρ[x ↦ [[N]]ρ]  (substitute)

An environment ρ′ extends another ρ, written ρ ⊆ ρ′, if for all variables x, if ρ(x) is defined then ρ′(x) is defined and ρ(x) = ρ′(x). Fix a lambda-model D with domain D. Terms are interpreted as elements of D as usual (we leave the erase operation, which deletes type information, implicit) and types are interpreted as PERs on D.

Pairing and projection operations in the model are defined by:

⟨a, b⟩ = [[λf. fxy]][x ↦ a, y ↦ b]
π_{1}p = p · [[λx. λy. x]][ ]
π_{2}p = p · [[λx. λy. y]][ ]

We first show some constructions for building PERs, and then the interpretation proper.

Definition 5.2 (PER Constructions) We define PERs to interpret the types of λ_{≤{}}, as follows:

• For each primitive type P, we assume a PER R_{P} such that P ≤_{Prim} P′ implies R_{P} ⊆ R_{P′}.

• Let R be a PER and S(a) be a PER for all a ∈ dom(R), such that S(a) = S(b) whenever a R b.

Define the PER Π(R, S) by:

f Π(R, S) g  iff  ∀a, b. a R b ⟹ f · a S(a) g · b

Define the PER Σ(R, S) by:

⟨a_{1}, b_{1}⟩ Σ(R, S) ⟨a_{2}, b_{2}⟩  iff  a_{1} R a_{2} and b_{1} S(a_{1}) b_{2}

• Let R be a PER. Define the PER [p]_{R} by:

m [p]_{R} n  iff  m R n and m R p

The interpretation [[Γ]] of a context Γ is a PER. The interpretation of a type in some context is a family of PERs [[Γ ⊢ A]]g indexed by elements g ∈ [[Γ]] that is invariant under the choice of representative of equivalence class in [[Γ]].

Definition 5.3 (Interpretation of Contexts and Types) For each context Γ, we define a PER [[Γ]] by:

[[⟨⟩]] = D × D
[[Γ, x: A]] = Σ([[Γ]],[[Γ ⊢ A]])

For each context Γ and type A, we define a PER [[Γ ⊢ A]]g, for each g ∈ dom([[Γ]]):

[[Γ ⊢ P]]g = R_{P}
[[Γ ⊢ Πx: A. B]]g = Π([[Γ ⊢ A]]g, Λa. [[Γ, x: A ⊢ B]]⟨g, a⟩)
[[Γ ⊢ {M}_{A}]]g = [ [[M]]g^{Γ} ]_{[[Γ ⊢ A]]g}

Notice that ⊢ is just used as a place-holder here, it does not signify a judgement derivation. The symbol Λ stands for lambda-abstraction at the meta-level, and g^{Γ}: Var ⇀ D is the environment defined by projections on g:

g^{⟨⟩}(y) undefined, for all y.
g^{Γ, x:A}(y) = \{ \begin{matrix}π_{2}(g), & if y ≡ x, \\ (π_{1}(g))^{Γ}(y) & if y ≢ x. \end{matrix}

The following theorem establishes the main soundness property of the model construction. It also shows well-definedness of the interpretation of contexts [[Γ]] and of types [[Γ ⊢ A]], whenever Γ is a context and Γ ⊢ A. The parts of the theorem need to be proven simultaneously because of type dependency.

Theorem 5.4 (Well-Definedness and Soundness) 1. If Γ Context then [[Γ]] is a PER.

2. If Γ ⊢ A then [[Γ ⊢ A]]g_{1} = [[Γ ⊢ A]]g_{2} whenever g_{1} [[Γ]] g_{2}.

3. If Γ ⊢ M : A then [[M]]g_{1}^{Γ} ([[Γ ⊢ A]]g_{1}) [[M]]g_{2}^{Γ} whenever g_{1} [[Γ]] g_{2}.

4. If Γ ⊢ A ≤ B then [[Γ ⊢ A]]g ⊆ [[Γ ⊢ B]]g for all g ∈ [[Γ]]. Proof. Simultaneously by induction on derivations, making use of axioms of the lambdamodel and the definitions of the PER constructions. ⊓ ⊔

Notice that a special case of part 3 is the soundness property that Γ ⊢ M : A implies [[M]]g^{Γ} ∈ [[Γ ⊢ A]]g for any g ∈ [[Γ]]. The existence of PER models (generated from λmodels and some PERs to interpret atomic types), together with this soundness result, guarantee the consistency of the calculus.

6 Related and Further Work

We have presented the type system λ_{≤{}}, which adds singleton types and Π-types to the simply-typed lambda-calculus with subtypes, λ_{≤}. This gives a system with types that depend on terms. Singleton types {M}_{A} can be interpreted in a PER model as the equivalence class of [[M]] in the PER [[A]].

The judgements of λ_{≤{}} are defined simultaneously and typing embeds in subtyping in a simple way. Noticing this, we can give alternative shorter presentations of the system which “wrap-up” judgements in terms of each other; this can be useful because it simplifies tedious simultaneous inductions. One way is to encode typing in terms of subtyping, defining Γ ⊢ M : A iff Γ ⊢ {M}_{A} ≤ B holds for some B. Another is to encode subtyping in terms of typing, defining Γ ⊢ A ≤ B iff Γ, x: A ⊢ x : B; we get the usual subtyping rules if a rule of η-reduction is added.

Decidability of type-checking has not yet been investigated, but we conjecture that it holds. A typical approach would be to first study the reduction behaviour of terms and types, for both β-reduction and Γ-reduction. We would hope to find a normalization result and a set of syntax-directed rules for the system, with points where normalization occurs. The final step would be to give a termination argument for the deterministic rules, to show that they define a complete algorithm.

Research into type systems for object-oriented programming (e.g., [Car88b, BL90, CG92]) gave inspiration for this work. Most systems in the literature do not treat type dependency at the same time as subtyping (Cardelli’s is an exception). Hayashi’s extensions of System F [Hay94] have singleton types with the same form as those described here. His calculi have union and intersection types, so dependent products become a derived notion. Hayashi’s treatment of singletons differs; his is based on encoding a propositional equality (which reflects his intention to create a constructive logic), rather than a definitional one. He has to add a rule of subject reduction as primitive, since there is a counterexample to its admissibility involving union types.

We hope that some of the development here will carry over to systems with application at the level of types, but the situation with full dependent types is more difficult than the simple case where each term in a type is warmly insulated with singleton braces. The harder case is the topic of some joint work in progress between the author and Adriana Compagnoni.

Acknowledgements. I am grateful to Benjamin Pierce, Don Sannella, and Andrzej Tarlecki for their wisdom, help, and encouragement during the progress of this work. Useful comments and corrections were provided by the CSL referees. I was supported by a UK EPSRC postgraduate studentship.

References

[Asp95] David R. Aspinall. Algebraic specification in a type-theoretic setting. Forthcoming PhD thesis, Department of Computer Science, University of Edinburgh, 1995.

[BL90] Kim B. Bruce and Giuseppe Longo. A modest model of records, inheritance and bounded quantification. Information and Computation, 87:196–240, 1990.

[BTCGS91] Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172–221, 1991.

[Car88a] Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988.

[Car88b] Luca Cardelli. Structural subtyping and the notion of power type. In Fifteenth Annual ACM Symposium on Principles of Programming Languages, 1988.

[CG92] Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[CL91] Luca Cardelli and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417–458, 1991.

[Hay94] Susumu Hayashi. Singleton, union and intersection types for program extraction. Information and Computation, 109, 1994.

[HL80] R. Hindley and G. Longo. Lambda calculus models and extensionality. Z. Math. Logik Grundlag. Math., 26:289–310, 1980.

[HP91] Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89:107–136, 1991.

[KST94] Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. The definition of Extended ML. Technical Report ECS-LFCS-94-300, LFCS, Department of Computer Science, University of Edinburgh, 1994.

[SP94] Paula Severi and Erik Poll. Pure Type Systems with Definitions. In Logical Foundations of Computer Science, LFCS’94, Lecture Notes in Computer Science 813, pages 316–328. Springer-Verlag, 1994.

[SST92] Donald T. Sannella, Stefan Sokołowski, and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: Parameterisation revisited. Acta Informatica, 29:689–736, 1992.

[SW83] Donald Sannella and Martin Wirsing. A kernel language for algebraic specification and implementation. In Proceedings of International Conference on Foundations of Computation Theory, Borgholm, Sweden, Lecture Notes in Computer Science 158. Springer-Verlag, 1983.