A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

Andreas Abel^{1}, Thierry Coquand^{2}, and Miguel Pagano^{3}

1 Ludwig-Maximilians-Universität München, abel@informatik.uni-muenchen.de

                2 Göteborg University, coquand@cs.chalmers.se

3 Universidad Nacional de Córdoba, miguel.pagano@gmail.com

Abstract. We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.

1 Introduction and Related Work

One of the raisons d’être of proof-checkers like Agda [26], Coq [18], and Epigram [23] is to decide if a given term has some type; i.e., if a term corresponds to a proof of a proposition [17]. Hence, the convenience of such a system is, in part, determined by the types for which the system can check membership. We extend the decidability of type-checking done in previous works [1, 2] for Martin-Löf type-theories [21, 25] by considering singleton types and proof-irrelevant propositions.

Singleton types were introduced by Aspinall [8] in the context of specification languages. An important use of singletons is as definitions by abbreviations (see [8, 14]); they were also used to model translucent sums in the formalisation of SML [19]. It is interesting to consider singleton types because beta-eta phase separation fails: one cannot do eta-expansion before beta-normalisation because the shape of the types at which to eta-expand is still unknown at this point; and one cannot postpone eta-expansion after beta-normalisation, because etaexpansion can trigger new beta-reductions. Stone and Harper [29] decide type checking in a LF with singleton types and subtyping. Yet it is not clear whether their method extends to computation on the type level. As far as we know, our work is the first where singleton types are considered together with a universe.

De Bruijn proposed the concept of irrelevance of proofs [11], for reducing the burden in the formalisation of mathematics. As shown by Werner [30], the use of proof-irrelevance types together with sigma types is one way to get subset types à la PVS [27] in type-theories having the eta rule—this direction was explored by Sozeau [28, Sec. 3.3].

Checking dependent types relies on checking types for equality. To this end, we compute η-long normal forms using normalisation by evaluation (NbE) [22]. Syntactic expressions are evaluated into a semantic domain and then reified back to expressions in normal form. To handle functional and open expressions, the semantic domain has to be equipped with variables; a major challenge in rigorous treatments of NbE has been the problem to generate fresh identifiers. Solutions include term families [10], liftable de Bruijn terms [7], or Kripke semantics [4]. In this work we present a novel formulation of NbE which avoids the problem completely: reification is split into an η-expansion phase (↓) in the semantics, followed by a read back function (R) into the syntax which is indexed by the number of already used variables. This way, a standard PER model is sufficient, and technical difficulties are avoided.

Outline. The definitions of two calculi are presented in section 2. In section 3 we define the semantics of this LF in a PER model, and we show soundness of the model wrt. the derived rules of the calculus. We use this model to introduce a NbE algorithm, for which we prove completeness (if t = s is derivable, then nbe(t) and nbe(s) are identical). In section 4 we prove, using logical relations, the soundness of the algorithm (i.e., t = nbe(t) is derivable). In section 5 we define a bi-directional algorithm for checking the type of normal forms and inferring the type of neutral terms.

2 The calculus as a Generalised Algebraic Theory

In the section, we introduce the calculus. For ease of reading, and for showing the modularity of our approach, we present it as two calculi: the first one has dependent function spaces, singleton types, and a universe closed under function spaces and singletons. In the second calculus we leave out singleton types and we add proof-irrelevant types.

We present the calculi using the formalism proposed by Cartmell for generalised algebraic theories (GAT) [12]; however, our calculi are not proper GATs (the rules are written in the so-called “informal syntax” and the rule for application is ambiguous). We give only the introductory rules and the axioms; the rules stating that equality is a congruence relation, called derived rules, are omitted. An example of a derived rule is

\frac{A = B ∈ Type(Γ) γ = δ ∈ Δ → Γ}{A γ = B δ ∈ Type(Δ)} .

Calculus with singleton types. Sorts. The set of sort symbols is {Ctx, →, Type, Term}.

\overline{Ctx is a type} (ctx-sort)  \frac{Γ, Δ ∈ Ctx}{Γ → Δ is a type} (subs-sort)
\frac{Γ ∈ Ctx}{Type(Γ) is a type} (type-sort) \frac{Γ ∈ Ctx  A ∈ Type(Γ)}{Term(Γ, A) is a type} (term-sort)

In the following, whenever a rule has a hypothesis A ∈ Type(Γ), then Γ ∈ Ctx shall be a further, implicit hypothesis. Similarly, σ ∈ Γ → Δ presupposes Γ ∈ Ctx and Δ ∈ Ctx, and t ∈ Term(Γ, A) presupposes A ∈ Type(Γ), which in turn presupposes Γ ∈ Ctx. Note that judgements of the form Γ ∈ Ctx, A ∈ Type(Γ), t ∈ Term(Γ, A), and σ ∈ Γ → Δ correspond to the more conventional forms Γ ⊢, Γ ⊢ A, Γ ⊢ t : A, and Γ ⊢ σ : Δ, resp. In the rest of the paper we use the latter.

Operators. The set of operators is quite large and instead of giving it at once, we define it as the union of the disjoint sets of operators for contexts, substitutions, types, and terms.

Contexts. There are two operators for contexts: S_{C} = {⋄, . }.

\overline{⋄ ∈ Ctx} (empty-ctx)  \frac{Γ ∈ Ctx  A ∈ Type(Γ)}{Γ.A ∈ Ctx} (ext-ctx)

Substitutions. For substitutions we have five operators: S_{S} = {id , ⟨⟩, ( , ), , p}.

\frac{Γ ∈ Ctx}{id_{Γ} ∈ Γ → Γ} (id-subs)  \frac{Γ ∈ Ctx}{⟨⟩ ∈ Γ → ⋄} (empty-subs)

\frac{δ ∈ Γ → Θ  σ ∈ Θ → Δ}{σ δ ∈ Γ → Δ} (comp-subs)

\frac{σ ∈ Γ → Δ  t ∈ Term(Γ, A σ)}{(σ, t) ∈ Γ → Δ.A} (ext-subs)  \frac{A ∈ Type(Γ)}{p ∈ Γ.A → Γ} (fst-subs)

Types. The set of operators for types is S_{T} = {U, Fun , , { } }.

\frac{Γ ∈ Ctx}{U ∈ Type(Γ)} (u-f) \frac{A ∈ Term(Γ, U)}{A ∈ Type(Γ)} (u-el) \frac{A ∈ Type(Γ)  B ∈ Type(Γ.A)}{Fun A B ∈ Type(Γ)} (fun-f)

\frac{A ∈ Type(Γ)  t ∈ Term(Γ, A)}{\{t\}_{A} ∈ Type(Γ)} (sing-f) \frac{A ∈ Type(Δ)  σ ∈ Γ → Δ}{A σ ∈ Type(Γ)} (subs-type)

Terms. The set of operators for terms is S_{E} = {Fun , { } , , q, λ , App }.

\frac{A ∈ Term(Γ, U)  B ∈ Term(Γ.A, U)}{Fun A B ∈ Term(Γ, U)} (fun-u-i) \frac{t ∈ Term(Γ.A, B)}{λt ∈ Term(Γ, Fun A B)} (fun-i)

\frac{B ∈ Type(Γ.A)  t ∈ Term(Γ, Fun A B)  u ∈ Term(Γ, A)}{App t u ∈ Term(Γ, B (id_{Γ} , u))} (fun-el)

\frac{σ ∈ Γ → Δ  t ∈ Term(Δ, A)}{t σ ∈ Term(Γ, A σ)} (subs-term) \frac{A ∈ Type(Γ)}{q ∈ Term(Γ.A, A p)} (hyp)

\frac{A ∈ Term(Γ, U)  t ∈ Term(Γ, A)}{\{t\}_{A} ∈ Term(Γ, U)} (sing-u-i) \frac{t ∈ Term(Γ, A)}{t ∈ Term(Γ, \{t\}_{A})} (sing-i)

\frac{a ∈ Term(Γ, A)  t ∈ Term(Γ, \{a\}_{A})}{t ∈ Term(Γ, A)} (sing-el)

Axioms. We give the axioms without the premises, except in the cases where they can not be inferred.

Substitutions.

(σ δ) γ = σ (δ γ)  ⟨⟩ σ = ⟨⟩
id_{Γ} σ = σ  σ id_{Γ} = σ
id_{⋄} = ⟨⟩  id_{Γ.A} = (p, q)
p (σ, t) = σ  (σ, t) δ = (σ δ, t δ)

Substitutions on types, and terms; η and β-axioms.

U γ = U  {t}_{A} σ = {t σ}_{A σ}
(Fun A B) σ = Fun (A σ) (B (σ p, q))  q (σ, t) = t
t (σ δ) = (t σ) δ  t id_{Γ} = t
(λt) σ = λ(t (σ p, q))  (App r s) σ = App (r σ) (s σ)
App (λt) r = t (id_{Γ} , r)  λ(App (t p) q) = t

\frac{t, t′ ∈ Term(Γ, \{a\}_{A})}{t = t′ ∈ Term(Γ, \{a\}_{A})} (sing-eq-i) \frac{t = t′ ∈ Term(Γ, \{a\}_{A})}{t = t′ ∈ Term(Γ, A)} (sing-eq-el)

Notation. We denote with |Γ | the length of the context Γ; and Γ!i is the projection of the i-th component of Γ, for 0 ⩽ i < |Γ |. We say Δ ⩽^{i} Γ if Δ ⊢ p^{i} : Γ; where p^{i} is the i-fold composition of p with itself. We denote with Terms the set of words freely generated using symbols in S_{S} ∪ S_{T} ∪ S_{E}. We write t ≡_{T} t′ for denoting syntactically equality of t and t′ in T ⊆ Terms. We call A the tag of {a}_{A}.

Definition 1 (Neutral terms, and normal forms).

Ne ∋ k ::= q | qp^{i+1} | App k v
Nf ∋ v, V, W ::= U | Fun V W | {v}_{V} | λv | k

Remark 1 (Weakening of judgements). Let Δ ⩽^{i} Γ, Γ ⊢ A = A′, and Γ ⊢ t = t′ : A; then Δ ⊢ A p^{i} = A′ p^{i}, and Δ ⊢ t p^{i} = t′ p^{i} : A p^{i}.

Remark 2 (Syntactic validity).

1. If Γ ⊢ t : A, then Γ ⊢ A.

2. If Γ ⊢ t = t′ : A, then both Γ ⊢ t : A, and Γ ⊢ t′ : A.

3. If Γ ⊢ A = A′, then both Γ ⊢ A, and Γ ⊢ A′.

Lemma 1 (Inversion of types).

1. If Γ ⊢ Fun A B, then Γ ⊢ A, and Γ.A ⊢ B.

2. If Γ ⊢ {a}_{A}, then Γ ⊢ A, and Γ ⊢ a : A.

3. If Γ ⊢ k, then Γ ⊢ k : U.

Lemma 2 (Inversion of typing).

1. If Γ ⊢ Fun A′ B′ : A, then Γ ⊢ A′ : U, and also Γ.A′ ⊢ B′ : U;

2. If Γ ⊢ {b}_{B} : A, then Γ ⊢ B : U, and also Γ ⊢ b : B;

3. If Γ ⊢ λt : A, then Γ.A′ ⊢ t : B′.

4. If Γ ⊢ t : {a}_{A}, then Γ ⊢ t : A, and Γ ⊢ t = a : A.

5. If Γ ⊢ q p^{i} : A, then either Γ ⊢ A = (Γ!i) p^{i+1}; or Γ ⊢ A = {a}_{A′}, and Γ ⊢ a = q p^{i} : A′.

Calculus with Proof-Irrelevance. Our treatment of proof-irrelevance is based on [9, 20]. The motivation for a canonical element witnessing the existence of a proof is to keep the modularity of the algorithm for deciding equality; but since its introduction breaks completeness of type-checking, we consider two calculi: the proof (programming) developments are done in a calculus without prf-tm, and the type-checking is performed in a calculus with it. We show then that this is a conservative extension.

Introductory rules.

\frac{A ∈ Type(Γ)}{Prf A ∈ Type(Γ)} (prf-f) \frac{a ∈ Term(Γ, A)}{[a] ∈ Term(Γ, Prf A)} (prf-i) \frac{t ∈ Term(Γ, A)}{O ∈ Term(Γ, Prf A)} (prf-tm)

\frac{A ∈ Type(Γ)  t, t′ ∈ Term(Γ, Prf A)}{t = t′ ∈ Term(Γ, Prf A)} (prf-eq)

\frac{B ∈ Type(Γ)  b ∈ Term(Γ.A, B p)  t ∈ Term(Γ, Prf A)}{b where^{B} t ∈ Term(Γ, Prf B)} (prf-el)

(Prf A) δ = Prf (A δ)  [t] δ = [t δ]  O δ = O
(b where^{B} t) δ = b (δ p, q) where^{B δ} (t δ)  b where^{B} [t] = [b (id, t)]

Lemma 3 (Inversion).

1. If Γ ⊢ [t] : A, then Γ ⊢ A = Prf A′ and Γ ⊢ t′ : A′.

2. If Γ ⊢ b where^{B} t : A, then Γ ⊢ A = Prf B, and Γ ⊢ t : Prf A′, and Γ.A′ ⊢ b : B p.

As is expected we have now more normal forms, and more neutral terms:

Ne ∋ k ::= … | v where^{V} k
Nf ∋ v, V ::= … | Prf V | [v] | O

Now we prove that the calculus with prf-tm is a conservative extension of the one without it. We decorate the turnstile, and the equality symbol with ^{∗} for referring to judgements in the extended calculus.

Definition 2. A term t′ is called a lifting of a term t, if all the occurrences of O in t have been replaced by terms s_{0}, …, s_{n−1}, and O does not occur in any s_{i}. We extend this definition to substitutions, contexts, and equality judgements.

If Γ′ is a lifting of Γ, and Γ =^{∗} Γ′, and also Γ′ ⊢ then we say that Γ′ is a good-lifting of Γ. We extend the definition of good-lifting to the others kinds of judgement.

Lemma 4. Let Γ ⊢^{∗} J, then there exists a good-lifting Γ′ ⊢ J′; moreover for any other good-lifting Γ′′ ⊢ J′′ of Γ ⊢^{∗} J, we have Γ′ = Γ′′, and Γ′ ⊢ J′ = J′′.

Corollary 1. The calculus ⊢^{∗} is a conservative extension of ⊢.

3 Semantics

In this section we define a PER model of the calculus presented in the previous section. The model is used to define a normalisation function later.

3.1 PER semantics

Definition 3. We define a domain D = 𝕆 ⊕ Var_{⊥} ⊕ [D → D] ⊕ D × D ⊕ D × D ⊕ 𝕆 ⊕ D × [D → D] ⊕ D × D, where Var is a denumerable set of variables (as usual we write x_{i} and assume x_{i} ≠ x_{j} if i ≠ j, for i, j ∈ ℕ), E_{⊥} = E ∪ {⊥} is lifting, 𝕆 = {⊤}_{⊥} is the Sierpinski space, [D → D] is the set of continuous functions from D to D, ⊕ is the coalesced sum, and D × D is the Cartesian product of D [6].

An element of D which is not ⊥ can be of one of the forms:

⊤  (d, d′)  for d, d′ ∈ D
Var x_{i}  U  for x_{i} ∈ Var
Lam f  Fun d f  for d ∈ D, and f ∈ [D → D]
App d d′  Sing d d′  for d, d′ ∈ D .

We define application · : [D × D → D] and the projections p, q : [D → D] by

f · d = if f = Lam f′ then f′ d else ⊥,
p d = if d = (d_{1}, d_{2}) then d_{1} else ⊥,
q d = if d = (d_{1}, d_{2}) then d_{2} else ⊥.

We define a partial function R : ℕ → D → Terms which reifies elements from the model into terms; this function is similar to the read-back function of Gregoire and Leroy’s [16].

Definition 4 (Read-back function).

R_{j} U = U
R_{j} (Fun X F) = Fun (R_{j} X)
(R_{j+1} (F (Var x_{j})))
R_{j} (Sing d X) = {R_{j} d}_{R_{j} X}

R_{j} (App d d′) = App (R_{j} d) (R_{j} d′)
R_{j} (Lam f) = λ(R_{j+1} (f(Var x_{j})))
R_{j} (Var x_{i}) = \begin{cases}q & if j ⩽ i \\ q p^{j−i−1} & if j > i \end{cases}

Partial Equivalence Relations. A partial equivalence relation (PER) over a set D is a binary relation over D which is symmetric and transitive.

If R is a PER over D, and (d, d′) ∈ R then it is clear that (d, d) ∈ R. We define dom(R) = {d ∈ D | (d, d) ∈ R} . If (d, d′) ∈ R, sometimes we will write d = d′ ∈ R, and d ∈ R if d ∈ dom(R). We denote with PER(D) the set of all PERs over D.

If R ∈ PER(D) and F : dom(R) → PER(D), we say that F is a family of PERs indexed by R iff for all d = d′ ∈ R, F d = F d′. If F is a family indexed by R, we write F : R → PER(D).

We define two binary relations over D: one for neutral terms and the other for normal forms.

d = d′ ∈ Ne : ⟺ ∀i ∈ ℕ. R_{i} d and R_{i} d′ are defined and R_{i} d ≡_{Ne} R_{i} d′
d = d′ ∈ Nf : ⟺ ∀i ∈ ℕ. R_{i} d and R_{i} d′ are defined and R_{i} d ≡_{Nf} R_{i} d′

The following definitions are standard [8, 14] (except for 1); they will be used in the definition of the model.

Definition 5. Let X ∈ PER(D) and F ∈ X → PER(D).

– 1 = {(⊤, ⊤)};

– ∐ X F = {(d, d′) | p d = p d′ ∈ X and q d = q d′ ∈ F (p d)};

– ∏ X F = {(f, f′) | f · d = f′ · d′ ∈ F d, for all d = d′ ∈ X };

– {{d}}_{X} = {(e, e′) | d = e ∈ X and d = e′ ∈ X }.

We define U, T ∈ PER(D) and [ ] : dom(T ) → PER(D) using Dybjer’s schema of inductive-recursive definition [15]. We show then that [ ] is a family of PERs over D.

Definition 6 (PER model).

– Inductive definition of U ∈ PER(D).

• Ne ⊆ U,

• if X = X′ ∈ U and d = d′ ∈ [X], then Sing d X = Sing d′ X′ ∈ U,

• if X = X′ ∈ U and for all d = d′ ∈ [X], F d = F′ d′ ∈ U then

Fun X F = Fun X′ F′ ∈ U.

– Inductive definition of T ∈ PER(D).

• U ⊂ T ,

• U = U ∈ T ,

• if X = X′ ∈ T , and d = d′ ∈ [X] then Sing d X = Sing d′ X′ ∈ T ,

• if X = X′ ∈ T , and for all d = d′ ∈ [X], F d = F′ d′ ∈ T , then

Fun X F = Fun X′ F′ ∈ T .

– Recursive definition of [ ] ∈ dom(T ) → PER(D).

• [U] = U,

• [Sing d X] = {{d}}_{[X]},

• [Fun X F] = ∏ [X] (d ↦ [F d]),

• [d] = Ne, in all other cases.

Lemma 5. The function [ ] is a family of PER(D) over T .

3.2 Normalisation and η-Expansion in the Model

The usual way to define NbE [7] is to introduce a reification function which maps elements from the model into normal forms; and a function mapping neutral terms to elements of the model (the former function is called the inverse of the evaluation function, and the later “make self evaluating” in [10]). A tricky point of the algorithm is to find a new variable when reifying functions as abstractions.

In this work we do not need to worry about variable capturing when reifying, because we can define functions corresponding to reification, and lifting of neutrals in the model avoiding completely the need to deal with fresh variables.

Definition 7. The partial functions ↑ , ↓ : D → D → D and ⇓ : D → D are given as follows:

↑_{Fun X F} d = Lam (e ↦ ↑_{F e} App d ↓_{X} e) ↓_{Fun X F} d = Lam (e ↦ ↓_{F ↑_{X} e} (d · ↑_{X} e))
↑_{Sing d X} e = d  ↓_{Sing d X} e = ↓_{X} d
↑_{U} d = d  ↓_{U} d = ⇓ d
↑_{d} e = e  ↓_{d} e = e, in all other cases.
⇓(Fun X F) = Fun (⇓ X) (d ↦ ⇓(F ↑_{X} d)) ⇓ U = U
⇓(Sing d X) = Sing (↓_{X} d) (⇓ X)  ⇓ d = d, in all other cases.

Lemma 6 (Characterisation of ↑, ↓, and ⇓). Let X = X′ ∈ T , then

1. if k = k′ ∈ Ne then ↑_{X} k = ↑_{X′} k′ ∈ [X];

2. if d = d′ ∈ [X], then ↓_{X} d = ↓_{X′} d′ ∈ Nf ;

3. and also ⇓ X = ⇓ X′ ∈ Nf .

Definition 8 (Semantics).

Contexts.

[[⋄]] = 1  [[Γ.A]] = ∐ [[Γ]] (d ↦ [[[A]]d])

Substitutions.

[[⋄]]d = ⊤  [[id]]d = d
[[(γ, t)]]d = ([[γ]]d, [[t]]d)  [[p]]d = p d
[[γ δ]]d = [[γ]]([[δ]]d)

Terms (and types).

[[U]]d = U  [[Fun A B]]d = Fun ([[A]]d) (e ↦ [[B]](d, e))
[[{a}_{A}]]d = Sing ([[a]]d) ([[A]]d)  [[App t u]]d = [[t]]d · [[u]]d
[[λt]]d = Lam (d′ ↦ [[t]](d, d′))  [[t γ]]d = [[t]]([[γ]]d)
[[q]]d = q d

Definition 9 (Validity).

1. ⋄ ⊨ iff true

2. Γ.A ⊨ iff Γ ⊨ A

3. Γ ⊨ A iff Γ ⊨ A = A

4. Γ ⊨ A = A′ iff Γ ⊨ and for all d = d′ ∈ [[Γ]], [[A]]d = [[A′]]d′ ∈ T

5. Γ ⊨ t : A iff Γ ⊨ t = t : A

6. Γ ⊨ t = t′ : A iff Γ ⊨ A and for all d = d′ ∈ [[Γ]], [[t]]d = [[t′]]d′ ∈ [[[A]]d]

7. Γ ⊨ σ : Δ iff Γ ⊨ σ = σ : Δ

8. Γ ⊨ σ = σ′ : Δ iff Γ ⊨, Δ ⊨, and for all d = d′ ∈ [[Γ]], [[σ]]d = [[σ′]]d′ ∈ [[Δ]].

Theorem 1 (Soundness of the Judgements). if Γ ⊢ J, then Γ ⊨ J.

Proof. By induction on Γ ⊢ J.

Theorem 2 (Completeness of NbE). If ⊢ t = t′ : A, then ↓_{[[A]]} [[t]] = ↓_{[[A]]} [[t′]] ∈ Nf .

Proof. By Thm. 1 we have [[t]] = [[t′]] ∈ [[[A]]] and we conclude by Lem. 6.

Calculus with Proof-Irrelevance. We extend all the definition concerning the construction of the model;

D = … ⊕ D ⊕ 𝕆 ;

the new inhabitants will be written as Prf d, and ⋆, respectively. The read-back function is extended by the equations R_{j} (Prf d) = Prf (R_{j} d) and R_{j} ⋆ = O. We add a new clause in the definition of T ,

if X = X′ ∈ T , then Prf X = Prf X′ ∈ T , and [Prf X] = {(⋆, ⋆)} .

The definitions of normalisation and expansion are extended for Prf X,

↑_{Prf X} d = ⋆  ↓_{Prf X} d = ⋆  ⇓ Prf X = Prf ⇓ X .

The semantic equations for the new constructions are

[[Prf A]]d = Prf [[A]]d  [[[a]]]d = ⋆
[[b where^{B} t]]d = ⋆  [[O]]d = ⋆ .

Remark 3. All of lemmata 5, 6, and theorems 1, and 2 are valid for the calculus with proof-irrelevance.

4 Logical relations

In order to prove soundness of our normalisation algorithm we define logical relations [24] between types and elements in the domain of T , and between terms and elements in the domain of the PER corresponding to elements of T .

Definition 10 (Logical relations). The relations Γ ⊢ A ∼ X ∈ T (ternary) and Γ ⊢ t : A ∼ d ∈ [X] are defined simultaneously by induction on X ∈ T .

– Neutral types: X ∈ Ne. • Γ ⊢ A ∼ X ∈ T iff for all Δ ⩽^{i} Γ, Δ ⊢ A p^{i} = R_{|Δ|} ⇓ X.

• Γ ⊢ t : A ∼ d ∈ [X] iff Γ ⊢ A ∼ X ∈ T , and for all Δ ⩽^{i} Γ,

Δ ⊢ t p^{i} = R_{|Δ|} ↓_{X} d : A p^{i}.

– Universe X = U.

• Γ ⊢ A ∼ U ∈ T iff Γ ⊢ A = U.

• Γ ⊢ t : A ∼ X ∈ [U] iff Γ ⊢ A = U, and Γ ⊢ t ∼ X ∈ T .

– Singletons.

• Γ ⊢ A ∼ Sing d X ∈ T iff Γ ⊢ A = {a}_{A′} for some A′, a, and Γ ⊢ a : A′ ∼ d ∈ [X].

• Γ ⊢ t : A ∼ d′ ∈ [Sing d X] iff Γ ⊢ A = {a}_{A′} for some A′, a, such that

Γ ⊢ t : A′ ∼ d ∈ [X], and Γ ⊢ A′ ∼ X ∈ T .

– Function spaces.

• Γ ⊢ A ∼ Fun X F ∈ T iff Γ ⊢ A = Fun A′ B, and Γ ⊢ A′ ∼ X ∈ T , and Δ ⊢ B (p^{i}, s) ∼ F d ∈ T for all Δ ⩽^{i} Γ and Δ ⊢ s : A′ p^{i} ∼ d ∈ [X].

• Γ ⊢ t : A ∼ f ∈ [Fun X F] iff Γ ⊢ A = Fun A′ B, Γ ⊢ A′ ∼ X, and Δ ⊢ App (t p^{i}) s : B (p^{i}, s) ∼ f · d ∈ [F d] for all Δ ⩽^{i} Γ and Δ ⊢ s : A′ p^{i} ∼ d ∈ [X].

The following lemmata show that the logical relations are preserved by judgemental equality, weakening of the judgement, and the equalities on the corresponding PERs.

Lemma 7. Let Γ ⊢ A = A′, Γ ⊢ t = t′ : A, Γ ⊢ A ∼ X ∈ T , and Γ ⊢ t : A ∼ d ∈ [X]; then Γ ⊢ A′ ∼ X ∈ T , and Γ ⊢ t′ : A′ ∼ d ∈ [X].

Lemma 8 (Monotonicity). Let Δ ⩽^{i} Γ, then

1. if Γ ⊢ A ∼ X ∈ T , then Δ ⊢ A p^{i} ∼ X ∈ T ; and

2. if Γ ⊢ t : A ∼ d ∈ [X], then Δ ⊢ t p^{i} : A p^{i} ∼ d ∈ [X].

Lemma 9. Let Γ ⊢ A ∼ X ∈ T and Γ ⊢ t : A ∼ d ∈ [X], then

1. if X = X′ ∈ T , then Γ ⊢ A ∼ X′ ∈ T ; and

2. if d = d′ ∈ [X], then Γ ⊢ t : A ∼ d′ ∈ [X].

The following lemma plays a key role in the proof of soundness. It proves that if a term is related to some element in (some PER), then it is convertible to the reification of the corresponding element in the PER of normal forms.

Lemma 10. Let Γ ⊢ A ∼ X ∈ T , Γ ⊢ t : A ∼ d ∈ [X], and k ∈ Ne, then

1. Γ ⊢ A = R_{|Γ |} ⇓ X,

2. Γ ⊢ t = R_{|Γ |} ↓_{X} d : A; and

3. if for all Δ ⩽^{i} Γ, Δ ⊢ t p^{i} = R_{|Δ|} k : A p^{i}, then Γ ⊢ t : A ∼ ↑_{X} k ∈ [X].

In order to finish the proof of soundness we have to prove that each welltyped term (and each well-formed type) is logically related to its denotation; with that aim we extend the definition of logical relations to substitutions and prove the fundamental theorem of logical relations.

Definition 11 (Logical relation for substitutions).

– Γ ⊢ σ : ⋄ ∼ d ∈ 1.

– Γ ⊢ (σ, t) : Δ.A ∼ (d, d′) ∈ ∐ X (d ↦ [F d]) iff Γ ⊢ σ : Δ ∼ d ∈ X, Γ ⊢ A σ ∼ F d ∈ T , and Γ ⊢ t : A σ ∼ d′ ∈ [F d].

After proving the counterparts of 7, 8 and 9 for substitutions, we can proceed with the proof of the main theorem of logical relations.

Theorem 3 (Fundamental theorem of logical relations). Let Δ ⊢ δ : Γ ∼ d ∈ [[Γ]].

1. If Γ ⊢ A, then Δ ⊢ A δ ∼ [[A]]d ∈ T ;

2. if Γ ⊢ t : A, then Δ ⊢ t δ : A δ ∼ [[t]]d ∈ [[[A]]d]; and

3. if Γ ⊢ γ : Θ then Δ ⊢ γ δ : Θ ∼ [[γ]]d ∈ [[Θ]].

We define for each context Γ an element ρ_{Γ} of D, that is, by construction, logically related to id_{Γ}. This environment will be used to define the normalisation function; also notice that if we instantiate Thm. 3 with ρ_{Γ}, then a well-typed term under Γ will be logically related to its denotation.

Definition 12. Let ρ_{Γ} = P_{Γ} ⊤, where P_{⋄} d = d and P_{Γ.A} d = (d′, ↑_{[[A]]d′} Var x_{|Γ |}) with d′ = P_{Γ} d. Then Γ ⊢ id_{Γ} : Γ ∼ ρ_{Γ} ∈ [[Γ]] for Γ ∈ Ctx.

Definition 13 (Normalisation algorithm). Let Γ ⊢ A, and Γ ⊢ t : A.

nbe_{Γ} (A) = R_{|Γ |} ⇓[[A]]ρ_{Γ}
nbe_{Γ}^{A}(t) = R_{|Γ |} ↓_{[[A]]ρ_{Γ}} [[t]]ρ_{Γ}

The first point of soundness is a direct consequence of Thm. 3 and Lem. 7; and the second point is obtained using Lem. 10.

Corollary 2 (Soundness of NbE). Let Γ ⊢ A, and Γ ⊢ t : A, then

1. Γ ⊢ A ∼ [[A]]ρ_{Γ} ∈ T , and Γ ⊢ t : A ∼ [[t]]ρ_{Γ} ∈ [[[A]]ρ_{Γ}]; and

2. Γ ⊢ A = nbe(A), and Γ ⊢ t = nbe(t) : A.

Remark 4. By expanding the definitions, we easily check

1. nbe_{Γ} (Fun A B) = Fun (nbe_{Γ} (A)) (nbe_{Γ.A}(B)), and

2. nbe_{Γ} ({a}_{A}) = {nbe_{Γ}^{A}(a)}_{nbe_{Γ} (A)}.

Corollary 3. If Γ ⊢ A, and Γ ⊢ A′, then we can decide Γ ⊢ A = A′. Also if Γ ⊢ t : A, and Γ ⊢ t′ : A, we can decide Γ ⊢ t = t′ : A.

Corollary 4 (Injectivity of Fun and of { } ). If Γ ⊢ Fun A B = Fun A′ B′, then Γ ⊢ A = A′, and Γ.A ⊢ B = B′. Also Γ ⊢ {t}_{A} = {t′}_{A′}, then Γ ⊢ A = A′, and Γ ⊢ t = t′ : A.

Calculus with Proof-Irrelevance. We add the corresponding cases in the definition of logical relations,

Γ ⊢ A ∼ Prf X ∈ T , iff Γ ⊢ A = Prf A′, and Γ ⊢ A′ ∼ X ∈ T ; and
Γ ⊢ t : A ∼ d ∈ [Prf X], iff Γ ⊢ A ∼ Prf X ∈ T .

Remark 5. All the lemmata 7, 8, 9, 10, theorem 3, and remarks 2, 4 are still valid. Moreover we also have nbe(Prf A) = Prf (nbe(A)).

5 Type-checking algorithm

In this section we define a bi-directional type-checking algorithm for terms in normal form, and a type-inference algorithm for neutral terms. We prove its correctness and completeness.

The algorithm is similar to previous ones [13, 3]. The only difference is due to the presence of singleton types. We deal with this by η-normalising the type, and considering first if the normalised type is a singleton (side-condition in typechecking of neutrals); in that case we check that the term is typeable with the tag of the singleton type, and that it is equal to the term of the singleton.

We stress the importance of having a normalisation function with the property stated in Rem. 4, and also to have decidability of equality. In fact, it is enough to have a function nbe( ) such that:

1. nbe({a}_{A}) = {nbe(a)}_{nbe(A)}, and nbe(Fun A B) = Fun nbe(A)nbe(B) ;

2. nbe_{Γ} (A) = nbe_{Γ} (B) if and only if Γ ⊢ A = B, and nbe_{Γ}^{A}(t) = nbe_{Γ}^{A}(t′), if and only if Γ ⊢ t = t′ : A.

In this section, let V, V′, W, v, v′, w ∈ Nf , and k ∈ Ne. We define a function to get the deepest tag of a singleton, that is essentially the same as in [8],

\overline{V} = \begin{cases}\overline{W} & if V ≡ \{w\}_{W} \\ V & otherwise. \end{cases}

The predicates for type-checking are defined mutually inductively, together with the function for inferring types.

Definition 14 (Type-checking and type-inference).

Types Γ ⇐ V. We presuppose Γ ⊢.

\overline{Γ ⇐ U} \frac{Γ ⇐ V  Γ.V ⇐ W}{Γ ⇐ Fun V W} \frac{Γ ⇐ V  Γ ⊢ v ⇐ nbe(V)}{Γ ⇐ \{v\}_{V}} \frac{Γ ⊢ k ⇐ U}{Γ ⇐ k}

Terms Γ ⊢ v ⇐ V. We presuppose Γ ⊢ V, and V in η-long normal form with respect to Γ.

\frac{Γ ⊢ V ⇐ U  Γ.V ⊢ W ⇐ U}{Γ ⊢ Fun V W ⇐ U}  \frac{Γ.V ⊢ v ⇐ W}{Γ ⊢ λv ⇐ Fun V W}

\frac{Γ ⊢ V ⇐ U  Γ ⊢ v ⇐ nbe(V)}{Γ ⊢ \{v\}_{V} ⇐ U}  \frac{Γ ⊢ v ⇐ V′  Γ ⊢ v′ = v : V′}{Γ ⊢ v ⇐ \{v′\}_{V′}}

\frac{Γ ⊢ k ⇒ V′  Γ ⊢ \overline{V′} = V}{Γ ⊢ k ⇐ V} V ≢ \{w\}_{W}

Type inference Γ ⊢ k ⇒ V. We presuppose Γ ⊢.

\overline{Γ.A_{i}…. A_{0} ⊢ q p^{i} ⇒ nbe(A_{i} p^{i+1})} \frac{Γ ⊢ k ⇒ V  Γ ⊢ \overline{V} = Fun V′ W  Γ ⊢ v ⇐ V′}{Γ ⊢ App k v ⇒ nbe(W (id, v))}

Theorem 4 (Correctness of type-checking).

1. If Γ ⇐ V, then Γ ⊢ V.

2. If Γ ⊢ v ⇐ V, then Γ ⊢ v : V.

3. If Γ ⊢ k ⇒ V, then Γ ⊢ k : V.

Proof. By simultaneous induction on the type-checking judgement.

In order to prove completeness we define a lexicographic order on pairs of terms and types, in this way we can make induction over the term, and the type.

Definition 15. Let v, v′ ∈ Nf , and A, A′ ∈ Type(Γ), then (v, A) ≺ (v′, A′) is the lexicographic order on Nf × Type(Γ). The corresponding orders are v ≺ v′ iff v is an immediate sub-term of v′; and A ≺^{Γ} A′, iff nbe(A′) ≡ {w}_{nbe(A)}.

Theorem 5 (Completeness of type-checking).

1. If Γ ⊢ V, then Γ ⇐ V.

2. If Γ ⊢ v : A, then Γ ⊢ v ⇐ nbe(A).

3. If Γ ⊢ k : A, and Γ ⊢ k ⇒ V′, then Γ ⊢ \overline{nbe(A)} = \overline{V′}.

Proof. By simultaneous induction on V, and well-founded induction on (v, A).

Calculus with Proof-Irrelevance.

Definition 16 (Type-checking and type-inference).

\frac{Γ ⇐ V}{Γ ⇐ Prf V} \frac{Γ ⊢ v ⇐ V}{Γ ⊢ [v] ⇐ Prf V} \frac{Γ ⊢ k ⇒ Prf V′  Γ.V′ ⊢ v ⇐ nbe(V p)}{Γ ⊢ v where^{V} k ⇒ Prf V}

Remark 6. Thm. 4 is still valid for the calculus with prf-tm. Moreover, Thm. 5 is valid if we add the axiom Γ ⊢ O ⇐ Prf V.

Remark 7. Type checking happens always before normalisation. If the term to type-check does not contain O, the case Γ ⊢ O ⇐ Prf V will never be reached— although occurrences of O may be created by normalisation.

Corollary 5. The type-checking algorithm is correct (by Cor. 1) and complete (by last remark) with respect to the calculus without prf-tm.

6 Conclusion

The main contributions of the paper are the definition of a correct and complete type-checking algorithm, and the simplification of the NbE algorithm for a calculus with singletons, one universe, and proof-irrelevant types. The type-checker is based on the NbE algorithm which is used to decide equality and to prove the injectivity of the type constructors. We emphasise that the type-checking algorithm is modular with respect to the normalisation algorithm. All the results can be extended to a calculus with annotated lambda abstractions, yielding a type-checking algorithm for terms not necessarily in normal forms.

The full version [5] extends this work by sigma-types and data types and an implementation of the type checker in Haskell.

References

1. Abel, A., Aehlig, K., Dybjer, P.: Normalization by evaluation for Martin-Löf type theory with one universe. In: Fiore, M., ed., Proc. of the 23rd Conf. on the Mathematical Foundations of Programming Semantics (MFPS XXIII), volume 173 of Electr. Notes in Theor. Comp. Sci. Elsevier (2007), 17–39

2. Abel, A., Coquand, T., Dybjer, P.: Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In: Proc. of the 22nd IEEE Symp. on Logic in Computer Science (LICS 2007). IEEE Computer Soc. Press (2007), 3–12

3. Abel, A., Coquand, T., Dybjer, P.: On the algebraic foundation of proof assistants for intuitionistic type theory. In: Garrigue, J., Hermenegildo, M. V., eds., Proc. of the 9th Int. Symp. on Functional and Logic Programming, FLOPS 2008, volume 4989 of Lect. Notes in Comput. Sci. Springer-Verlag (2008), 3–13

4. Abel, A., Coquand, T., Dybjer, P.: Verifying a semantic βη-conversion test for Martin-Löf type theory. volume 5133 of Lect. Notes in Comput. Sci. Springer-Verlag (2008), 29–56

5. Abel, A., Coquand, T., Pagano, M.: A modular type-checking algorithm for type theory with singleton types and proof irrelevance (full version) (2009). Available on http://www.tcs.ifi.lmu.de/˜ abel/singleton.pdf

6. Abramsky, S., Jung, A.: Handbook of Logic in Computer Science, chapter Domain Theory. Oxford University Press (1994), 1–168

7. Aehlig, K., Joachimski, F.: Operational aspects of untyped normalization by evaluation. Math. Struct. in Comput. Sci. 14 (2004) 587–611

8. Aspinall, D.: Subtyping with singleton types. In: Pacholski, L., Tiuryn, J., eds., Computer Science Logic, 8th Int. Wksh., CSL ’94, volume 933 of Lect. Notes in Comput. Sci. Springer-Verlag (1995), 1–15 9. Awodey, S., Bauer, A.: Propositions as [Types]. J. Log. Comput. 14 (2004) 447–471 10. Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed λ-

calculus. In: Proc. of the 6th IEEE Symp. on Logic in Computer Science (LICS’91). IEEE Computer Soc. Press (1991), 203–211

11. Bruijn, N. G. d.: Some extensions of Automath : the AUT-4 family (1994)

12. Cartmell, J.: Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic (1986) 32–209

13. Coquand, T.: An algorithm for type-checking dependent types. Science of Computer Programming 26 (1996) 167–177

14. Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. Fundam. Inform. 65 (2005) 113–134

15. Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic 65 (2000) 525–549

16. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proc. of the 7th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP ’02), volume 37 of SIGPLAN Notices. ACM Press (2002), 235–246

17. Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. Journal of the Association of Computing Machinery 40 (1993) 143–184

18. INRIA: The Coq Proof Assistant, Version 8.1. INRIA (2007). http://coq.inria.fr/ 19. Lee, D. K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard

ML. In: Hofmann, M., Felleisen, M., eds., Proc. of the 34th ACM Symp. on Principles of Programming Languages, POPL 2007. ACM Press (2007), 173–184

20. Maillard, O.-A.: Proof-irrelevance, strong-normalisation in Type-Theory and PER. Technical report, Chalmers Institute of Technology (2006)

21. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)

22. Martin-Löf, P.: Normalization by evaluation and by the method of computability (2004). Talk at JAIST, Japan Advanced Institute of Science and Technology, Kanazawa

23. McBride, C.: Epigram: Practical programming with dependent types. In: Vene, V., Uustalu, T., eds., 5th Int. School on Advanced Functional Programming, AFP 2004, Revised Lectures, volume 3622 of Lect. Notes in Comput. Sci. Springer-Verlag (2005), 130–170

24. Mitchell, J. C., Moggi, E.: Kripke-Style models for typed lambda calculus. In: LICS (1987), 303–314

25. Nordström, B., Petersson, K., Smith, J. M.: Programming in Martin Löf’s Type Theory: An Introduction. Clarendon Press, Oxford (1990)

26. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden (2007)

27. Shankar, N., Owre, S.: Principles and Pragmatics of Subtyping in PVS. In: WADT ’99: Selected papers from the 14th International Workshop on Recent Trends in Algebraic Development Techniques. Springer-Verlag, London, UK (2000), 37–52

28. Sozeau, M.: Subset coercions in Coq. In: Altenkirch, T., McBride, C., eds., Types for Proofs and Programs, Int. Wksh., TYPES 2006, volume 4502 of Lect. Notes in Comput. Sci. Springer-Verlag (2007), 237–252

29. Stone, C. A., Harper, R.: Extensional equivalence and singleton types. ACM Trans. Comput. Logic 7 (2006) 676–722

30. Werner, B.: On the strength of proof-irrelevant type theories. Logical Meth. in Comput. Sci. 4 (2008)