Singleton, Union and Intersection Types for Program Extraction

Susumu Hayashi ^{∗}

Department of Applied Mathematics and Informatics Ryukoku University Seta, Ohtsu, Shiga, Japan

            hayashi@whale.ryukoku.ac.jp

In memory of my mother, Yoshie Hayashi

Abstract

Two type theories, ATT and ATTT, are introduced. ATT is an impredicative type theory closely related to the polymorphic type theory of implicit typing of MacQueen et al. [MPS86]. ATTT is another version of ATT that extends the Girard-Reynolds second order lambda calculus. ATT has notions of intersection, union and singleton types. ATTT has a notion of refinement types as in the type system for ML by Freeman and Pfenning [FP91], plus intersection and union of refinement types and singleton refinement types. We will show how singleton, union and intersection types serve for development of programs without unnecessary codes via a variant of the Curry-Howard isomorphism. More exactly, they give a way to write types as specifications of programs without unnecessary codes which is inevitable in the usual Curry-Howard isomorphism.

1 Introduction

We introduce two constructive type theories: ATT (A Type Theory) and ATTT (ATT Typed more). ATT is an impredicative type theory closely related to the polymorphic type theory of implicit typing in [MPS86]. It is designed to develop programs without unnecessary codes via the Curry-Howard isomorphism. Constructive type theories are known as a basis for program development via constructive logic. But, when they were applied to the practice of formal program development of programs, they proved inadequate in practice. One defect of type theories is that developed programs must often include unnecessary codes for computation (see [HN88, Hay90]). This comes from the identification of proofs and programs. Our main aim here is to remedy this defect by introducing singleton, union and intersection types. Union and intersection types hide entities from the scene and singleton type exposes them. By these, we can exclude purely logical parts of proofs from extracted programs.

∗Partly supported by Grant No. 02249209 of the Japanese Ministry of Education.

We will introduce another type theory ATTT (A triple tee) as well. ATTT is a system based on the idea of “refinement” of types. ATTT is a conservative extension of the Girard-Reynolds second order lambda calculus, which we will refer as λ2. Thus it can be used to develop typed programs in λ2.

As a framework for program extraction, ATTT apparently has many superior points to ATT. But we dare present ATT as well. ATT and ATTT can be regarded representations of the same idea by two different typing disciplines, implicit typing and explicit typing, respectively. Furthermore, almost all literatures on union and intersection types use type systems similar to ATT rather than ATTT. ATT would be useful to compare them and ours. Last not but least, ATT is simpler to understand and present. It will help readers to understand ATTT.

The aim of this paper is to introduce ATT and ATTT and establish their fundamental mathematical properties. Applications of ATT and ATTT for the practice of program extraction will appear elsewhere.

2 A type theory ATT

Before giving a formal syntax of ATT, we will give an intuitive explanation of the syntax and the intended semantics. ATT has objects, types and kinds. These three syntactic categories are roughly defined by the following grammar:

K ::= Type.
A ::= x | c | A → A | A ∧ A | A ∨ A |
⋀ x ∈ K.A | ⋁ x ∈ K.A |
⋀ x ∈ A.A | ⋁ x ∈ A.A |
{M}_{A}.
M ::= x | c | λx.M | MM.

We will use another constant, Kind, which does not appear in this grammar. In the grammar above, M, A and K denote objects, types and kinds, respectively. As it is a second order system, ATT has only one kind Type. So the kind level is inessential for ATT, but we include it for coherence with GTS-style presentations of type theories [Bar90], which will be used in this paper. (Although we follow GTS-presentation as far as possible, our notations and terminologies may sometimes diverge from the ones of GTS.)

The intended semantics of ATT assumes a fixed domain D of untyped partial λcalculus. Objects are elements of the domain. Normally, types in programming languages are interpreted as sets with common structure. Types of ATT, however, are interpreted as arbitrary subsets of D. In particular, the empty set is a type, as ATT is designed to achieve a kind of Curry-Howard isomorphism. The kind Type is the set of all subsets of D. The constant Kind is the singleton set of Type.

Now we give a rigorous formulation of ATT. Although ATT is a second order system, we have to formulate it as higher order systems like CoC [CH88], since the formation of singleton types depends on the typing of objects. A singleton type {A}_{B} is well formed only when B is a type of A.

Firstly, we define preterms (called pseudo terms in [Bar90]). Preterms are defined by the following grammar:

T ::= x | c | λx.T | T T | T → T | T ∧ T | T ∨ T | ⋀ x ∈ T.T | ⋁ x ∈ T.T | {T }_{T} .

Here, c and x stand for constants and variables, respectively. For program development, we have to extend this grammar by adding some basic types such as the type of natural numbers. To this end, we keep the definition of constants open. But we assume that at least Type and Kind are constants. These two constants are called sorts. In the following, s stands for a sort.

The symbols λ, ⋀, ⋁ are “quantifiers.” The notion of bound occurrences and free occurrences are defined as usual. The set of free variables of a preterm T will be written FV (T). The operation of α-conversion is defined as usual and we will identify two α-convertible preterms. Substitution of preterms is defined as usual. When a preterm B is substituted for a variable x in a preterm A, we denote the resulting preterm by A[x:= B].

The reduction and conversion of preterms are defined as usual by β-reduction. When B is obtained from A by successive β-reductions, we will write A → →_{β} B. When A and B are convertible, we will write A =_{β} B.

A judgment of ATT is of the form A ∈ B, where A and B are preterms. A context is a sequence of judgements of the form x ∈ A, where x is a variable. We will denote a context by Γ. When a variable x is not declared in a context Γ, then we say x is Γ-fresh. A sequent (hypothetical judgement) of ATT is the form Γ ⊢ J, where J is a judgment. Let Γ be x_{1} ∈ A_{1}, …, x_{n} ∈ A_{n}. Then Γ[x:= B] is x_{1} ∈ A_{1}[x:= B], …, x_{n} ∈ A_{n}[x:= B]. Similarly, if J is the judgment A ∈ B, then J[x:= C] is A[x:= C] ∈ B[x:= C].

A legal sequent of ATT is a sequent derivable by the following axiom and inference rules:

Axiom  Start rule  Weakening rule
⟨ ⟩ ⊢ Type ∈ Kind  {Γ ⊢ A ∈ s \atop Γ, x ∈ A ⊢ x ∈ A}  \begin{matrix}Γ ⊢ A ∈ B & Γ ⊢ C ∈ s \\ Γ, x ∈ C ⊢ A ∈ B \end{matrix}
where x is Γ-fresh.  where x is Γ-fresh.

Conversion rule  Subject reduction
\begin{aligned}Γ ⊢ A ∈ B & Γ ⊢ B′ ∈ s & B =_{β} B′ \\ & Γ ⊢ A ∈ B′ \end{aligned}  \begin{matrix}Γ ⊢ A ∈ B & A → →_{β} A′ \\ Γ ⊢ A′ ∈ B \end{matrix}

Rules for function space

→-formation  →-elimination
Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type
Γ ⊢ (A → B) ∈ Type

\begin{matrix}Γ ⊢ F ∈ (A → B) & Γ ⊢ C ∈ A \\ Γ ⊢ (F C) ∈ B \end{matrix}

→-introduction

Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type Γ, x ∈ A ⊢ C ∈ B
Γ ⊢ (λx.C) ∈ (A → B)

Rules for union ∨-formation

Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type
Γ ⊢ A ∨ B ∈ Type

∨-introduction

Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type Γ ⊢ C ∈ A
Γ ⊢ C ∈ A ∨ B
Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type Γ ⊢ C ∈ B
Γ ⊢ C ∈ A ∨ B

∨-elimination

\begin{matrix}Γ ⊢ C ∈ A ∨ B & Γ, x ∈ A ⊢ D ∈ E & Γ, x ∈ B ⊢ D ∈ E \\ Γ ⊢ D[x:= C] ∈ E[x:= C] \end{matrix}

where E is not a sort. ⋁-formation

Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ Type
Γ ⊢ (⋁ x ∈ A.B) ∈ Type

⋁-introduction

Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ Type Γ ⊢ D ∈ A Γ ⊢ C ∈ B[x:= D]
Γ ⊢ C ∈ (⋁ x ∈ A.B)

⋁-elimination

\begin{matrix}Γ ⊢ C ∈ (⋁ x ∈ A.B) & Γ, x ∈ A, y ∈ B ⊢ D ∈ E \\ Γ ⊢ D[y:= C] ∈ E[y:= C] \end{matrix}

where x is not in F V (D) ∪ F V (E) and E is not a sort. Rules for intersection

∧-formation  ∧-elimination
Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type

Γ ⊢ A ∧ B ∈ Type {Γ ⊢ C ∈ A ∧ B \atop Γ ⊢ C ∈ A}  {Γ ⊢ C ∈ A ∧ B \atop Γ ⊢ C ∈ B}

∧-introduction

Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type Γ ⊢ C ∈ A Γ ⊢ C ∈ B
Γ ⊢ C ∈ A ∧ B
⋀-formation  ⋀-elimination
Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ Type
Γ ⊢ (⋀ x ∈ A.B) ∈ Type

\begin{matrix}Γ ⊢ C ∈ (⋀ x ∈ A.B) & Γ ⊢ D ∈ A \\ Γ ⊢ C ∈ B[x:= D] \end{matrix}

⋀-introduction

Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ Type Γ, x ∈ A ⊢ C ∈ B
Γ ⊢ C ∈ (⋀ x ∈ A.B)

where x is not in F V (C). Rules for singleton

singleton-formation  singleton-introduction
Γ ⊢ B ∈ Type Γ ⊢ A ∈ B
Γ ⊢ {A}_{B} ∈ Type

\begin{matrix}Γ ⊢ B ∈ Type & Γ ⊢ A ∈ B \\ Γ ⊢ A ∈ \{A\}_{B} \end{matrix}

singleton-elimination

\begin{aligned}Γ ⊢ P_{1} ∈ \{A\}_{C} ∧ \{B\}_{C} & Γ ⊢ P_{2} ∈ D[x:= A] & Γ, x ∈ C ⊢ D ∈ T ype \\ & Γ ⊢ P_{2} ∈ D[x:= B] \end{aligned}

{Γ ⊢ A ∈ \{B\}_{C} \atop Γ ⊢ A ∈ C}

2.1 Some comments on the formal system of ATT

In this section, we will give some discussions on the formal system presented above.

2.1.1 The rule of subject reduction

ATT has the rule of subject reduction as a basic rule. The rule is an admissible rule for many type theories like CoC. Readers may think that the rule is unnecessary. But we have not succeeded to prove the rule for ATT without the rule. Furthermore, Pierce and Freeman [Pie91a] have observed an example which would be an counterexample for the rule in a type system closely related to ATT. Let’s briefly sketch their example. Let a, b and c be types. Then λx.y.z.x((λt.t)yz)((λt.t)yz) has the type

((a → a → d) ∧ (b → b → d)) → (c → a ∨ b) → c → d.

Trying to type these, we first deduce (λt.t)yz ∈ a ∨ b under the obvious context for x, y and z. On the other hand, xuu ∈ d is derivable under the same context plus u ∈ a or u ∈ b. By applying ∨-elmination to these, (λt.t)yz substitutes u and we have the typing of the term. But, reduced forms λx.y.z.x(yz)((λt.t)yz) or λx.y.z.x((λt.t)yz)(yz) would not have the type, as there would not be such a term as xuu for these terms. Note that the fully reduced form λx.y.z.x(yz)(yz) has the type, again.

It has not been known if this is a real counterexample for Pierce’s system, but it is very likely so. We conjecture that this is a counterexample also for ATT. In this paper, we do not need the rule of subject reduction at all. All results in this paper remain true for the system without the rule of subject reduction. But it would be useful for optimization and transformation of programs. So we added it as a basic rule.

2.1.2 The rules of singleton-elimination

We do not know if the first rule of singleton-elimination is the only right formulation. But this is the best formulation we know. Later, we will define a propositional equality by means of singleton and intersection types. Then this rule will turn into the equality rule used by Turner in his type theory NTT [Tur89]. Furthermore, we have been able to derive almost all properties which we need. Another possible rule of the singletonelimination is

Strong rule of (first) singleton-elimination

\begin{matrix}Γ ⊢ P_{1} ∈ \{A\}_{C} ∧ \{B\}_{C} & Γ ⊢ P_{2} ∈ D[x:= A] & Γ, x ∈ C ⊢ D ∈ T ype \\ Γ ⊢ P_{2}[x:= B] ∈ D[x:= B] \end{matrix}

This substitutes B for x in P_{2} as well as x in D. This rule is sound w.r.t. the semantics of ATT given later. But, this rule is not sound w.r.t. the transformation from ATT to ibMPS. (see 2.5). Thus this would not be a correct rule from type theoretic point of view.

2.1.3 Distributive laws

The rules for intersection and union are not strong enough to derive the distributive laws for them. The following judgments are not derivable by the rules for intersection and union:

a ∈ Type, b ∈ Type, c ∈ Type, x ∈ a ∧ (b ∨ c) ⊢ x ∈ (a ∧ b) ∨ (a ∧ c)
a ∈ Type, b ∈ Type, c ∈ Type, x ∈ (a ∨ b) ∧ (a ∨ c) ⊢ x ∈ a ∨ (b ∧ c)

Note that the converses are derivable. Furthermore, the latter judgment can be derived from the former judgment. (This was pointed by Barbanera and Dezani-Ciancaglini.) Some formal systems for intersection and union types include the laws above as axioms, e.g. [BDC91],[Pie90],[Pie91b]. (These papers mentioned consider also distributive laws for union and intersection with arrow. Their unprovability seems a problem with η-rule rather than rules for union and intersection. So we do not consider them in this paper.) We may include these as basic rules in ATT, as the metamathematical properties of ATT in this paper remain true. But, these laws do not seem necessary for our aim. Hence we do not include them in ATT. Later, we will show these distributive laws are derivable in ATTT (see 3.5).

2.1.4 Type formation

The inference rules above are designed so that types are formed only through formation rules. The side condition “E is not a sort” for ∨-elimination and ⋁-elimination prevents these rules forming new types unexpectedly. Dropping this side condition, E of ∨- elimination could be Type and then D[x:= C] ∈ Type would be derivable. Namely, a type D[x:= C] would be formed by ∨-elimination rule. The side condition was meant to avoid this. Note that the side condition is decidable.

However, the side condition may be superfluous. Types formed by these eliminations rules without the side condition might be formed by the formation rules. But, we do not know if this is alway true. At least, without the side condition, we do not know how to prove the results on classification of terms in 2.3. This is the reason why we included such a side condition. Even if the side conditon is superfluous, it would be better to keep the side condition to make track of formation of types clear.

2.2 Basic notions and lemmas

We will define some basic notions and prove some basic lemmas which are necessary to understand the structure of ATT.

Definition 1 If a sequent is derivable by the inference rules above, then it is called a legal sequent. If Γ ⊢ A ∈ B is a legal sequent, then Γ is called legal context, A ∈ B is legal judgment, and A and B are (legal) terms. To emphasize the context Γ, we will often say “a preterm A is a term under the context Γ.”

In the following, we list basic lemmas. They all can be easily proved by standard methods. So we will omit the proofs.

Lemma 1 (Church-Rosser property of preterms) If two preterms are β-convertible, then they can be reduced to a common preterm.

Lemma 2 If x_{1} ∈ A_{1}, …, x_{n} ∈ A_{n} ⊢ J is a legal sequent, then (i) if i ≠ j, then x_{i} ≠ x_{j}, (ii) the free variables of the term A_{i} are a subset of {x_{1}, …, x_{i−1}}, and (iii) the free variables of the judgment J are a subset of {x_{1}, …, x_{n}}.

Lemma 3 Assume that x_{1} ∈ A_{1}, …, x_{n} ∈ A_{n} ⊢ B ∈ C is a legal sequent. Then B is not the sort Kind. Furthermore, for each i, A_{i} is not the sort Kind and one of the followings holds:

1. A_{i} is the sort Type and x_{1} ∈ A_{1}, …, x_{i−1} ∈ A_{i−1} ⊢ A_{i} ∈ Kind is derivable.

2. x_{1} ∈ A_{1}, …, x_{i−1} ∈ A_{i−1} ⊢ A_{i} ∈ Type is derivable.

Lemma 4 (substitution) If Γ_{1}, x ∈ A, Γ_{2} ⊢ J and Γ_{1} ⊢ C ∈ A are legal sequents, then so is Γ_{1}, Γ_{2}[x:= C] ⊢ J[x:= C].

Lemma 5 (generalized weakening) When a context Γ is obtained from another context Γ′ by dropping some judgments in Γ′, then we say that Γ′ contains Γ. If Γ ⊢ J is a legal sequent and Γ′ is a legal context which contains Γ, then Γ′ ⊢ J is a legal sequent.

The first part of the following lemma is a special case of lemma 4 above and the second part is easily proved by induction on derivations. The second part was called “context replacement” by Luo [Luo90].

Lemma 6 (replacement) (i) If Γ ⊢ A ∈ B and Γ, x ∈ B ⊢ x ∈ B′ are derivable, then Γ ⊢ A ∈ B′ is derivable. (ii) If Γ, x ∈ A, Γ′ ⊢ J and Γ, x ∈ A′ ⊢ x ∈ A are derivable, then Γ, x ∈ A′, Γ′ ⊢ J is derivable.

2.3 Classification of terms

Every term of ATT (except the sort Kind) is classified into one of object, type and kind. This classification can be done by purely syntactical observation. Firstly, we define object, type and kind by their shapes. Then we prove that this classification is sound, e.g., if a term A is a type, then A ∈ Type is derivable.

Assume a preterm A is legal under context Γ. By lemma 2, all free variables of A are declared in Γ. Let x be a free variable of A. If it is declared by x ∈ Type, then we call it a type variable of Γ. Otherwise, we call it an object variable of Γ. So all free variables of any legal term under Γ are classified into type variables and object variables. We extend this classification to legal terms.

Definition 2 (classification under a variable classification) Assume that FV (A) is a union of two disjoint sets Obj and Typ. The variables of Obj are called object variables, and the variables of Typ are called type variables. Then objects, types and kinds under the classification of free variables ⟨Obj , Typ⟩ are defined as follows:

objects 1. An object variable is an object.

2. If A and B are objects, then so is (AB).

3. If A is an object under the classification ⟨Obj ∪ {x}, Typ⟩, then λx.A is an object under the classification ⟨Obj , Typ⟩.

types 1. A type variable is a type.

2. If A and B are types, then so are A → B, A ∨ B and A ∧ B.

3. If A is an object and B is a type, then {A}_{B} is a type.

4. If A is a type and B is a type under the classification ⟨Obj ∪{x}, Typ⟩, then ⋀ x ∈ A.B and ⋁ x ∈ A.B are types under the classification ⟨Obj , Typ⟩.

5. If A is a type under the classification ⟨Obj , Typ ∪ {x}⟩, then ⋀ x ∈ Type.A and ⋁ x ∈ Type.A are types under the classification ⟨Obj , Typ⟩.

kinds The constant Type is a kind.

Now we classify legal terms under a context using the classification above.

Definition 3 (classification under a context) Assume a preterm A is legal under context Γ. Let Obj be the set of object variables of Γ, and let Typ be the set of type variables of Γ. If A is an object under the classification ⟨Obj , Typ⟩, then A is an object under Γ. Types and kinds under Γ are defined in the same way.

Lemma 7 1. If x_{1} ∈ A_{1}, …, x_{n} ∈ A_{n} is a legal context, then either A_{i} is a type under the context x_{1} ∈ A_{1}, …, x_{i−1} ∈ A_{i−1} or A_{i} is a kind, i.e., A_{i} ≡ Type.

2. If Γ ⊢ A ∈ B is a legal sequent, then exactly one of the following holds:

(a) A is an object and B is a type under Γ.

(b) A is a type and B is a kind, i.e. B ≡ Type.

(c) A is a kind, i.e. A ≡ Type, and B is the sort Kind.

This lemma can be proved induction on derivations and shows that classification corresponds to our intutive notions of terms, types and kinds. Note that the uniqueness of the classification is trivial, as the sets of objects, types, kinds, and the sort Kind are syntactically disjoint.

The sort Type is an element of Kind by the axiom. It is coherent with the classification above. We shall check that a type as defined above is an element of the sort Type, as Type is intended to be the collection of types. Namely, we shall prove the following lemma.

Lemma 8 If Γ ⊢ A ∈ B is derivable and B is a type, then Γ ⊢ B ∈ Type is derivable.

This lemma is proved by induction on derivations using the following type inversion lemma, which is proved by induction on derivations using lemmas 1, 6 and 7.

Lemma 9 1. Let op be one of →, ∨, ∧. If Γ ⊢ (A op B) ∈ Type is derivable, then so are Γ ⊢ A ∈ Type and Γ ⊢ B ∈ Type.

2. Let OP be one of ⋁, ⋀. If Γ ⊢ (OP x ∈ A.B) ∈ Type is derivable, then so are Γ ⊢ A ∈ Type and Γ, x ∈ A ⊢ B ∈ Type.

3. If Γ ⊢ {A}_{B} ∈ Type is derivable, then so are Γ ⊢ B ∈ Type and Γ ⊢ A ∈ B.

Note that if a term is proved to be an element of Type, then it is one of the forms of the lemma above or a type variable. Hence, by lemma 9, any element of Type is formed by successive applications of the formation rules.

2.4 Semantics of ATT

A semantics of ATT can be given on any reasonable concrete model of partial untyped lambda calculus. Unfortunately, we cannot find any good reference for this kind of models of partial untyped lambda calculus. (A good reference for the typed case is [Mog88].) One possible approach is to start with models of ordinary (total) untyped lambda calculus. But this construction will invalidate an important proposition that if a term is typable then it denotes a meaningful value. So we will give a semantics using a particular domain theoretic model of the partial untyped lambda calculus by Plotkin [Plo85]. Plotkin reconstructed D_{∞} in the category of cpo’s and continuous partial functions. In his sense, a cpo may or may not have bottom element. His D_{∞} is a cpo with two total continuous functions i and j

D_{∞} i_{→} ; j^{←} [D_{∞} ⇀ D_{∞}] satisfying i ∘ j = id

Note that [D_{∞} ⇀ D_{∞}] is the set of partial continuous functions from D_{∞} to D_{∞}. We can interpret lambda terms as in the usual D_{∞}. Note that [[(AB)]]_{ρ} can be undefined, as i([[A]]_{ρ}) is a partial function. So an interpretation of a term may be undefined. Using Plotkin’s semantics, a semantics of ATT is given as follows.

Definition 4 (interpretation) Let TYPE be the set of subsets of D_{∞} and KIND be the singleton {TYPE}. Let ⟨Obj , Typ⟩ be a partition of the variables into object variables and type variables. A function ρ from the set of variables to D_{∞} ∪ TYPE ∪ KIND is called an assignment, if ρ(x) is in D_{∞} for an object variable x and ρ(x) is in TYPE for a type variable x. For simplicity, we assume that the only constants of ATT are Type and Kind. Let M be an object, a type, or a kind under ⟨Obj , Typ⟩. We define interpretation [[M]]_{ρ} of M. objects An object is a lambda term. The interpretation of objects is the same as the

usual interpretation of lambda terms.

types 1. If x is a type variable, then set [[x]]_{ρ} = ρ(x).

2. [[A → B]]_{ρ} = {f ∈ D_{∞}|∀x ∈ [[A]]_{ρ}.((i(f))(x) ∈ [[B]]_{ρ})}.
3. [[A ∨ B]]_{ρ} = [[A]]_{ρ} ∪ [[B]]_{ρ}.
4. [[A ∧ B]]_{ρ} = [[A]]_{ρ} ∩ [[B]]_{ρ}.
5. [[{A}_{B}]]_{ρ} = {x ∈ D_{∞}|x = [[A]]_{ρ} and [[A]]_{ρ} ∈ [[B]]_{ρ}}.
6. [[⋀ x ∈ A.B]]_{ρ} = ⋂_{v∈[[A]]_{ρ}}([[B]]_{ρ[x:= v]}).
7. [[⋁ x ∈ A.B]]_{ρ} = ⋃_{v∈[[A]]_{ρ}}([[B]]_{ρ[x:= v]}).

sorts [[Type]]_{ρ} = TYPE and [[Kind]]_{ρ} = KIND.

The soundness theorem is proved by induction on derivations.

Theorem 1 (soundness) Assume that Γ ⊢ A ∈ B is derivable. Let ρ be an environment with respect to the partition of variables induced by the context Γ. Then [[A]]_{ρ} and [[B]]_{ρ} are defined and [[A]]_{ρ} is an element of [[B]]_{ρ}. Hence the interpretation of any legal term is defined. Furthermore, this theorem holds for the system with the strong rule of singleton-elimination.

Although we gave a semantics in the category of sets, it would be possible to give a semantics in other categories with some conditions. Rosolini [Ros86] and others have introduced notions of partial categories which is intended for categories of partial maps. Following D. Scott’s semantics of lambda calculus in cartesian closed categories, we would be able to give a semantics of partial lambda calculus in partial cartesian closed categories. Then the partial CCC would be embeddable into a topos. In the topos, we would be able to give semantics of ATT, as we can define singleton, union and intersection by the constructive logic of the topos. This would be straightforward but is yet to be worked out.

Pierce [Pie90] has given a PER-semantics for a type system closely related to ATT. Pierce did not consider singleton type, but it would be interpreted by

x [[{A}_{B}]]_{ρ} y = x [[B]]_{ρ} y and x [[B]]_{ρ} [[A]]_{ρ}.

This semantics works for ATT as well. Then the rule of extensionality of functions can be added to the system as in Martin-Löf’s type theory of [Mar82]. But Pierce has pointed out an anomaly of this semantics: As the union of PER’s is not in general a PER, we have to collapse it by taking the transitive closure to interpret union types. This causes some expected equalities between types to fail. See [Pie90] for details.

2.5 Eliminating the non-computational part

In this section, we will show that the non-computational part of the proof is eliminable by a simple translation. This translation translates derivations in ATT into another type theory, ibMPS, which is a variant of the type theory of MacQueen et al. [MPS86]. As a corollary of the soundness of the translation, we obtain a strong normalization theorem for ATT.

The system ibMPS (inhabitable basic MacQueen, Plotkin and Sethi system) is roughly defined as follows:

ibMPS = ATT − singleton types

− first order big union and intersection types − conversion rule

The first order big union and intersection types mean types of the form ⋀ x ∈ A.B or ⋁ x ∈ A.B, where A is a type.

As we dropped the singleton types, types of ibMPS can be defined independently from the definition of legal terms as in the usual second order type theories. It is more natural to reformulate ibMPS in this way, but we do not do so here to avoid repetitions and to save space. We only list changes of ibMPS from ATT. Note that some rules for intersections and unions are changed. These changes come from the other changes.

Definition 5 (ibMPS) The system ibMPS is defined by changing ATT as follows:

1. Drop {T }_{T} from the syntax of the preterms, and drop all the rules for singleton types.

2. Change all the rules for ⋀ and ⋁, and ∨-elimination rule as follows:

Γ, x ∈ Type ⊢ B ∈ Type Γ ⊢ (⋀ x ∈ Type.B) ∈ Type

Γ, x ∈ Type ⊢ B ∈ Type
Γ ⊢ (⋁ x ∈ Type.B) ∈ Type
Γ, x ∈ Type ⊢ B ∈ Type Γ, x ∈ Type ⊢ C ∈ B
Γ ⊢ C ∈ (⋀ x ∈ Type.B)
Γ ⊢ C ∈ (⋀ x ∈ Type.B) Γ ⊢ D ∈ Type
Γ ⊢ C ∈ B[x:= D]
Γ, x ∈ Type ⊢ B ∈ Type Γ ⊢ D ∈ Type Γ ⊢ C ∈ B[x:= D]
Γ ⊢ C ∈ (⋁ x ∈ Type.B)
Γ ⊢ C ∈ (⋁ x ∈ Type.B) Γ, x ∈ Type, y ∈ B ⊢ D ∈ E
Γ ⊢ D[y:= C] ∈ E

\begin{aligned}Γ ⊢ C ∈ A ∨ B & Γ, x ∈ A ⊢ D ∈ E & Γ, x ∈ B ⊢ D ∈ E \\ & Γ ⊢ D[x:= C] ∈ E \end{aligned}

In the last two rules, E is not Type or Kind.

3. Drop the conversion rule.

It is easy to prove the following lemma by induction of derivations.

Lemma 10 (inhabitation rule) The following is an admissible rule of ibMPS.

{Γ, x ∈ A, Γ′ ⊢ B ∈ C \atop Γ, Γ′ ⊢ B ∈ C},

where x is not a free variable of B, and A is not Type. (Note that the “first order” variable x never appear in C. So we do not need variable condition on C.)

The inhabitation rules maintains that all types are inhabited (cf. [Mit90]). Note that ATT is regarded as having an empty type; otherwise singleton-elimination is not sound. Existence of an empty type is a characteristic of type systems based on the Curry-Howard isomorphism. On the other hand, in many systems purely for types in programming languages, types can be assumed to be inhabited. In this sense, we are translating a type theory for the Curry-Howard isomorphism (verification system) into a type theory for a programming language (computation system).

Definition 6 (translation from ATT to ibMPS) We define a translation M ↦ M^{∗} from preterms of ATT to preterms of ibMPS as follows:

1. c^{∗} = c.

2. x^{∗} = x.

3. (λx.A)^{∗} = (λx.A^{∗}).

4. (AB)^{∗} = (A^{∗}B^{∗}).

5. (A op B)^{∗} = (A^{∗} op B^{∗}), where op is one of →, ∧, ∨.

6. (OP x ∈ Type.B)^{∗} = OP x ∈ Type.B^{∗}, where OP is one of ⋀, ⋁.

7. (OP x ∈ A.B)^{∗} = B^{∗}, where A is not Type and OP is one of ⋀, ⋁.

8. ({A}_{B})^{∗} = B^{∗}.

The translation is naturally expanded to translations of judgments, contexts and sequents. Then the translation preserves derivability.

Theorem 2 If Γ ⊢ J is derivable in ATT, then so is Γ^{∗} ⊢ J^{∗} in ibMPS.

Proof. By induction of derivations. Let us check only the cases of ⋀-introduction and singleton-elimination, as the other cases are proved similarly.

Let us consider the case of ⋀-introduction. Assume that the last rule of the derivation is as follows:

Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ Type Γ, x ∈ A ⊢ C ∈ B
Γ ⊢ C ∈ (⋀ x ∈ A.B)

If A is not Type, then the translation of the conclusion is Γ^{∗} ⊢ C^{∗} ∈ B^{∗}. By the induction hypothesis, the translation of the last premise, Γ^{∗}, x ∈ A^{∗} ⊢ C^{∗} ∈ B^{∗}, is derivable. By the inhabitation rule, Γ^{∗} ⊢ C^{∗} ∈ B^{∗} is derivable. If A is Type, then the translation of the rule is the ⋀-introduction rule of ibMPS.

Now consider the case of singleton-elimination. Assume that the last rule of the derivation is as follows:

\begin{aligned}Γ ⊢ P_{1} ∈ \{A\}_{C} ∧ \{B\}_{C} & Γ ⊢ P_{2} ∈ D[x:= A] & Γ, x ∈ C ⊢ D ∈ T ype \\ & Γ ⊢ P_{2} ∈ D[x:= B] \end{aligned}

Since {A}_{C} is a legal term, C is a type and so x is an object variable. Since the translation eliminates all subterms which are objects, we see (D[x:= A])^{∗} ≡ (D[x:= B])^{∗} ≡ D^{∗}. Hence the translation of the conclusion of the rule is the same as the translation of the second premise and so it is derivable from the induction hypothesis.

Note that the strong rule of first singleton-elimination is unsound w.r.t. the translation. Let Γ be the context X ∈ Type, Y ∈ Type, x ∈ X, y ∈ Y. Then Γ, w ∈ {x}_{(X∨Y)} ∧ {y}_{(X∨Y)} ⊢ x ∈ X is provable in ATT. The strong rule infers the sequent Γ, w ∈ {x}_{(X∨Y)} ∧ {y}_{(X∨Y)} ⊢ y ∈ X. Assume the translation works for the strong rule. Then Γ, w ∈ (X ∨ Y) ∧ (X ∨ Y) ⊢ y ∈ X. is provable in ibMPS. By substituting x for w, we get Γ ⊢ y ∈ X. But, this is not provable in ibMPS.

The terms of ibMPS are strongly normalizable. A proof for a related system can be found in [Lei86] and it is applicable to ibMPS. So we do not give a proof here.

Theorem 3 Every term of ibMPS is strongly normalizable.

We can prove strong normalization property of ATT from this theorem.

Corollary 1 Every term of ATT is strongly normalizable. Proof. Let M be a term of ATT. Then M^{∗} is strongly normalizing by the previous theorem and theorem 2. If M is an object, then M^{∗} is identical to M. So M is strongly normalizing. If M is a type, then its subterms, which are objects, are legal terms of ATT by lemma 9. Since reduction can happen only in such subterms, M is strongly normalizing.

The following is also obvious:

Corollary 2 ATT is a conservative extension of ibMPS. Namely, any provable sequent of ibMPS is provable in ATT, and any provable sequent of ATT having only preterms of ibMPS is provable in ibMPS.

2.6 Some definable types and judgments

In this section, we will define some derived notions including dependent products and sums at the level of types.

(1) Dependent product. ATT does not have a dependent product Π unlike Martin-Löf type theories. Such a dependent product of types is definable by means of intersection types and function spaces. Assume that A and B are types. Then we define

Πx ∈ A.B =^{def} ⋀ x ∈ A.({x}_{A} → B)

The formation and elimination rules for Π are easily derivable.

We will derive the introduction rule. Assume that the following three sequents are derived:

(1) Γ ⊢ A ∈ Type, (2) Γ, x ∈ A ⊢ B ∈ Type, (3) Γ, x ∈ A ⊢ C ∈ B.

Let y and z be fresh variables. By renaming the variable x of (3) to z and applying generalized weakening, we can derive

Γ, x ∈ A, y ∈ {x}_{A}, z ∈ A ⊢ C[x:= z] ∈ B[x:= z].

Since y ∈ A is derivable under Γ, x ∈ A, y ∈ {x}_{A}, we can derive

Γ, x ∈ A, y ∈ {x}_{A} ⊢ C[x:= y] ∈ B[x:= y]

by substitution. On the other hand, we can derive y ∈ {y}_{A} ∧ {x}_{A} under the same context. Then we can derive the Π-introduction rule roughly as follows:

\begin{matrix}Γ, x ∈ A, y ∈ \{x\}_{A} ⊢ y ∈ \{y\}_{A} ∧ \{x\}_{A} & Γ, x ∈ A, y ∈ \{x\}_{A} ⊢ C[x:= y] ∈ B[x:= y] \\ Γ, x ∈ A, y ∈ \{x\}_{A} ⊢ C[x:= y] ∈ B[x:= y][y:= x] \end{matrix} ; Γ, x ∈ A ⊢ λy.(C[x:= y]) ∈ (\{x\}_{A} → B) ; Γ ⊢ λx.C ∈ ⋀ x ∈ A.(\{x\}_{A} → B)

In the second inference, we omitted the first two premises of →-introduction, which are easily derived. Note that we identify the two α-convertible terms λy.C[x:= y] and λx.C in the last step of the inference.

(2) Cartesian product. Using ⋀ at the level of types, we can define the cartesian product of two types by the standard method for polymorphic lambda calculi.

A × B =^{def} ⋀ X ∈ Type.((A → B → X) → X)

Note that the arrows → above are basic constructors of ATT. Pairing ⟨A, B⟩ and projections, fst(A), snd(A), are defined in the standard way.

(3) Dependent sum. The dependent sum of types is definable by means of union types and cartesian products. Assume that A and B are types. Then we define

Σx ∈ A.B =^{def} ⋁ x ∈ A.({x}_{A} × B)

Note that this dependent sum is a strong sum [Coq86], as the first component of a member a of Σx ∈ A.B is obtained by fst(a) as well as the second component. Note that a preterm Σx ∈ Type.B can be defined as above, but cannot be a type, as such a strong sum implies a contradiction [Coq86]. To derive (Σx ∈ Type.B) ∈ Type, {x}_{Type} ∈ Type has to be derived. But, to derive it by the rule of singleton-formation, Type ∈ Type is required but it is not derivable. Note that the standard definition of dependent sum of types is also possible in ATT:

Σx ∈ A.B =^{def} ⋀ y ∈ T ype.((Πx ∈ A.(B → y)) → y)

Since ATT has a strong sum, this sum turns out to be a strong sum. (This was pointed out by Luo.)

(3) Subset Type. A subset type is definable as follows:

{x ∈ A|B} =^{def} ⋁ x ∈ A. ⋁ y ∈ B.{x}_{A}

Note that subset type is a kind of dependent sum Σx ∈ A.B which exposes information from A and hides information from B. The strong sum defined above exposes information from both A and B. The union type ⋁ x ∈ A.B hides information from A and exposes information from B.

(4) Propositional equality. Martin-Löf type has a basic type Eq(A, M, N) called propositional equality. In higher order type theories like CoC, Leibnitz equality can be defined as a type (proposition). But it cannot be in second order theories. Having singleton types, an equality type can be defined in ATT as follows:

Eq(A, M, N) =^{def} {M}_{A} ∧ {N}_{A}

It is inhabited iff M and N are the same object of the type A. This equality is an equivalence relation, i.e., the following rules hold:

\begin{matrix}M ∈ A & A ∈ Type \\ M ∈ Eq(A, M, M) \end{matrix} {C ∈ Eq(A, N, M) \atop C ∈ Eq(A, M, N)} \begin{matrix}C_{1} ∈ Eq(A, M, N) & C_{2} ∈ Eq(A, N, P) \\ C_{2} ∈ Eq(A, M, P) \end{matrix}

The rule of singleton-elimination serves as the equality rule. Note that our propositional equality is closer to Leibnitz equality than to Martin-Löf’s, as it is a defined notion and is “not” an extensional equality. (Exactly speaking, our equality is neutral with respect to extensionality. We may add extensionality rules consistently, although extensionality is problematic as noted in 2.4.)

(5) Equality judgment. Martin-Löf type theory has an equality judgment M = N ∈ A. A similar judgment can be defined by

M = N ∈ A =^{def} M ∈ {N}_{A}

Note that the following rules hold:

{C ∈ Eq(A, M, N) \atop M = N ∈ A} {M = N ∈ A \atop M ∈ Eq(A, M, N)} {M = N ∈ A \atop N ∈ Eq(A, M, N)}

The following proposition ensures that our definition of equality is reasonable.

Proposition 1 (equality reflection) Assume that M ∈ A and N ∈ A are derivable under the empty context. Then M = N ∈ A is derivable under the empty context iff M and N are β-convertible.

Proof. The “if” direction is proved by applying the conversion rule to M ∈ {M}_{A}. Let us prove the “only if” direction. Let T be the set of closed terms of untyped lambda calculus. β-convertibility is an equivalence relation on it. Let D be the set of β-conversion equivalence classes of T. Then D is a model of (total) untyped lambda calculus known as the closed term model. Interpreting Type as the powerset of D, an interpretation of ATT is obtained in the same way as the semantics in section 2.4. Note that the interpretation is identical, i.e., [[M]]_{ρ} is the term obtained from M by the substitution induced by the assignment ρ. Note that [[{A}_{B}]]_{ρ} is the singleton of [[A]]_{ρ}. If M = N ∈ A, i.e., M ∈ {N}_{A}, is derivable under the empty context, then the equivalence classes of M and N must be identical by soundness and the interpretation of singleton. Hence M and N are β-convertible.

Equality reflection was first proved by Luo for Leibnitz equality in his system ECC [Luo90] by a syntactical analysis of normalized terms. (Martin-Löf had considered the same problem for his inconsistent type theory [Mar71].) It seems difficult to prove it for ATT by syntactical analysis. The possibility and importance of equality reflection for ATT was pointed out by Luo.

Many other important notions can be defined in ATT, e.g., subtype judgment and a variant of the conditional formulas of PX. But we do not include them here. They will appear elsewhere together with some interpretations of logic into ATT and ATTT (variants of the Curry-Howard isomorphism).

2.7 Application to program extraction

In this section, we sketch how program extraction is achieved in ATT. By the types and judgments defined in the previous section, we can write specifications of programs as types of ATT just as in Nuprl and CoC. (In practice, these are not enough. We have to add some additional types such as recursive types and recursion operators for them. But this is another matter.) A typical specification with a subset type is Π x ∈ A.{y ∈ B|C} (see [NPS90]). By this type, we mean the set of functions f from A → B such that C[y:= f(x)] is inhabited. Unfolding the definition of Π and the subset type, we have the following type:

⋀ x ∈ A.({x}_{A} → ⋁ y ∈ B. ⋁ z ∈ C.{y}_{B}).

The translation of this type into ibMPS is A → B. Hence a function f of this type has the type A → B in ibMPS and so also in ATT. Furthermore, the condition on f is fulfilled.

Subset types are used to hide unnecessary information in specifications. If one does not need to have the information from C of Π x ∈ A. Σ y ∈ B.C, then one replaces the Σ with a subset type. But this hides all of the information from C. In ATT, finer hiding of information is possible. Suppose that we need the information y_{2} but not y_{1} in Π x ∈ A. Σ y_{1} ∈ B_{1}. Σ y_{2} ∈ B_{2}.C. If the Σ for y_{1} is changed to a subset type, then it hides y_{2} as well. When the Σ is replaced by ⋁, then the specification become what we expect. Note that we cannot always exchange y_{1} and y_{2}, as y_{1} may appear in B_{2}. But, we do not know any natural and concrete example for this. This is one of the most important open problems in our approach.

3 ATTT: ATT Typed more

ATT is a type system based on untyped lambda calculus. Although untyped lambda calculus serves well as a semantics of type systems, there are some more natural semantics, e.g., coherence semantics. In this section, we introduce another type theory called ATTT based on Girard-Reynolds’ λ2. (The formal system of ATTT in this paper is different from the system in [Hay91], as the present system has a stronger singleton-elimination.) As the coherence space gives a semantics of λ2, it also gives a semantics of ATTT.

The basic idea of ATTT is to keep types just as in λ2 and introduce the notion of refinement (or refinement type) of types for specifications of programs. A refinement of a type T is a subset of T. In some semantics, e.g., in coherence semantics, a type is always inhabited. A refinement is an arbitrary subset of a type, so it can be empty.

The refinement approach of ATTT is closely related to the notion of a modified realizability interpretation. Modified realizability determines a set of realizers and their functionality. Let’s consider the modified realizability of the formula ∀x ∈ A.∃y ∈ B.(f(x) =_{C} g(y)). A term a is a realizer of the formula iff a is a term of type A → B and ∀x ∈ A.(f(x) = g(a(x))) holds. In ATTT, the formula is interpreted by the following refinement of the type A → B:

⋀ x ∈ A.({x}_{A} → ⋁ y ∈ B. ⋁ p ∈ Eq(C, f(x), g(y)).{y}_{B}).

The type A → B gives the functionality of the realizers of the formula and the refinement above gives the set of realizers of the formula. This will become clearer when we give a translation of ATTT into λ2 below.

The idea of refinement types was first introduced by Freeman and Pfenning [FP91] in the context of ML. Our notion of refinement was influenced by their work, although the aim and presentation are different. Freeman and Pfenning write A : B :: C iff A is an element of the refinement type B and B is a refinement of C. We will not introduce new judgment A : B :: C but will introduce a new kind refine(A) for each type A. This denotes the set of the refinements of A. Hence, the equivalent of A : B :: C is the pair of judgments A ∈ B and B ∈ refine(C).

3.1 Formulation of ATTT

The preterms of ATTT are defined by the following grammar:

T ::= x | c | λx ∈ T.T | T T | refine(T) | T → T | T ∧ T | T ∨ T |
Π x ∈ T.T | ⋀ x ∈ T.T | ⋁ x ∈ T.T | {T }_{T} .

Note that refine is not a constant but is a syntactical operator. Sorts of ATTT are Kind, Type, RKind and preterms of the form of refine(A). In the following, s stands for a sort. Among the sorts, RKind and refine(A) are called refinement sorts and refine(A) is called a refinement kind. We will give inference rules of ATTT below:

The axiom, start rule, weakening rule and conversion rule are the same as in ATT, so we do not reproduce them here. The rule of subject reduction is an admissible rule for ATTT (see 3.5). Besides these general rules, ATTT has two rules for refinement.

refine-formation  refine-subtyping
Γ ⊢ M ∈ Type

Γ ⊢ refine(M) ∈ RKind

Γ ⊢ C ∈ A Γ ⊢ A ∈ refine(B)
Γ ⊢ C ∈ B

Rules for dependent product

Π-formation

Γ, x ∈ Type ⊢ A ∈ Type
Γ ⊢ (Π x ∈ Type.A) ∈ Type

Γ, x ∈ Type ⊢ R ∈ refine(A)
Γ ⊢ (Π x ∈ Type.R) ∈ refine(Π x ∈ Type.A)

Π-introduction

Γ, x ∈ Type ⊢ A ∈ Type Γ, x ∈ Type ⊢ B ∈ A
Γ ⊢ (λx ∈ Type.B) ∈ (Π x ∈ Type.A)
Γ, x ∈ Type ⊢ R ∈ refine(A) Γ, x ∈ Type ⊢ B ∈ R
Γ ⊢ (λx ∈ Type.B) ∈ (Π x ∈ Type.R)

Π-elimination

Γ ⊢ F ∈ (Π x ∈ Type.A) Γ ⊢ B ∈ Type
Γ ⊢ (F B) ∈ A[x:= B]

Rules for function space →-formation

Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type

Γ ⊢ A → B ∈ Type

Γ ⊢ C ∈ refine(A) Γ ⊢ D ∈ refine(B)
Γ ⊢ C → D ∈ refine(A → B)

→-introduction

Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type Γ, x ∈ A ⊢ C ∈ B
Γ ⊢ (λx ∈ A.C) ∈ A → B
Γ ⊢ C ∈ refine(A) Γ ⊢ D ∈ refine(B) Γ, x ∈ C ⊢ E ∈ D
Γ ⊢ (λx ∈ A.E) ∈ C → D

→-elimination

\begin{matrix}Γ ⊢ F ∈ A → B & Γ ⊢ C ∈ A \\ Γ ⊢ (F C) ∈ B \end{matrix}

Rules for union ∨-formation

Γ ⊢ A ∈ refine(C) Γ ⊢ B ∈ refine(C)
Γ ⊢ A ∨ B ∈ refine(C)

∨-introduction

Γ ⊢ A ∈ refine(C) Γ ⊢ B ∈ refine(C) Γ ⊢ D ∈ A
Γ ⊢ D ∈ A ∨ B
Γ ⊢ A ∈ refine(C) Γ ⊢ B ∈ refine(C) Γ ⊢ D ∈ B
Γ ⊢ D ∈ A ∨ B

∨-elimination

\begin{matrix}Γ ⊢ C ∈ A ∨ B & Γ, x ∈ A ⊢ D ∈ E & Γ, x ∈ B ⊢ D ∈ E \\ Γ ⊢ D[x:= C] ∈ E[x:= C] \end{matrix}

where E is not a sort. ⋁-formation

Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ refine(C)
Γ ⊢ (⋁ x ∈ A.B) ∈ refine(C)

where s is not Kind. ⋁-introduction

Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ refine(C) Γ ⊢ D ∈ A Γ ⊢ E ∈ B[x:= D]
Γ ⊢ E ∈ (⋁ x ∈ A.B)

where s is not Kind.

⋁-elimination

\begin{matrix}Γ ⊢ C ∈ (⋁ x ∈ A.B) & Γ, x ∈ A, y ∈ B ⊢ D ∈ E \\ Γ ⊢ D[y:= C] ∈ E[y:= C] \end{matrix}

where x is not in F V (D) ∪ F V (E) and E is not a sort.

Rules for intersection

∧-formation  ∧-elimination
Γ ⊢ A ∈ refine(C) Γ ⊢ B ∈ refine(C)

Γ ⊢ A ∧ B ∈ refine(C) {Γ ⊢ C ∈ A ∧ B \atop Γ ⊢ C ∈ A} {Γ ⊢ C ∈ A ∧ B \atop Γ ⊢ C ∈ B}

∧-introduction

Γ ⊢ A ∈ refine(C) Γ ⊢ B ∈ refine(C) Γ ⊢ D ∈ A Γ ⊢ D ∈ B
Γ ⊢ D ∈ A ∧ B
⋀-formation  ⋀-elimination
Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ refine(C)
Γ ⊢ (⋀ x ∈ A.B) ∈ refine(C)

\begin{matrix}Γ ⊢ C ∈ (⋀ x ∈ A.B) & Γ ⊢ D ∈ A \\ Γ ⊢ C ∈ B[x:= D] \end{matrix}

where s is not Kind.

⋀-introduction

Γ ⊢ A ∈ s Γ, x ∈ A ⊢ B ∈ refine(C) Γ, x ∈ A ⊢ D ∈ B
Γ ⊢ D ∈ (⋀ x ∈ A.B)

where x is not in F V (D) and s is not Kind.

Rules for singleton

singleton-formation  singleton-introduction
Γ ⊢ B ∈ Type Γ ⊢ A ∈ B
Γ ⊢ {A}_{B} ∈ refine(B)

\begin{matrix}Γ ⊢ B ∈ Type & Γ ⊢ A ∈ B \\ Γ ⊢ A ∈ \{A\}_{B} \end{matrix}

singleton-elimination

\begin{matrix}Γ ⊢ P_{1} ∈ \{A\}_{C} ∧ \{B\}_{C} & Γ ⊢ P_{2}[x:= A] ∈ D[x:= A] & Γ, x ∈ C ⊢ D ∈ s \\ Γ ⊢ P_{2}[x:= B] ∈ D[x:= B] \end{matrix}

where s is a refinement kind. (Note that P_{2} is a preterm.)

The second elimination rule of ATT is not present in ATTT, because it is derivable in ATTT. (If {A}_{B} is a legal term, then {A}_{B} ∈ refine(B) is derivable. Then refinesubtyping implies C ∈ B from C ∈ {A}_{B}.) Note that the remained elimination rule is a strong singleton-elimination rule. As opposite to the case of ATT, this is sound for the translation from ATTT to λ2 introduced later. The rule is stated only for refinements. The same rule for types is an admissible rule (corollary 6.)

Legal sequents and terms, etc. are defined as in ATT. Basic lemmas, e.g., the Church-Rosser property, substitution etc., hold for ATTT as well. Lemma 3 must be changed as follows:

Lemma 11 Assume that x_{1} ∈ A_{1}, …, x_{n} ∈ A_{n} ⊢ B ∈ C is a legal sequent. Then B is neither Kind nor RKind. Furthermore, for each i, A_{i} is neither Kind nor RKind, and one of the followings holds:

1. A_{i} is the kind Type and x_{1} ∈ A_{1}, …, x_{i−1} ∈ A_{i−1} ⊢ A_{i} ∈ Kind is derivable.

2. A_{i} has the form refine(D) and x_{1} ∈ A_{1}, …, x_{i−1} ∈ A_{i−1} ⊢ A_{i} ∈ RKind is derivable.

3. x_{1} ∈ A_{1}, …, x_{i−1} ∈ A_{i−1} ⊢ A_{i} ∈ Type is derivable.

4. x_{1} ∈ A_{1}, …, x_{i−1} ∈ A_{i−1} ⊢ A_{i} ∈ refine(D) is derivable for some D.

3.2 Classification of terms of ATTT

We classify the terms of ATTT as in the classification in ATT.

Definition 7 (classification under variable classification) Assume that FV (A) is a union of three disjoint sets Obj, Typ and Ref. The variables of Obj are called object variables, the variables of Ref are called refinement variables, and the variables of Typ are called type variables. Then objects, types, refinements, kinds and refinement kinds (r-kinds for short) under the classification of free variables ⟨Obj , Typ, Ref ⟩ are defined as follows:

objects 1. An object variable is an object.

2. If A and B are objects, then so is (AB).

3. If A is an object under the classification ⟨Obj ∪ {x}, Typ, Ref ⟩ and B is a type, then λx ∈ B.A is an object under the classification ⟨Obj , Typ, Ref ⟩.

types 1. A type variable is a type.

2. If A and B are types, then so is A → B.

3. If A is a type and B is a type under the classification ⟨Obj , Typ ∪{x}, Ref ⟩, then Π x ∈ Type.A is a type under the classification ⟨Obj , Typ, Ref ⟩.

refinements 1. A refinement variable is a refinement.

2. If A is an object and B is a type, then {A}_{B} is a refinement.

3. If A and B are refinements, then so are A → B, A ∨ B and A ∧ B.

4. If A is a refinement under the classification ⟨Obj , Typ ∪ {x}, Ref ⟩, then Π x ∈ Type.A is a refinement under the classification ⟨Obj , Typ, Ref ⟩.

5. If A is a type or a refinement, and B is a refinement under the classification ⟨Obj ∪{x}, Typ, Ref ⟩, then ⋀ x ∈ A.B and ⋁ x ∈ A.B are refinements under the classification ⟨Obj , Typ, Ref ⟩.

6. If A is an r-kind and B is a refinement under the classification ⟨Obj , Typ, Ref ∪ {x}⟩, then ⋀ x ∈ A.B and ⋁ x ∈ A.B are refinements under the classification ⟨Obj , Typ, Ref ⟩.

kind The constant Type is a kind.

r-kind If A is a type, then refine(A) is an r-kind.

As in the case of ATT, any legal term of ATTT is uniquely classified into one of the classifications above, or one of Kind and RKind. ATTT-versions of the basic lemmas for ATT also hold. It should be clear how to formulate and prove them and so we will not include them here.

3.3 Translation of ATTT into λ2

Now we give a translation of ATTT into a GTS-formulation of λ2. The GTS-formula-tion of λ2 is given by dropping refine(T), T ∨T, T ∧T, ⋁ x ∈ T.T, ⋀ x ∈ T.T and {T }_{T} from the grammar of preterms. The conversion rule, rule of subject reduction and all of the rules for these are also dropped, e.g., the second inference rule of Π-formationis dropped. (Note that the rule of subject reduction is an admissible rule of λ2.) The system was called λ2 in [Bar90].

Definition 8 (translation of preterms of ATTT into λ2) We define a nondeterministic translation from ATTT to λ2. That is, we define a binary relation M ⇝ M′ between preterms M of ATTT and preterms M′ of λ2, as follows:

1. RKind ⇝ Kind and c ⇝ c for the other constant c.

2. refine(A) ⇝ Type.

3. x ⇝ x.

4. If A ⇝ A′ and B ⇝ B′, then (λx ∈ A.B) ⇝ (λx ∈ A′.B′).

5. If A ⇝ A′ and B ⇝ B′, then (AB) ⇝ (A′B′).

6. If A ⇝ A′ and B ⇝ B′, then (Π x ∈ A.B) ⇝ (Π x ∈ A′.B′) and (A → B) ⇝ (A′ → B′)

7. If A ⇝ A′ and B ⇝ B′, then A op B ⇝ A′ and A op B ⇝ B′, where op is one of ∧, ∨.

8. If A ⇝ A′ and B ⇝ B′, then (OP x ∈ refine(A).B) ⇝ B′[x:= A′], where OP is one of ⋀, ⋁.

9. If B ⇝ B′ and A is not an r-kind, then (OP x ∈ A.B) ⇝ B′, where OP is one of ⋀, ⋁.

10. If B ⇝ B′, then {A}_{B} ⇝ B′.

If M ⇝ M′ holds, then we call M′ a translation of M.

The translation of judgments is naturally defined. If A ⇝ A′ and B ⇝ B′, then A ∈ B ⇝ A′ ∈ B′. The translation of contexts and sequents is not straightforward, however.

Definition 9 (translation of contexts and sequents) Let Γ be x_{1} ∈ A_{1}, …, x_{n} ∈ A_{n} and A_{i} ⇝ A′_{i} for i = 1, …, n. Set

Γ = Γ_{0}, x_{p_{1}} ∈ refine(T_{p_{1}}), Γ_{1}, …, x_{p_{m}} ∈ refine(T_{p_{m}}), Γ_{m}

such that any judgment in Γ_{j} (j = 1, …, m) is not of the form x ∈ refine(T). That is, x_{p_{1}} ∈ A_{p_{1}}, …, x_{p_{m}} ∈ A_{p_{m}} is the enumeration of all of the judgments in Γ whose A_{i} is an r-kind and refine(T_{p_{j}}) = A_{p_{j}}.

Let Γ′_{j} be the context obtained from Γ_{j} by replacing each judgment x_{i} ∈ A_{i} by x_{i} ∈ A′_{i}. For j = 1, …, m, let σ_{j} be the substitution [x_{p_{1}} := T_{p_{1}}, ⋯, x_{p_{j}} := T_{p_{j}}]. (Note that x_{p_{j}} does not occur freely in T_{p_{j+k}}, as T_{p_{j+k}} is a type.) In particular, we will denote σ_{m} by [Γ]. Set

Γ′ = Γ′_{0}, Γ′_{1}σ_{1}, …, Γ′_{m}σ_{m}.

Then we call Γ′ a translation of the context Γ and write Γ ⇝ Γ′.

Next, we define the translation of a sequent. Let S be Γ ⊢ B ∈ C. Assume that Γ ⇝ Γ′, B ⇝ B′ and C ⇝ C′. Set

S′ = Γ′ ⊢ B′[Γ] ∈ C′[Γ].

Then we call S′ a translation of the sequent S and write S ⇝ S′.

For example, x ∈ Type, z ∈ x ⊢ x ∈ Type is a translation of the legal sequent

x ∈ Type, y ∈ refine(x), z ∈ y ⊢ (y ∧ {z}_{x}) ∈ refine(x).

The soundness of the translation is stated as follows:

Theorem 4 If S is a legal sequent of ATTT and S ⇝ S′, then S′ is a legal sequent of λ2.

Note that if M is an object or a type, then it is a preterm of λ2, and any translation of M is identical to M. By this observation, the following is obvious:

Corollary 3 ATTT is a conservative extension of λ2 in the same sense of corollary 2. Furthermore, if Γ ⊢ J is provable in ATTT and Γ ⊢ J ⇝ Γ′ ⊢ J′, then Γ ⊢ J′ is also provable in ATTT.

The second part of the theorem above is a consequence of generalized weakening and the fact that any judgment K of Γ′ is derivable under the context Γ in ATTT. This fact is easily proved by the induction on the length of Γ.

An inversion principle similar to the type inversion principle for ATT (lemma 9) holds for ATTT. Hence, we can prove the strong normalization property as in the case of ATT.

Corollary 4 Every term of ATTT is strongly normalizable.

Note that strong normalization property of legal objects and types is obvious by the conservativity result.

Theorem 4 is a corollary of the following proposition.

Proposition 2 1. If S is a legal sequent of ATTT and S ⇝ S′, then S′ is a legal sequent of λ2.

2. If S is a legal sequent of ATTT and S ⇝ S′ and S ⇝ S′′, then S′ and S′′ are identical.

3. If Γ ⊢ A ∈ refine(B) is a legal sequent of ATTT and

(Γ ⊢ A ∈ refine(B)) ⇝ (Γ ⊢ A′ ∈ C),

then A′ is B and C is Type.

This propostition can be proved by simultaneous induction on derivations. The proof is straightforward, but lengthy. So we do not include it. Note that the following lemma is used to show the soundness of the singleton-elimination rule. This lemma can be proved by induction on the complextity of P.

Lemma 12 The following is an admissible rule of λ2:

Γ ⊢ A ∈ C Γ ⊢ B ∈ C Γ ⊢ P [x:= A] ∈ D Γ ⊢ D ∈ Type
Γ ⊢ P [x:= B] ∈ D

As a corollary of proposition 2, we can prove the following:

Corollary 5 If Γ ⊢ A ∈ refine(B) and Γ ⊢ A ∈ refine(B′) are legal sequents of ATTT, then B and B′ are identical.

We will call the unique type B of A ∈ refine(B) the type of A written type(A). Note that type(A) depends on the context under which A is legal. When we emphasize this fact, we will write type_{Γ}(A).

In the rule of singleton-elimination, D is restricted to refinements. The same rule for types is an admissible rule.

Corollary 6 The rule of singleton-elimination of ATTT is an admissible rule, when the sort s is replaced by the kind Type.

Proof. Assume the three premises of the rule are proveble in ATTT and s is Type. Note that D[x:= A] is identical to D, as D is a type and so x is not free in D. By the translation, the following sequents are provable in λ2:

Γ′ ⊢ A ∈ C, Γ′ ⊢ B ∈ C, Γ′ ⊢ P_{2}[x:= A] ∈ D, Γ′ ⊢ D ∈ Type.

By lemma 12, Γ′ ⊢ P_{2}[x:= B] ∈ D is derivable in λ2. By generalized weakening and corollary 3, the conclusion of the rule is derivable in ATTT.

3.4 A decidability result

We conjecture that typechecking in ATT will be undecidable. On the other hand, ATTT has a nice decidability result.

Definition 10 (family) A family is a sort or a type. If N is a family and Γ ⊢ M ∈ N is provable, then N is called a family of M under Γ. It is easy to see that a family N of M under Γ uniquely exists for any legal term M under Γ. We call this family N the family of M under Γ.

Theorem 5 Let Γ denote a context and M denote a preterm except Kind and RKind. There are algorithms V_{C} and V_{F} satisfying the followings:

1. V_{C}(Γ) always returns ⊤ or ⊥.

2. V_{C}(Γ) is ⊤ iff Γ is a legal context.

3. V_{F} (Γ, M) always returns ⊥ or a family.

4. if V_{F} (Γ, M) is ⊥, then Γ is illegal or M is illegal under Γ.

5. if V_{F} (Γ, M) is not ⊥, then V_{F} (Γ, M) is the family of M under Γ.

Corollary 7 Provability of Γ ⊢ M ∈ N is decidable, unless N is a refinement.

Objects of ATTT are regarded as programs and refinements are regarded as specifications or formulas. For a refinement N, Γ ⊢ M ∈ N means that the program M meets the specification N. This notion cannot be decidable. On the other hand, types of ATTT are regarded as types in the sense of programming languages and refinements of ATTT are regarded as specifications (or formulas). These two notions and membership of types are decidable as expected.

Contrary to corollary 7, provability of a sequent is always decidable in calculi like CoC. This is because objects of such calculi contain logical information as well as computational contents (program). Namely, they are partly proofs. It’s no wonder that proof is a decidable notion. As both of logical information and computational contents are coded by means of typed lambda-calculus, CoC cannot distinguish program-parts and proof-parts and so proof-parts must be executed in execution time. An approach to avoid this defect is keeping proof-parts in a separated term. This approach was taken in [BM91].

It is easy to define V_{C} by V_{F}, since Γ, x ∈ M is legal iff V_{F} (Γ, M) is not ⊥. We present the algorithms V_{F} below. Their properties can be proved by means of a lexicographical induction on complexity of M and the length of Γ. The proof is left to the readers.

V_{F} (Γ, M) is if V_{C}(Γ) is ⊥ then return ⊥ else if M is a variable then

if M ∈ N appears in Γ then if N is a refinement then return type_{Γ}(A) else return N else return ⊥

else if M is Type then return Kind

else if M is refine(N) then

if V_{F} (Γ, N) is Type then return RKind else return ⊥ else if M is Πx ∈ M_{1}.M_{2} then

if M_{1} is Type then if V_{F} (Γ, x ∈ M_{1}, M_{2}) is Type then return Type else if V_{F} (Γ, x ∈ M_{1}, M_{2}) is refine(N) then return refine(Πx ∈ Type.N) else return ⊥ else return ⊥

else if M is M_{1} → M_{2} then if V_{F} (Γ, M_{1}) and V_{F} (Γ, M_{2}) is Type then return Type else if V_{F} (Γ, M_{1}) is refine(N_{1}) and V_{F} (Γ, M_{2}) is refine(N_{2}) then

return refine(N_{1} → N_{2})

else return ⊥ else if M is M_{1} op M_{2}, where op is ∧ or ∨ then

if V_{F} (Γ, M_{1}) and V_{F} (Γ, M_{2}) is refine(N) then

return refine(N) else return ⊥

else if M is OP x ∈ M_{1}.M_{2} where OP is ⋀ or ⋁ then

if V_{F} (Γ, M_{1}) is a sort except Kind and V_{F} (Γ, x ∈ M_{1}, M_{2}) is refine(N) then

return refine(N) else return ⊥

else if M is {M_{1}}_{M_{2}} then if V_{F} (Γ, M_{2}) is Type and V_{F} (Γ, M_{1}) is M_{2} then return M_{2} else return ⊥

else if M is (M_{1}M_{2}) then if V_{F} (Γ, M_{1}) is Πx ∈ V_{F} (Γ, M_{2}).N then return N[x:= M_{2}] else if V_{F} (Γ, M_{1}) is V_{F} (Γ, M_{2}) → N then return N else return ⊥

else if M is λx ∈ M_{1}.M_{2} then

if V_{F} (Γ, M_{1}) is Type and V_{F} (Γ, x ∈ M_{1}, M_{2}) is a type then

return M_{1} → V_{F} (Γ, x ∈ M_{1}, M_{2}) else if M_{1} is Type then

if V_{F} (Γ, x ∈ Type, M_{2}) is a type then

return Πx ∈ Type.V_{F} (Γ, x ∈ Type, M_{2})

else return ⊥ else return ⊥

3.5 RL-rule and LR-rule

An implication of singleton-elimination rule is the following RL-rule (Right-to-Left-rule).

{Γ ⊢ P ∈ \{M\}_{C} ∧ D \atop Γ ⊢ M ∈ D}

Note that D is a refinement. Since we can move M from the right hand side of ∈ to the left hand side. We call the opposite rule LR-rule.

{Γ ⊢ M ∈ D \atop Γ ⊢ M ∈ \{M\}_{C} ∧ D}

It’s a trivial implication of the introduction rules for singleton and intersection.

In set theory, a set D has a nonempty intersection with a singleton {M}, iff M ∈ D holds. The RL-rule and LR-rule are a counterpart of this fact.

Proposition 3 RL-rule and LR-rule are derivable in ATTT.

Proof. Let’s prove RL-rule. Assume Γ ⊢ P ∈ {M}_{C} ∧D is provable. Let x be a fresh variable and s be the family of D (under Γ). Then Γ ⊢ P ∈ {M}_{C}, Γ ⊢ P ∈ {P }_{C}, Γ ⊢ P ∈ D, Γ, x ∈ C ⊢ D ∈ s are derivable. Regarding P as x[x:= P], the conclusion of the RL-rule is derived by the singleton-elimination form these.

Note that the strong rule is essentially used in the proof above. It is easy to see the (weak) rule of singleton-elimination and LR-rule imply the strong rule of singletonelimination. The proof of this fact is left for readers.

By means of LR-rule and RL-rule, we may regard refinement types as predicates (or sets). Let D be a refinement type of the kind refine(A) and M be an object of the type A. Then, D may be regarded as a predicate on the type A and the refinement D ∧ {M} may be regarded as the application D(M) of the predicate D to the object M. We regard D ∧ {M} a true formula iff it has the element M. By LR-rule and RL-rule, D ∧ M is true iff M ∈ D holds. In this sense, D ∧ − is a transformation from refinements to predicates.

An implication of RL-rule and LR-rule is subject reduction.

Corollary 8 Subject reduction holds for ATTT.

Proof. Assume Γ ⊢ M ∈ N is provable and M reduces to M′. We wish to prove Γ ⊢ M′ ∈ N. If N is a term of λ2, then we can prove it by subject reduction for λ2 and corollary 3. If N is a refinement, then we apply LR-rule and conversion rule to it and get Γ ⊢ M ∈ N ∧ {M′}. By RL-rule, we get the sequent to be proved. If N is a refinement kind, then we can prove it by easy induction on the derivation.

Another implication of RL-rule and LR-rule is distributive laws for union and intersection discussed in 2.1.3. Let us prove the following:

Γ_{0}, x ∈ (a ∨ b) ∧ c ⊢ x ∈ (a ∧ c) ∨ (b ∧ c),

where Γ_{0} is a context which maintains a, b, c are refinements of a type. Let Γ_{1} be Γ_{0}, x ∈ (a ∨ b) ∧ c). Then the following are derivable:

(1) Γ_{1} ⊢ x ∈ (a ∧ {x}) ∨ (b ∧ {x}) (2) Γ_{1} ⊢ x ∈ c

Let Γ_{2} be the context Γ_{1}, y ∈ a ∧ {x}. Using RL-rule, we can derive Γ_{2} ⊢ x ∈ a. From this and (2), we can derive Γ_{2} ⊢ x ∈ (a ∧ c) ∨ (b ∧ c). Similarly, Γ_{1}, y ∈ b ∧ {x} ⊢ x ∈ (a ∧ c) ∨ (b ∧ c) is derivable. By applying ∨-elimination to (1) and these two, we can derive the judgment to be proved. The other law presented in 2.1.3 is proved similarly.

Note that a special case of the distributive law considered above is x ∈ (a ∨ b) ∧ {x} = (a ∧ {x}) ∨ (b ∧ {x}). Regarding refinements as predicates, this turns out (a ∨ b)(x) = a(x) ∨ b(x). This is the distributivity of application and union.

3.6 Semantics of ATTT

The semantics of ATTT is fairly simple. We start with the so called BMM-semantics of λ2 (see [BMM90] for BMM-semantics). The BMM-semantics is a “concrete” semantics, that is, each type of λ2 is interpreted as a set. Let [[A]]_{ρ} be the interpretation of type A under assignment ρ. Then we interpret refinement kinds by

[[refine(A)]]_{ρ} = Pow([[A]]_{ρ}).

Pow(X) is the powerset of X. Hence, refinements of a type are subsets of the interpretation of the type. Singleton, intersection and union refinements are interpreted in the usual sense of set theory. Then it is straightforward to check the soundness. A more intrinsic semantics could be given in appropriate categories, such as the topos of Pitts [Pit87]. Furthermore, we conjecture that there is a PL-category-like second-order categorical framework for ATTT.

As remarked in section 2.4, the PER-semantics for ATT has some anomalies. But this is not so in ATTT, because we can state the extensionality rule only for types and not for refinements.

Extensionality

Γ ⊢ A ∈ Type Γ ⊢ B ∈ Type
Γ, f ∈ (A → B), g ∈ (A → B), x = y ∈ A ⊢ f(x) = g(y) ∈ B
Γ, f ∈ (A → B), g ∈ (A → B) ⊢ f = g ∈ (A → B)

Note that we can define the equality judgment only for types and not for refinements, since a = b ∈ A is a ∈ {b}_{A} and so A must be a type. Hence, two functions from refinement R_{1} → R_{2} must be compared in the type type(R_{1}) → type(R_{2}).

3.7 An example of a specification

Here, we present an example of a specification in ATTT. We specify the quotient and remainder algorithm for natural numbers. Let Nat be a type of natural numbers, e.g., the polymorphic natural numbers Πx ∈ Type.(x → x) → (x → x). A specification would be

∀a ∈ Nat.∀b ∈ Nat^{+}.∃q ∈ Nat.∃r ∈ Nat.(a = b ∗ q + r ∧ r < b).

In the above, Nat^{+} is a refinement of positive natural numbers. It may be defined by ⋁ n ∈ Nat.{suc(n)}_{Nat}. Let R(a, b, q, r) be a refinement which is inhabited iff the formula holds. As we don’t wish to have a proof for R(a, b, q, r) in the outputs of the quotient and remainder functions to be specified, we regard ∃r ∈ Nat as a subset type operation. Hence ∃r ∈ Nat.(a = b ∗ q + r ∧ r < b) should be replaced by

⋁ r ∈ Nat. ⋁ prf ∈ R(a, b, q, r).{r}_{Nat}.

Hence the specification turns to

∀a ∈ Nat.∀b ∈ Nat^{+}.∃q ∈ Nat. ⋁ r ∈ Nat. ⋁ prf ∈ R(a, b, q, r).{r}_{Nat}.

The universal and existential quantifiers are defined by the same way as in 2.6. The type of this specification (refinement) is Nat → Nat → (Nat × Nat), where “×” is the polymorphic cartesian product. Note that the type of the specification is irrelevant to the type of R(a, b, q, r).

Another formalization of the specification without the auxiliary refinement R(a, b, q, r) is

∀a ∈ Nat.∀b ∈ Nat^{+}.∃q ∈ Nat. ⋁ r ∈ Nat.
⋁ p1 ∈ {a}_{Nat} ∧ {b ∗ q + r}_{Nat}.
⋁ p2 ∈ (⋁ x ∈ Nat^{+}.{r + x}_{Nat} ∧ {b}_{Nat}).{r}_{Nat}.

The type of this specifications is again Nat → Nat → (Nat × Nat).

Note that the induction principle for Nat must be added to ATTT to prove these specifications as was done in systems like PX and Coq. (See 2.4.1 and 4.3 of [HN88]and 1.1.8 of [D^{+}91].)

4 Related works

Many authors have studied union and intersection types from disparate motivations, e.g., [FP91, MPS86, BDC91, Pie90, Pie91b, Rey88]. A more complete list of the literature on the subject and a fine survey of them can be found in [Pie91b]. But we here list only related work devoted to the same aim as ours: program extraction.

No literature has considered the suite of types, Singleton, Union and Intersection Types, SUIT in short, for program extraction. An exception is the work by Parigot and Krivine. They considered first order and second order intersections for a similar purpose to program extraction [Par88, Par89, KP90]. Parigot uses a type closely related to singleton types in [Par89]. But they do not consider union types, because they use functions explicitly rather than existential quantifiers.

Although none of types of SUIT is used explicitly, Paulin’s modified realizability interpretation for CoC [PM89] and Burstall’s deliverable [BM91] seem closely related to our work. Actually, these two were our constant sources of ideas. As we pointed out, ATTT is an axiomatization of modified realizability. The translation from ATTT to λ2 seems to be a counterpart of Paulin’s extraction operator E in [PM89]. There would be a formal relationship between Paulin’s realization method and a higher order version of ATTT.

Burstall’s deliverable is closely related to modified realizability and so to Paulin’s work. His motivation was to separate proofs and programs in program development via CoC or ECC. This is close to our motivation of separating logic and computation. In ATTT, refinements serve as the device of logic and types serve as the device of computation. Unlike the deliverable approach, the logical part, i.e., inference on refinement, is not recorded in the terms developed. In deliverables, programs and proofs are separated terms of CoC. Roughly, a deliverable is a pair of a program and its correctness proof. In our case, the program part of a deliverable is the term A of the derived judgment A ∈ B and the proof is represented as the derivation of the judgment. The exact relationships to Paulin and Burstall’s work remain to be studied.

5 Future work

Full decidability of typechecking with SUIT is hopeless. Typechecking in the deliverable approach is reduced to typechecking of CoC and so is automatic. This is because of the presence of a term recording a history of proofs separately from programs. We feel that this approach separates proofs and programs more than we expect. There seems no apparent association of subparts of the proof-term and program-term of a deliverable. It would be difficult to see that a subterm of a program-term was verified by a part of the proof-term, and in what way. We are working to add annotations recording history of derivations to our calculi. Such annotations should record all the logical information of inference rules, but they should not be respected by computaion. When annotations are literally erased from the program text, then we get the pure program and the results of the pure program and the original program with annotations are the same. That is, these annotations should work like the documentation part in Knuth’s WEB language. With these annotations, typechecking in ATT and ATTT must become decidable.

The application of SUIT to program extraction was briefly mentioned. We have already had some applications of SUIT for the aim, which will appear elsewhere. But SUIT in practice of program extraction has not been well studied. In particular, we have not considered SUIT in backward reasoning.

We have designed higher order versions of ATT and ATTT. Their metatheories are yet to be studied. We believe that there is a general method for adding SUIT to a type theory at least in the way of ATTT without interfering with any features of the original type theory. Such a method might give a general way to add logic to type theory.

The right semantics of ATT and ATTT is yet to investigate as noted in the paper. Furthermore, semantics of SUIT fully consistent with extensionality is yet to study. We conjecture that there is no such semantics.

Acknowledgments

I thank Zhaohui Luo, Christine Paulin, Benjamin Pierce and Yukihide Takayama for fruitful discussions on the subject and helpful comments on the paper. I am very grateful for thorough comments and criticisms on the paper by Jan Smith and Tierry Coquand. Their comments and criticisms were extremely helpful to polish the paper.

References

[Bar90] H. Barendregt. Introduction to generalized type systems. Technical Report no.90-8, University of Nijmegen, May 1990.

[BDC91] F. Barbanera and M. Dezani-Ciancaglini. Intersection and union types. In T.Ito and A.R.Meyer, editors, Theoretical Aspect of Computer Software (Lecture Notes in Comuter Science No. 526), pages 651–674, Berlin, 1991. Springer-Verlag.

[BM91] R. Burstall and J. McKinna. Deliverable: an approach to program development in the calculus of constructions. An earlier version is in the preliminary proceeding of the Logical Frameworks BRA meeting at Sophia Antipolis 1990, April 1991.

[BMM90] K.B. Bruce, A.R. Meyer, and J. C. Mitchell. The semantics of second-order lambda calculus. Information and Computation, 85:76–134, 1990.

[CH88] Th. Coquand and G. Huet. Calculus of constructions. Information and Computation, 76:95–120, 1988.

[Coq86] Th. Coquand. An analysis of Girard’s paradox. In Proceedings of First Annual Symposium on Logic in Computer Science, 1986.

[D^{+}91] C. Dowek et al. The coq proof assistant user’s guide, version 5.6. Technical Report No. 134, INRIA, December 1991.

[FP91] T. Freeman and F. Pfenning. Refinement types for ML. In ACM SIGPLAN’91 Conference on Programming Language Design and Implementation, Toronto, Ontario. ACM Press, June 1991.

[Hay90] S. Hayashi. Constructive mathematics and computer-aided reasoning systems. In P.P. Petkov, editor, MATHEMATICAL LOGIC, pages 43–52. Plenum Press, New York, 1990.

[Hay91] S. Hayashi. Singleton, union and intersection types for program extraction. In T.Ito and A.R.Meyer, editors, Theoretical Aspect of Computer Software (Lecture Notes in Comuter Science No. 526), pages 701–730, Berlin, 1991. Springer-Verlag.

[HN88] S. Hayashi and H. Nakano. PX: A Computational Logic. The MIT Press, Cambridge, Mass., 1988.

[KP90] J.-L. Krivine and M. Parigot. Programmimg with proofs. Journal of Information Processing and Cybernetics EIK, 26:149–167, 1990.

[Lei86] D. Leivant. Typing and convergence in the lambda calculus. Theoretical Computer Science, 44:51–68, 1986.

[Luo90] Z. Luo. An Extended Calculus of Constructions. PhD thesis, Department of Computer Science, University of Edinburgh, July 1990.

[Mar71] P. Martin-Löf. A theory of types. Technical Report 71-3, University of Stockholm, 1971.

[Mar82] P. Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology, and Philosophy of Science VI, pages 153–179. North-Holland, 1982.

[Mit90] J. C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, pages 365–458. North-Holland, 1990.

[Mog88] E. Moggi. The Partial Lambda-Calculus. PhD thesis, Department of Computer Science, University of Edinburgh, 1988.

[MPS86] D. MacQueen, G. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. Information and Control, 71:95–130, 1986.

[NPS90] B. Nordström, K. Petersson, and J.M. Smith. Programming in Martin-Löf’s type theory, an introduction. Clarendon Press, Oxford, 1990.

[Par88] M. Parigot. Programming with proofs: a second order type theory. In ESOP ’88 (Lecture Notes in Computer Science No. 300). Springer-Verlag, 1988.

[Par89] M. Parigot. Recursive programming with proofs. In Proceedings of Symposium Mathematiques et Informatique, Luminy, France, October 1989. To appear in Theoretical Computer Science.

[Pie90] B.C. Pierce. Preliminary investigation of a calculus with intersection and union types. Unpublished manuscript, June 1990.

[Pie91a] B.C. Pierce. personal communication. 1991.

[Pie91b] B.C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, School of Computer Science, Carnegie Mellon University, Feburary 1991.

[Pit87] A.M. Pitts. Polymorphism is set theoretic constructively. In D.H. Pitt et al., editors, Category theory and computer science (Lecture Notes in Comuter Science No. 283), pages 12–39, Berlin, 1987. Springer-Verlag.

[Plo85] G. Plotkin. Lectures given at ASL Stanford meeting. Unpublished lecture notes, July 1985.

[PM89] C. Paulin-Mohring. Extracting F_{ω}’s programs from proofs in the calculus of construction. In Proceedings of 16th Annual ACM Symposium on Principles of Programming Languages, 1989.

[Rey88] J.C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, School of Computer Science, Carnegie Mellon University, June 1988.

[Ros86] G. Rosolini. Continuity and effectiveness in topoi. PhD thesis, Department of Computer Science, Carnegie-Mellon University, 1986.

[Tur89] D. Turner. A new formulation of constructive type theory. In P. Dybjer et al., editors, Proceedings of the Workshop on Programming Logic, pages 258–294, 1989. Report 54, Programming Methodology Group, Department of Computer Science, Chalmers University of Technology and University of Göteborg.