MSFP 2008

A Partial Type Checking Algorithm for Type : Type

Andreas Abel^{1 ,3}

Institut für Informatik, Ludwigs-Maximilians-Universität München Oettingenstr. 67, D-80538 München

Thorsten Altenkirch^{1 ,2 ,4}

School of Computer Science, The University of Nottingham Nottingham, NG8 1BB, UK

Abstract We analyze a partial type checking algorithm for the inconsistent domain-free pure type system Type:Type (λ∗). We show that the algorithm is sound and partially complete using a coinductive specification of algorithmic equality. This entails that the algorithm will only diverge due to the presence of diverging computations, in particular it will terminate for all typeable terms. Keywords: Dependent Types, Pure Type Systems, Type Checking, Type:Type

1 Introduction

In this paper, we analyze and implement a partial type checking algorithm for the inconsistent theory Type:Type (λ∗) similar to the one presented in [6]. This is an instance of a domain-free pure type system [4] and it seems possible to extend it to any functional pure type system (PTS). The motivation for this work is to implement type checkers for dependently typed programming languages which support general recursion such as Augustsson’s Cayenne [3]. We use Type:Type as a test case for a language with dependent types avoiding the syntactic complexity of a full programming language.

Our main contribution is that we show soundness and partial completeness. By partial completeness we mean that if the algorithm diverges, it will do only because the program or its type, or their combination, contains some loop; divergence

1 Research supported by the coordination action TYPES (510996). 2 Research supported by EPSRC grant Observational Equality For Dependently Typed Programming (EP/C512022/1)

3 andreas.abel@ifi.lmu.de
4 txa@cs.nott.ac.uk

This paper is electronically published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

Abel, Altenkirch

because of an error in the algorithm is excluded. Hence, for a given PTS it is sufficient to establish termination to show that the algorithm is complete and does indeed decide the typing relation. We believe that this is a promising approach, because it means we can establish basic syntactic properties of the typing algorithm independently of termination.

In particular, we give algorithmic typing rules Γ ⊢ t ⇇ A, read in context Γ, term t checks against type A, in two versions: Γ ⊢^{μ} t ⇇ A, using inductive equality, and Γ ⊢^{ν} t ⇇ A, using coinductive equality. The inductive version of the algorithm is shown sound, whereas the coinductive version is proven complete.

We present the algorithm for Type:Type (type is a type) with type equality by untyped β-conversion =_{β}. Our proofs crucially rely on the injectivity of the function type constructor Πx: A. B which is a consequence of confluence of β-reduction in our case.

The type checking algorithm computes weak head normal forms (whnf) of types. This is sufficient, because β-reduction is standardizing. Standardization can be subsumed by the slogan if a term β-reduces to a whnf, then weak head reduction reaches a whnf of the same shape. For instance, if t ⟶_{β}^{∗} λxu, then t ⟶_{w}^{∗} λxu′ with u′ ⟶_{β}^{∗} u. With confluence, this becomes: if t =_{β}^{∗} λxu, then t ⟶_{w}^{∗} λxu′ with u′ =_{β}^{∗} u.

Related work.

The algorithm presented here is basically a modern reimplementation of Coquand’s algorithm [6], see also [7], but the study of partial completeness using coinduction is new. The fact that we consider only β-equality simplifies the treatment — a syntactic study of βη-equality along the lines of [9,8] is left for future work. The recent work by the first author [1] is also directed at βη-equality but relies on normalization.

Overview.

We start by presenting Type:Type and verifying some basic properties. Next we specify the type checking algorithm in relational form and show soundness of the inductive type checking relation. The completeness of the coinductive relation is then established using coinduction. Finally we present an implementation of the algorithm in Haskell and discuss further extensions of the present work.

2 Type:Type

The Curry-style λ^{∗} is a domain free pure type system [5] with just one sort Type, axiom Type :Type and rule (Type,Type,Type).

Syntax.

As usual for pure type systems, there is only one grammatical class Expression for terms t, u, types A, B, C, and sorts s. Metavariable x ranges over a countably infinite set of variable identifiers.

Exp ∋ t, u, A, B, C, s ::= x | λxt | t u | Πx:A. B |Type expressions
Ne ∋ n  ::= x | n u  neutral terms
Cxt ∋ Γ  ::= ⋄ | Γ, x:A  typing contexts

We identify expressions up to α-conversion. A context Γ is just a list of pairs x:A, but it is also considered a finite map from variables to types. Hence, no variable may be assigned two types in a context.

Capture-avoiding substitution of u for x in t is written t[u/x]. One-step βreduction is denoted by ⟶_{β}, its reflexive-transitive closure by ⟶_{β}^{∗} and its reflexivetransitive-symmetric closure by =_{β}. By confluence, t =_{β} t′ if and only if there is some u with t ⟶_{β}^{∗} u and t′ ⟶_{β}^{∗} u. Weak head reduction is given by the rule

(λxt) u u_{1} … u_{n} ⟶_{w} t[u/x] u_{1} … u_{n}

for n ⩾ 0. Its reflexive-transitive closure is written ⟶_{w}^{∗}. (Typeable) whnfs are neutral terms n, abstractions λxt, function types Πx:A. B, and the constant Type. In the following we employ a vector notation and write t u_{1} … u_{n} simply as t u.

Proposition 2.1 (Standardization of β-reduction [11])

(i) If t ⟶_{β}^{∗} x u′ then t ⟶_{w}^{∗} x u and u ⟶_{β}^{∗} u′. (ii) If t ⟶_{β}^{∗} λxu′ then t ⟶_{w}^{∗} λxu and u ⟶_{β}^{∗} u′. (iii) If C ⟶_{β}^{∗} Πx:A′. B′ then C ⟶_{w}^{∗} Πx:A. B and A ⟶_{β}^{∗} A′ and B ⟶_{β}^{∗} B′. (iv) If C ⟶_{β}^{∗} Type then C ⟶_{w}^{∗} Type.

Using confluence, ⟶_{β}^{∗} can be replaced by =_{β} in the above statements. In particular, we can derive the following corollary from confluence:

Corollary 2.2 (Injectivity of Π) If Πx: A. B =_{β} Πx: A′. B′ then A =_{β} A′ and B =_{β} B′.

Inference rules of λ∗.

The terms t of type A are given by the judgement Γ ⊢ t : A which is mutually defined with the judgement Γ ⊢ ok for well-formed contexts. If J is a judgement, we write D :: J to express that D is a derivation of J.

Well-formed contexts Γ ⊢ ok.

cxt-empty \overline{⋄ ⊢ ok}  cxt-ext \frac{Γ ⊢ A :Type}{Γ, x:A ⊢ ok}

Typing Γ ⊢ t : A.

type-f \frac{Γ ⊢ ok}{Γ ⊢Type :Type}  fun-f \frac{Γ, x:A ⊢ B :Type}{Γ ⊢ Πx:A. B :Type}

hyp \frac{Γ ⊢ ok  (x:A) ∈ Γ}{Γ ⊢ x : A}  fun-i \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λxt : Πx:A. B}

fun-e \frac{Γ ⊢ t : Πx:A. B  Γ ⊢ u : A}{Γ ⊢ t u : B[u/x]}  conv \frac{Γ ⊢ t : A  A =_{β} B}{Γ ⊢ t : B}

The judgement Γ ⊢ t : A implies Γ ⊢ ok, which is easy to check.

The following inversion lemma is independent of injectivity.

Lemma 2.3 (Inversion of Typing) (i) If D :: Γ ⊢Type : C then C =_{β} Type. (ii) If D :: Γ ⊢ Πx:A. B : C then C =_{β} Type and Γ, x:A ⊢ B :Type. (iii) If D :: Γ ⊢ x : C then C =_{β} Γ(x). (iv) If D :: Γ ⊢ λxt : C then C =_{β} Πx:A. B and Γ, x:A ⊢ t : B.

(v) If D :: Γ ⊢ t u : C then Γ ⊢ t : Πx:A. B with Γ ⊢ u : A and C =_{β} B[u/x].

Proof. By induction on D.  □  □

Typing enjoys the usual properties of weakening, substitution, and subject reduction for β. The proofs are standard.

3 A Type-Checking Algorithm

The most elementary format of a strongly typed functional program is a list of non-recursive declarations of the form x : A = t, meaning identifier x of type A is defined as term t. In a list of declarations, later declarations may rely on the type and definition of previously declared identifiers. It is reasonable to assume that both t and A are free of β-redexes, however, during type-checking redexes will occur in types.

We use a bidirectional representation of algorithmic type checking, using Γ ⊢ t ⇉ A to denote that the type A of t can be inferred and Γ ⊢ t ⇇ A that t can be checked to have type A.

A program is type checked by first ensuring that A is a well-formed type, written Γ ⊢ A ⇉ Type, then checking that t is of type A, written Γ ⊢ t ⇇ A, adding the declaration x : A = t to the global environment and proceeding with the next declaration.

Type inference

Γ ⊢ t ⇉ A. (Input: Γ well-formed, t neutral and β-normal. Output: A with Γ ⊢ t : A.)

inf-var \overline{Γ ⊢ x ⇉ Γ(x)}

inf-fun-e \frac{Γ ⊢ t ⇉ C  C ⟶_{w}^{∗} Πx:A. B  Γ ⊢ u ⇇ A}{Γ ⊢ t u ⇉ B[u/x]}

inf-type

Γ ⊢Type ⇉Type

inf-fun-f \frac{Γ ⊢ A ⇉ s  s ⟶_{w}^{∗} Type  Γ, x:A ⊢ B ⇉ s′  s′ ⟶_{w}^{∗} Type}{Γ ⊢ Πx:A. B ⇉Type}

Type inference diverges for applications t u when the inferred type of t has no whnf. We don’t specify here that the result of type inference has to be a whnf, even though we will use whnfs in the implementation. Indeed, any inferred type will have to be reduced to a whnf when it is used anyway.

Type checking Γ ⊢ t ⇇ A. (Input: Γ, A with Γ ⊢ A :Type, t β-normal. Output: none.)

chk-inf \frac{Γ ⊢ t ⇉ A ⊢ A ∼ A′}{Γ ⊢ t ⇇ A′} t not a λ

chk-fun-i \frac{C ⟶_{w}^{∗} Πx:A. B  Γ, x:A ⊢ t ⇇ B}{Γ ⊢ λxt ⇇ C}

Rule chk-red is applied when we want to check an abstraction against a type which is not yet in whnf. Checking against a type which has no whnf diverges.

Algorithmic equality

⊢ A ∼ A′. If the type of a term t is declared as A′ but inferred as A (rule chk-inf), we need to ensure that A and A′ are β-equal. The following rules specify an algorithm which alternates weak head normalization (aq-red-l and aq-red-r) and structural comparison (the other rules).

aq-red-l \frac{t_{1} ⟶_{w} t′_{1}  ⊢ t′_{1} ∼ t_{2}}{⊢ t_{1} ∼ t_{2}}  aq-red-r \frac{t_{2} ⟶_{w} t′_{2}  ⊢ t_{1} ∼ t′_{2}}{⊢ t_{1} ∼ t_{2}}

aq-var \overline{⊢ x ∼ x}  aq-app \frac{⊢ n ∼ n′  ⊢ u ∼ u′}{⊢ n u ∼ n′ u′}  aq-λ \frac{⊢ t ∼ t′}{⊢ λxt ∼ λxt′}

aq-type \overline{⊢Type ∼Type}  aq-fun \frac{⊢ A ∼ A′  ⊢ B ∼ B′}{⊢ Πx:A. B ∼ Πx:A′. B′}

4 Soundness

A terminating run of the type checker corresponds to a finite derivation in the system of algorithmic rules presented above. Hence, when we want to reason that the algorithm is sound, i. e., that it only accepts well-typed terms, we need to consider inductive algorithmic equality ⊢^{μ} t ∼ t′ and algorithmic typing Γ ⊢^{μ} t ⇇/⇉ A which refers to inductive equality.

Lemma 4.1 (Soundness of algorithmic equality) D :: ⊢^{μ} t ∼ t′ implies t =_{β} t′.

Proof. Trivially by induction on D.  □  □

Theorem 4.2 (Soundness of bidirectional type checking) (i) If D :: Γ ⊢^{μ}

t ⇉ A and Γ ⊢ ok then Γ ⊢ t : A. (ii) If D :: Γ ⊢^{μ} t ⇇ C and Γ ⊢ C :Type, then Γ ⊢ t : C.

Proof. Simultaneously by induction on D. Likewise trivial.  □  □

5 Completeness

Since type-checking of λ∗ is undecidable, an appropriate completeness result for our algorithm would be: if β-normal t is of type A, checking t against A does not fail finitely. I. e., the algorithm might diverge or succeed, but not report an error. We make this formal by considering the coinductive version of algorithmic equality ⊢^{ν} t ∼ t′, i. e., we allow infinite derivations, and a version of algorithmic typing Γ ⊢^{ν} t ⇇/⇉ A which refers to coinductive equality. In the following we prove, using the technique of coinduction [10], that finite derivations of typing and equality in the declarative system (of Section 2) map to possibly infinite derivations in the algorithmic system (of Section 3).

First we show that if two terms t_{1} and t_{2} are β-equal, then D :: ⊢^{ν} t_{1} ∼ t_{2}. In case t_{1} ≡ Ω := (λx. x x) (λx. x x), the derivation D is simply an infinite repetition of aq-red-l. Note that the same derivation shows ⊢^{ν} Ω ∼ t for an arbitrary term t, hence, the contraposition of the following lemma cannot hold:

Lemma 5.1 (Completeness of algorithmic equality) If t_{1} =_{β} t_{2} then ⊢^{ν} t_{1} ∼ t_{2}.

Proof. By coinduction. We consider the following cases:

• Case t_{1} ⟶_{w} t′_{1}. Then ⊢^{ν} t_{1} ∼ t_{2} follows by rule aq-red-l using coinductive hypothesis ⊢^{ν} t′_{1} ∼ t_{2}.

• Case t_{2} ⟶_{w} t′_{2}. Analogously.

In the remaining cases, t_{1} and t_{2} are whnfs.

• Case t_{1} ≡Type =_{β} t_{2}. By confluence, t_{2} ⟶_{β}^{∗} Type. Since t_{2} is a whnf, t_{2} ≡Type. The goal follows by aq-type.

• Case t_{1} ≡ Πx: A_{1}. B_{1} =_{β} t_{2}. By confluence, t_{2} ≡ Πx: A_{2}. B_{2} with A_{1} =_{β} A_{2} and B_{1} =_{β} B_{2}. The goal follows by aq-fun with coinductive hypotheses ⊢^{ν} A_{1} ∼ A_{2} and ⊢^{ν} B_{1} ∼ B_{2}.

The other cases are proven analogously.  □  □

Next we show that for a well-typed and checkable (i. e., β-normal) term t there is an algorithmic typing derivation with possibly infinite derivations of algorithmic equality.

Theorem 5.2 (Completeness of type checking) Let t β-normal and Γ ⊢ t : C.

(i) If t is neutral then Γ ⊢^{ν} t ⇉ A and A =_{β} C. (ii) In any case, Γ ⊢^{ν} t ⇇ C.

Proof. Simultaneously by induction on t.

• Case t ≡ x. By inversion C =_{β} Γ(x). We have Γ ⊢^{ν} x ⇉ Γ(x) by inf-var. The second goal follows since by Lemma 5.1 ⊢^{ν} Γ(x) ∼ C.

• Case t ≡ n u. By inversion, Γ ⊢ n : Πx: A. B with Γ ⊢ u : A and C =_{β} B[u/x]. By induction hypothesis, Γ ⊢^{ν} n ⇉ D with D =_{β} Πx : A. B. By confluence and standardization, D ⟶_{w}^{∗} Πx : A′. B′ with A =_{β} A′ and B =_{β} B′. Since by the conversion rule, Γ ⊢ u : A′ we have by second induction hypothesis Γ ⊢^{ν} u ⇇ A′, hence, by inf-fun-e we can conclude Γ ⊢^{ν} n u ⇉ B′[u/x] with B′[u/x] =_{β} B[u/x] =_{β} C. This implies the second goal Γ ⊢^{ν} t ⇇ C.

• Case t ≡Type. By inversion C =_{β} Type. We conclude by inf-type.

• Case t ≡ Πx:A. B. By inversion, C =_{β} Type and Γ, x:A ⊢ B :Type which implies Γ ⊢ A : Type. By the first induction hypothesis we have Γ ⊢^{ν} A ⇉ s with s =_{β} Type. By second induction hypothesis, Γ, x: A ⊢^{ν} B : s′ with s′ =_{β} Type. Since by confluence and standardization s ⟶_{w}^{∗} Type and s′ ⟶_{w}^{∗} Type, we conclude by inf-fun-f.

• Case t ≡ λxt′. By inversion, C =_{β} Πx : A. B and Γ, x : A ⊢ t′ : B. Since C ⟶_{w}^{∗} Πx: A′. B′ with A =_{β} A′ and B =_{β} B′, we have Γ, x: A′ ⊢ t′ : B′. By induction hypothesis Γ, x:A′ ⊢ t′ ⇇ B′ and we conclude by chk-fun-i. □

□

Completeness leads to the following important corollary which shows that the only reason that the algorithm will reject a typeable term is non-termination:

Corollary 5.3 Let t β-normal and Γ ⊢ t : C but Γ ⊬^{μ} t ⇇ C. Then a subterm of t has an inferred or ascribed type which is not strongly normalizing.

Proof. From 5.2 we know that D :: Γ ⊢^{ν} t ⇇ C. Since ⊢ and ⊢^{ν} differ only in the equality check, there must be types A and A′ with an infinite derivation of ⊢^{ν} A ∼ A′ contained in D. This derivation must contain infinitely many applications of aq-red-l or aq-red-r, thus, A or A′ is not strongly normalizing. □

6 Haskell Implementation

In the following, we present a Haskell implementation of our type checking algorithm for λ∗. We choose an efficient implementation of substitution and weak head reduction through closures. In the end, it is very similar to Coquand’s algorithm [6], however, we distinguish closures and weak head normal forms through different data types, making some invariants explicit this way. Also, we explicitly use monads, and this in an abstract way that makes the implementation extensible, e. g., to universe inference.

We use monads for handling of errors and lookup in the typing context, which is implemented by finite maps.

module TypeType where
import Control.Monad.Error
import Control.Monad.Reader

import Data.Map (Map)

import qualified Data.Map as Map

Syntax

as parsed from a file is represented by abstract syntax trees of (Haskell) type Exp. Variables are referred to by Name. We maintain the invariant that function types appear only in the form Pi a (Abs x b).

type Name = String
data Exp
= Var Name
| Abs Name Exp
| App Exp Exp
| Pi Exp Exp
| Type
deriving Show

arr a b = Pi a (Abs "_" b)

Values and environments.

Evaluation is lazy, so values are closures Clos t rho, pairs of an expression t and an environment rho. When type checking the body of an Abstraction, the free variable is mapped a unique Id, called a generic value Gen by Coquand [6]. Thus, the environment component rho may map variable names either to generic values or to closures in turn. The (Haskell) type e of environments is passed as a parameter to Val, since we do not want to commit to a particular representation of environments here.

type Id = Int

data Show e ⇒ Val e

= Gen Id
| Clos Exp e
deriving Show

type Ty e = Val e

The weak head normal form (whnf) of a closure might either be an introduction, WType, WPi, or WAbs, or an elimination of a generic value, WNe, i.e., an identifier applied to several closures. Evaluation does not step under binders, thus, the whnf of a function closure Clos (Abs x t) rho is simply WAbs x t rho.

data Show e ⇒ Whnf e

= WNe Id [Val e ] -- reversed list of arguments
| WAbs Name Exp e
| WPi (Val e) (Val e)
| WType
deriving Show

type WTy e = Whnf e

Environments, which map names to values, are left abstract. We specify them via the type class Env, providing operations for construction (emptyEnv and extEnv, extension) and query (lookupEnv).

class Show e ⇒ Env e where

emptyEnv :: e
extEnv :: Name → Val e → e → e
lookupEnv :: e → Name → Val e

Evaluation and application.

whnf computes the weak head normal form of a value, by removing the weak head β-redexes. There are two cases of values: generic values Gen, which are already weak head normal, and closures, which we normalize using the auxiliary function whnf′.

whnf :: Env e ⇒ Val e → Whnf e

whnf (Gen i)  = WNe i [ ]
whnf (Clos t rho) = whnf′ t rho

whnf′ computes the whnf of an expression in an environment rho. The value of variables Var x is looked up in the environment. The result might be a closure which has to be evaluated recursively. Or, it might be a generic value, in case x has become free by stepping under its binder. Applications are the source of redexes, which are resolved lazily (cbn), using function app. Expressions of the other shapes, Abs, Pi, and Type, are already whnfs.

whnf′ :: Env e ⇒ Exp → e → Whnf e

whnf′ (Var x) rho = whnf (lookupEnv rho x)
whnf′ (App t u) rho = app (whnf′ t rho) (Clos u rho)
whnf′ (Abs x t) rho = WAbs x t rho
whnf′ (Pi a b) rho = WPi (Clos a rho) (Clos b rho)
whnf′ Type  rho = WType

app applies a whnf to a closure, reducing the result to a whnf. The function part can only be neutral or an abstraction, other cases are impossible since ill-typed.

app :: Env e ⇒ Whnf e → Val e → Whnf e

app (WNe i vs)  v = WNe i (v : vs)
app (WAbs x t rho) v = whnf′ t (extEnv x v rho)

A context for type checking.

We hide the context in a monad of class MonadCxt. The context provides both a type and a value for each name. bind extends the context with both type and value. new extends it with the given type, creating a new generic value. new′ creates just a generic value, in situations where its type does not matter.

The type of a name can be queried by typeOf , and expression can be closed in the context which acts like an environment in this case (this is the only way we need to refer to the values of names).

class (Env e, Monad m) ⇒ MonadCxt e m | m → e where

bind :: Name → Ty e → Val e → m a → m a
new :: Name → Ty e → (Val e → m a) → m a
new′ :: Name → (Val e → m a) → m a

new′ x = new x dontCare

typeOf :: Name → m (Ty e)
close :: Exp → m (Val e)

    dontCare = error "Internal error: no type assigned to variable"

Bidirectional type checking.

infer t infers the type of expression t, returning it in whnf. Inferable are all expressions shapes except abstractions.

For a variable, the type is looked up in the context and then weak head normalized. This does not introduce unnecessary divergence, since an inferred type needs always to be converted to weak head normal form, either to check whether it is a function type (see case App), or to compare it to another type (see eq below). Note however, that types in the context are not in weak head normal form. Normalizing them before adding them to the context would indeed introduce unnecessary divergence, e.g., for unused variables of diverging type.

infer :: MonadCxt e m ⇒ Exp → m (WTy e)

infer (Var x) = typeOf x >>= return ∘ whnf
infer (App t u) = do w ← infer t

case w of

WPi v f → do check u v

u′ ← close u

return (whnf f ‘app‘ u′)

→ fail ("expected " ++ show t ++

                            " to be of function type")

infer Type  = return WType
infer (Pi a b) = do check′ a WType

v ← close (a ‘arr‘ Type)

check b v

return WType

check t v checks expression t against type value v by converting the type to weak head normal form and calling check′. check′ treats only abstractions Abs x t, which must be of function type Pi v f , and their body t must type check in the context extended by x whose type is v and whose value is set to a new generic value i. The type of non-abstractions t is inferred as w′ and compared to the ascribed type w.

check :: MonadCxt e m ⇒ Exp → Ty e → m () check t v = check′ t (whnf v) check′ :: MonadCxt e m ⇒ Exp → WTy e → m ()

check′ (Abs x t) (WPi v f ) = new x v (λi → check′ t (whnf f ‘app‘ i))
check′ (Abs x t) w  = fail ("expected " ++ show w ++

                             " to be a function type")

check′ t  w  = do w′ ← infer t

eq w′ w

Equality checking

of values. We define three mutually recursive functions, each returning a monadic boolean m (). eq operates on whnfs, eq′ on arbitrary closures, eqs compares lists of closures of the same length. Two function closures WAbs are tested for equality by applying them to a new generic value i.

eq :: MonadCxt e m ⇒ Whnf e → Whnf e → m ()

eq WType WType = return ()
eq (WPi a b) (WPi a′ b′)  = eq′ a a′ >> eq′ b b′
eq v@(WAbs{ }) v′@(WAbs x ) = new′ x (λi → eq (v ‘app‘ i) (v′ ‘app‘ i))
eq (WNe i vs) (WNe i′ vs′) | i ≡ i′ = eqs vs vs′

eq w w′ = fail ("equality check fails for " ++ show w ++

" and " ++ show w′)

eq′ :: MonadCxt e m ⇒ Val e → Val e → m () eq′ v v′ = eq (whnf v) (whnf v′) eqs :: MonadCxt e m ⇒ [Val e ] → [Val e ] → m ()

eqs [ ] [ ] = return ()
eqs (v : vs) (v′ : vs′) = eq′ v v′ >> eqs vs vs′

eqs vs vs′ = fail ("equality check fails: " ++

              "argument vectors of different lengths")

Declarations.

Input to the type checker are declarations of the form x : A = t meaning name x has type A and definition t. The type checker will first ensure that A is a wellformed type, evaluate it (lazily), then check t against the value of A, and finally bind x to type value of A and the value of t in the current environment. Then it will go on to the next declaration.

data Decl = Decl{name :: Name, ty :: Exp, value :: Exp } deriving Show checkDecl :: MonadCxt e m ⇒ Decl → m (Ty e, Val e) checkDecl (Decl x a t) = do

check′ a WType

v ← close a

check t v

w ← close t

return (v, w) type Decls = [Decl ] checkDecls :: MonadCxt e m ⇒ Decls → m () checkDecls [ ] = return () checkDecls (d : ds) = do

(a, v) ← checkDecl d

bind (name d) a v (checkDecls ds)

An implementation of contexts.

We implement contexts as finite maps from names to their type and value. They also handle the generation of fresh identifiers. To this end, the next unused generic value is store in field nextFree. cxtLookup just retrieves the type of a name, cxtExt just binds a type to a name, and cxtBind binds both type and value to a name.

data Cxt = Cxt{nextFree :: Int

, cxt :: Map Name (Ty Cxt, Val Cxt)}

deriving Show

cxtLookup :: Monad m ⇒ Cxt → Name → m (Ty Cxt) cxtLookup gamma x = case Map.lookup x (cxt gamma) of

Just (a, v) → return a

  Nothing → fail ("identifier not in scope: " ++ x)

cxtEmpty :: Cxt

cxtEmpty = Cxt 0 Map.empty cxtExt :: Name → Ty Cxt → Cxt → Cxt cxtExt x a (Cxt n gamma) = Cxt (n + 1) (Map.insert x (a, Gen n) gamma) cxtBind :: Name → Ty Cxt → Val Cxt → Cxt → Cxt cxtBind x a v gamma = gamma{cxt = Map.insert x (a, v) (cxt gamma)}

Contexts can be seen as environments, since they provide a value for each name.

instance Env Cxt where
emptyEnv = cxtEmpty

extEnv x v rho = rho{cxt = Map.insert x (dontCare, v) (cxt rho)} lookupEnv rho x | Just (a, v) ← Map.lookup x (cxt rho) = v

Implementation of the type checking monad.

During type checking, we need to query the context and we need to raise errors. The type checking monad wraps a reader monad ReaderT Cxt (see module Control.Monad.Reader) around an error monad Either String. The implementation of the MonadCxt operations access the context through the MonadReader operation ask and modify it through local. The Reader Monad here is only used to hide the plumbing used in a standard implementation of static binding. In particular shadowing of variables is implemented by replacing the previous definition.

type TC = ReaderT Cxt (Either String)

instance MonadCxt Cxt TC where
typeOf x = do gamma ← ask

cxtLookup gamma x

close t  = do rho ← ask

return (Clos t rho)

new x a f = do gamma ← ask

local (cxtExt x a) (f (Gen (nextFree gamma)))

bind x a v c = local (cxtBind x a v) c

The implementation of the main type checking loop uses the reader monad to type check a sequence of declarations.

checkFile :: Decls → IO ()

checkFile ds = case (checkDecls ds ‘runReaderT ‘ cxtEmpty) of

      Right () → putStrLn "Type checking succeeded"
      Left s → putStrLn ("Type checking error: " ++ s)

Acknowledgment.

The Haskell code has been typeset by lhs2TeX (Andres Löh and Ralf Hinze).

7 Conclusion

We have presented a correct partial type checking algorithm for λ∗ which has nonnormalizing types. It should be possible to extend the algorithm for functional PTS by annotating types with sorts—however, there is a known issue with the abstraction rule which needs to be investigated (see [12]).

We have shown that the algorithm will only fail because of the presence of diverging terms during type checking (Corollary 5.3). This does not mean that the algorithm could not be improved, e.g., it could check for syntactic equality before normalizing terms. However, in practice we are interested in type checking in a normalizing fragment of the theory anyway. Indeed, for a given PTS we only have to show normalization to be able to conclude that our algorithm decides the typing relation. Thus, apart from being applicable for non-terminating type systems our paper also suggests a new way of showing decidability of terminating type theories: as in this paper, one can prove partial correctness of type checking, and then show normalization separately which entails decidability of type checking.

The proof presented here should be also extensible to languages with explicit recursion and additional features to model dependent data types, e.g., we plan to apply it to ΠΣ, a core language for dependently typed programming [2].

Another line of research would be to extend our approach to λ∗ with βη-equality using a type-sensitive implementation of the equality checker. The problem is that the separation of equality checking and type checking does not work anymore— however, we conjecture that such an algorithm would still be sound and partially complete.

References

[1] Abel, A., T. Coquand and P. Dybjer, Verifying a semantic βη-conversion test for Martin-Löf type theory, in: Mathematics of Program Construction, MPC’08, 2008, to appear.

[2] Altenkirch, T. and N. Oury, ΠΣ: A core language for dependently typed programming (2008), draft, available on http://www.cs.nott.ac.uk/˜ txa/publ/.

[3] Augustsson, L., Cayenne - a language with dependent types, in: Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA, September 27-29, 1998, SIGPLAN Notices 34 (1999), pp. 239–250.

[4] Barthe, G. and T. Coquand, Remarks on the equational theory of non-normalizing pure type systems, Journal of Functional Programming 16 (2006), pp. 137–155.

[5] Barthe, G. and M. H. Sørensen, Domain-free pure type systems, J. Funct. Program. 10 (2000), pp. 417– 452.

[6] Coquand, T., An algorithm for type-checking dependent types, in: Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17–21, 1995, Kloster Irsee, Germany), Science of Computer Programming 26 (1996), pp. 167–177.

[7] Coquand, T. and M. Takeyama, An implementation of Type : Type, in: P. Callaghan, Z. Luo, J. McKinna and R. Pollack, editors, Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, Lecture Notes in Computer Science 2277 (2000), pp. 53–62.

[8] Goguen, H., “A Typed Operational Semantics for Type Theory,” Ph.D. thesis, University of Edinburgh (1994), available as LFCS Report ECS-LFCS-94-304.

[9] Goguen, H., Justifying algorithms for βη conversion, in: V. Sassone, editor, Foundations of Software Science and Computational Structures, 8th International Conference, FoSSaCS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, Lecture Notes in Computer Science 3441 (2005), pp. 410–424.

[10] Gordon, A., A tutorial on co-induction and functional programming, in: Functional Programming, Glasgow 1994 (1995), pp. 78–95.

[11] Plotkin, G., Call-by-name, call-by-value, and the λ-calculus, Theoretical Computer Science 1 (1975), pp. 125–159.

[12] Pollack, R., “The Theory of LEGO,” Ph.D. thesis, University of Edinburgh (1994).