Next: Judgements Up: Semantics Previous: The Computation System

## The Type System

For convenience we shall extend the relation to possibly open terms. If s or t contain free variables then does not hold; otherwise, it is true if and only if s has value t. Also, define to mean that and .

Recall that the members of a type are its canonical members and the terms which have those members as values. The integers are the canonical  members of  the type int. The denumerably many atom constants are the canonical members of the type atom. The type void is empty. The type A|B is like a disjoint union of types A and B. The terms inl(a) and inr(b) are canonical members so long as and ; a and b need not be canonical. (The operator names inl and inr are mnemonic for ``inject left'' and ``inject right''.) The canonical members of x:A#B are the terms <a,b> with and , a and b not necessarily canonical. Note that the type from which the second component is selected may depend on the value of the first component. The canonical members of the type A list represent lists of members of A. The empty list is represented by nil. A nonempty list with head a is represented by a.b, where b evaluates to a member of the type A list and represents the tail.

A term of the form t(a) is called an application of t to a, and a is called its argument. The members of x:A->B are called functions, and each canonical member is a lambda term, `\` x.b, whose application to any is a member of . It is required that applications to equal members of type A be equal. Clearly, t(a) if x:A->B and .

The significance of some constructors derives from the representation of propositions  as types. A proposition represented by a type is true if and only if the type is inhabited. The type a<b is inhabited if and only if the value of a is less than the value of b. The type (a=b in A) is inhabited if and only if . Obviously, the type (a=a in A) is inhabited if and only if , so `` a in A'' has been adopted as a notation for this type. The members of {x:A|B} are the members a of A such that is inhabited. Types of the form {x:A|B} are called set types. The set constructor provides a device for specifying subtypes; for example, {x:int|0<x} has just the positive integers as canonical members.

The members of x,y:A//B are the members of A. The difference between this type and A is equality. x,y:A//B if and only if a and are members of A and is inhabited. Types of this form are called quotient types. The relation is an equivalence relation over A in a and ; this is built into the criteria for x,y:A//B being a type.

Now consider equality  on the other types already discussed. (Recall that terms are equal in a given type if and only if they evaluate to canonical terms equal in that type. Recall also that is an equivalence relation in a and when restricted to members of A.) Members of int are equal (in int) if and only if they have the same value. The same goes for type atom. Canonical members of A|B ( x:A#B, A list) are equal if and only if they have the same outermost operator and their corresponding immediate subterms are equal (in the corresponding types). Members of x:A->B are equal if and only if their applications to any member a of A are equal in . We say equality on x:A->B is extensional . The types a<b and (a=b in A) have at most one canonical member, axiom. Equality in {x:A|B} is just the restriction of equality in A to {x:A|B}.

We must now consider the notion of functionality . A term B is type --functional in if and only if A is a type and for any a and such that . A term b is B--functional in if and only if B is type--functional in and for any a and such that . There are restrictions on type formation involving type--functionality. These can be seen in the type formation clauses of section 8.2 for x:A#B, x:A->B, and {x:A|B}. In each of these B must be type--functional in x:A. We may now say that the members of x:A->B are the lambda terms `\`x.b such that b is B--functional in . In the type x,y:A//B, that B must be type--functional in both x,y:A follows from the fact that x:A->y:A->B->B must be a type. There are also constraints on the typehood of x,y:A//B which guarantee that the relation is an equivalence  relation on members of A and respects equality in A. It should be noted that if A is empty then every term is type--functional in its free variables over A. Hence, x:void#3 is a type (with no members) even though 3 is not a type.

Equal types have the same membership and equality, but not conversely. Type   equality in

is not extensional; that is, it is not enough for type equality that two types should have the same membership and equality. In equal  canonical types always have the same outermost type constructor. The relations that must hold between the respective immediate subterms are seen easily enough in the definition of type equality given in section on page . It should be noted that in contrast to equality between types of the form x:A#B or x:A->B, much less is required for {x:A|B}= {x:A|} than type--functional equality of B and in x:A. All that is required is the existence of functions which for each evaluate to functions mapping back and forth between and . Equality between quotient types is defined similarly. If x does not occur free in B then A#B= x:A#B, A->B= x:A->B, and {A|B}= {x:A|B}; if x and y do not occur free in B then A//B= x,y:A//B. As a result there is no need for clauses in the type system description giving the criteria for A#B and the others explicitly.

Now consider the so--called universes , (k positive). The members of are types. The universes are cumulative ; that is, if j is less than k then membership and equality in are just restrictions of membership and equality in . Universe is closed under all the type--forming operations except formation of for i greater than or equal to k. Equality (hence membership) in is similar to type equality as defined previously except that equality (membership) in is required wherever type equality (typehood) was formerly required, and although all universes are types, only those Ui such that i is less than k are in . Equality in is the restriction of type equality to members of .

So far the only noncanonical  form explicitly mentioned in connection with the type system is application. We shall elaborate here on a couple of forms, and it should then be easy to see how to treat the others. The spread  form is used for computational analysis of pairs. The pair of components is spread apart so that the components can be used separately.

*
* & T is type functional in z:( x:A#B)
* & <a ,b >
* if and

Since then for some a and b where , and . Hence and have the same value, so it is enough that But from our hypotheses it follows that so it is enough that Now since x:A#B and equality respects evaluation; therefore in light of T's functionality in z: (x:A#B).

The list   induction form allows one to perform inductive analysis of lists. list_ind(e;s;x,y.t) is a function (in e) which halts on all members of A list. It is the function (in e) defined by primitive  recursion, where s is the result for the base case of e= nil (in A list) and t shows how to build the value for e= x.y (in A list) from x, y and the value of the function being defined on y, this value being passed through u during evaluation.
if
* A list
* & T is type functional in z:( A list)
* & nil
* &
* if & &

Let us prove this by induction on the length of the list represented by e, all other variables universally quantified. Suppose . By definition we know that list_ind(e;s;x,y,u.t) and s have the same value, so it is enough for the base case that ; this is true since T is functional in A list, , and . Now suppose that for some a and b, a.b , , and . Now

and

have the same value, so it is enough that the substitution into t is in . and b represents a shorter list than e; therefore, by inductive hypothesis

It follows that the substitution into t is in , so it is enough that ; this holds because of T's functionality and the equality of a.b and e (in A list).

The decide form is used to discern a left from a right injection, and to permit computation on the injected term. The ind form is used to define functions recursively on integers. The reader is referred to chapter 2 or to the exposition of the rules for further elaboration of the use of noncanonical forms.

Next: Judgements Up: Semantics Previous: The Computation System

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995