Vol.13 No.6

J. of Comput. Sci. & Technol.

Nov. 1998

Structures Definable in P o l y m o r p h i s m Fu Yuxi ( ~ g ~ ) Department of Computer Science, Shanghai .Iiao Tong University, Shanghai 200030, P.R. China Received July 19, 1996; revised November 25, 1997.

Abstract Encodings in polymorphism with finite product types are considered. These encodings are given in terms of/-algebras. They have the property that the ground terms are precisely the closed normal terms of the encoded types. The proof of a well-known result is transplanted to the setting and it is shown why weak recursion is admissible. The paper also shows how to carry out the dual encodings using the existential quantifier. K e y w o r d s : Polymorphic types, type theory.

1

Introduction

The idea of coding up some well-known free structures in the second order lambda calculus has been around for quite a long time, although the first recorded result is as late as in 1985 [21. The criterion for a successful encoding, if possible, of an algebraic structure is that it should produce a model that is isomorphic to the term model of the structure. The main result in loc.cit, is that the first order free structures can be faithfully encoded in polymorphlsm. Besides, the coding procedure is effective. Nevertheless, many questions remain unsolved in this area. The emergence of recent interest in the subject is due to the much studied relationship between polymorphism on one hand and flmctional languages on the other. Perhaps even more fascinating is the question of parametricity where one's goal is to find models in which the interpretations of the encodings are initial among the models of the corresponding structures. See [8, 19, 26] for some results on t h e topic and [13] for interpretation of inductive types in the same models. There has also been attempt to carry out similar construction in dependent calculi[4'25]. But so far there has been no good result. We are not sure to what extent this is due to our ignorance of the free structures of generalized algebras [s]. From another point of view, the coding-up technique belongs to internal type theory I1~ For such a technique to work at all, the ambient type theory must be extensional, or equivalently the basic type constructors must be functorial. A well-known example is the encoding of inductive types via W-types [T'I~]. This point is extremely important if we are designing a language that admits the introduction of new types, hence new type constructors. Then in order for the system to work properly, the user-defined types must be extensional. This is largely a summary paper about the encodings in the second order ),-calculus. But there are some improvements and generalizations. We will show how inductive types can be encoded in polymorphism via weakly initial/-algebras which are more suitable than weakly initial T-algebras (for the definition of T-algebras and its application in type theory[r'24'12]). Next we show why weak recursion is admissible in the polymorphic encodings. Finally, we transplant the proof in [2] to our setting. The dual encodings for coinductive types using existential quantifier are also studied.

2

F u n c t o r in P o l y m o r p h i s m The second order lambda calculus 5~-we use has extensional finite product types. The reasons Supported by NNSFC, grant number 69503006.

580

J. of C o m p u t . Sci. & Technol.

Vol.13

for this requirement are twofold. (1) We want simple recursion, albeit a weak one. This can be o b t a i n e d via i n d u c t i o n only if the extensional p r o d u c t types are available. (2) T h e usual encoding for inductive types has a deficiency. For example b o t h V X . X - + ( X - - + X ) - + X a n d VX.(X--~X)--+X--~X code up the type of n a t u r a l n u m b e r s N. B u t the canonical t e r m AX.,kf:X--+X.Ax:X.fx is not normal. We can do away with this problem by using product types as in V X . X x ( X - + X ) - - + X where x is the product operator. T h e abstract s y n t a x for types in our polymorphic calculus is as follows: T := 1 [ X I T--+T J T x T I VX.A, whereas t h a t for terms is t : - - , I (t, t) I rrlt I 7r2t I Ax:T.t I tt I A X . t I t(T). D e f i n i t i o n 2.1. Iso(1), the set of types isomorphic to 1, is the set defined as follows: (i) 1 E Iso(1); (ii) if B E Iso(1), then A--~B E Iso(1) for every type A; (iii) i] A e Iso(1) and B 9 Iso(1), then A x B 9 Iso(1); (iv) i] A 9 Iso(1) and X is a type variable, then VX.A 9 lso(1). D e f i n i t i o n 2.2. For each A E Iso(1), the associated canonical representative !A is defined inductively as follows: (i) !1 is *; (ii) !A• is (!A, !B); (iii) !A-*B is )~x:A.!B; (iv) !VX.A is AX.!A. L e m r n a 2.3. Let P ( X ) be a type in 3v with free variables among X 1 , . . . , X,~ such that P ( f ) 9 Iso(1). Then every term of P ( 1 , . . . , 1), not necessarily closed, is equal to the canonical representative !P(1,...,1) of type P ( 1 , . . . , 1). D e f i n i t i o n 2.4. -,~ is the notion of reduction consisting of the standard extensional reduction

rules together with the following: a

!* .x~

(!A,Tr2c) 5

!A

c

(~1c, !B> ",.* q e ~x:A.M(!A)

if a : A and A 9 Iso(1) and a is not !A, if c: A x B and A 9 Iso(1), if c : A x B and B 9

n* M ",-+

if A 9 Iso(1).

As usual, -,-** will denote the reflexive, transitive a n d compatible closure of ",-*; a n d ----will mean the equality relation generated by -,~* [1l. T h e following result is taken from [6, 5]. T h e o r e m 2.5. -,-** is confluent and effectively weakly normalizing. So the normal form of a

second order .k-term is unique and can be effectively found out. In Section 6 we will use existential quantification to code up coinductive types. First let's refresh our m e m o r y on the rules a b o u t 3-types:

PHp:P(A) Intro F F - t : ~ X . P ( X ) F , x : P ( X ) ~ - q : C Elirn F F- 6(n,p): 3X.P(X) F t- E(t,(X,x).q): C F}-p:P(A) P,x:P(X)~-q:C F~-t:3X.P(X) r,z:3X.P(X)~-q:C P I- E(6(A, p), (X, x).q) = q[A/X, p/x]: C F }- E(t, (X, x).q[6(X, x)/z]) = q[t/z] : C T h e i n t u i t i o n of the above rules is as follows. T h e introduction rule says t h a t to prove 3 X . P ( X ) one must find a t y p e A and a proof of P(A). T h e elimination rule describes the reverse inference: if we know a proof of 3 X . P ( X ) a n d can prove C when assuming a proof of P ( X ) ( X must not occur in C), t h e n we can prove C without m a k i n g the assumption. These are the t y p e theoretical formulation of t h e corresponding rules of the second order logic (2s]. As for the r e d u c t i o n rules, the first is clearly t h e c o m p u t a t i o n a l rule [14], the second is the extensionality rule [19]. T h e existential types have b e e n used to model abstract d a t a types [24]. Suppose f : A--~B, g : B-+C a n d h : A-+D. g o f will denote the t e r m Ax:A.g(f(x)) whereas (f, h) will s t a n d for the term Ax:A.(fx, hx). We say a t y p e variable X is positive (negative) in a type expression F ( X ) if (i) F ( X ) is a constant type or (ii) Z is positive (negative) in b o t h F I ( X ) and F~(X) when F ( X ) = F I ( X ) x F ~ ( X ) or (iii) X is negative (positive) in F I ( X ) a n d positive (negative) in F2(X) when F ( X ) = FI(X)--+F~(X) or (iv) X is positive (negative) in G ( X , Y ) when F ( X ) = VY.G(X, Y). Here it does not m a t t e r whether Y is positive or negative in G(X, Y). A positive or negative type constructor in a nond e p e n d e n t t y p e d calculus can be regarded as a functor on the category of terms a n d contexts. Such functors are p u t to effective use in [28, 24, 11] to code up inductive a n d coinductive d a t a types in polymorphism. T h e technique used here is closely related to the encodings of pure free varieties as carefully studied in [2], confer also [14].

No.6

Structures Definable in Polymorphism

581

Let C be the category whose objects are dosed types. A morphism from A to B is the equivalence class of closed terms f : A--+B. The opposite category of C will be denoted by C ~ Suppose F ( X 1 , . . . ,X,~) is a type expression in .T. Then F defines a functor from C*x ... xC* to C. The i-th component of C* x .-. x C* is C if Xi is positive in F ( ) ( ) and is C ~ if Xi is negative in F ( X ) . The term F()~) defines the object part of a functor. The morphism part F ( ) f ) ~ of the functor should be a term of type

F(,~) ~ : V.X.VY.MI-+ . . . ---+M,,--~ F( X )-.-+F (]7) where Mi is either Xi--+]~ or Y~--~Xi depending on whether Xi is positive or negative in F ( ) ( ) . By abuse of notation, we will write X - + Y for M I - + . . . - + M , ~ and Af : X--+Y for ,kfl:M1...',kf,~:M,~. Notice that F ( ) ( ) ~ depends on the choice of ~'. For instance, if F contains three free type variables X, Y and Z, t h e n F ( X , Y)~ is different from F(Y, Z) ~ Having said that, we will however leave out the variables X in F ( X ) ~ when there is no confusion. We now define F ~ inductively on the structure of F(Jf) (we omit the negative case): 9 F(.~) = A, a constant type. F ~ clefA.X.A~'.,kff:.X--+~'..~a:A.a.

9 F()() = Xi. F ~ de=fAX.A~'.,,~f:X-+Y.AxI:Xi.fixi. 9 F()~) = FI()~)x " - •

Let

F ~ ~-~fAX.A~'.Af:.X--~Y'..kh:FI(.~)x... xF,~(..~).((F~.XYf(Trlh),..., F,~.X~'f(~',~h)). 9 F(X) = FI(-~)-+F2()~). By induction hypothesis, we define

FO d~=fAX.A'Y.A f:X---~ Y.),h:FI (..Y)--+F2(.X)..ky:FI (~').F~.,~'Y f ( h( F~'Y X fy) ). 9 F(ff~) = VZ.G(.X, Z). F ~ de_fA.X.AY.)~f:X--+Y.)~h:VZ.G(.X, Z).AZ.G(..~)~

In this definition, Z is treated as a constant in G(X)% Occasionally, we write F ~ F~ ~ The extensional rules are essential to the functoriality of F ~

3

Inductive Type in Polymorphism

There are two ways to have inductive types in polymorphism. One is to postulate rules for these types in ~-. This external approach is adopted in [20, 16, 17, 21]. The other approach is to internally code up the inductive types in 5v. Take the type of natural numbers for example. In the former approach, we introduce a type N together with introduction, elimination and equality rules. The equality rule says that

R e c ( I , x + 1) = i(x, R e c ( f , 2)) holds for any term of type N. But in the latter approach, the previous equality holds only for closed terms of N. Section 4 explains why. The internal method is weaker but by no means less interesting. In [16, i7] the author studies a categorical language based on the following construction (and its dual) that generates new data types. Let P ( X ) be an n-tuple [ P t ( X ) , - - - , P,,(X)] where Z is positive in P I ( X ) , ' " , P~,(X). We may declare a new type as follows:

~ X . P ( X ) --sum X with constructors inl : PI(X)------+X; in,, : P,,(X)----+X end. The reason we call it a sum-construction is that, categorically, the meaning of a /z-type is best captured by requiring the functor [P1 (X)] + . . . + [P,, (X)] to be initial, where [P1 ( Z ) ] , . . . , [P~ (X)] are interpretations of P I ( X ) , . . . , P,~(X) on a suitable category. This is done in [28] by coding up

582

J. of C o m p u t . Sci. & Technol.

Vol.13

the corresponding initial T-algebras. O u r view is t h a t the I-algebras i n t r o d u c e d in [22] are most suitable to the description of the encodings of Hagino's categorical d a t a types. T h e d a t a types tree a n d ]orest are defined in terms of each other. T h a t is a n example of m u t u a l l y d e p e n d e n t inductive d a t a types. In the following example we generalize Hagino's n o t a t i o n in a straightforward way. Example 3.1. T h e d a t a types of trees a n d forests are defined as follows: (T, F) = s u m (X1, X2) w i t h c o n s t r u c t o r s s p a n : A• j o i n : X1 xX2---+X2, empty

: 1---+X2

end. It says t h a t a tree consists of a root and a forest; a forest is either e m p t y or a tree together with a forest. T h e structural recursion enjoys three equations:

Itr F ( e m p t y ) =cl (*), I t r f (join(t, I ) ) =c~ ( l t r T ( t), Itr F (y) ),

Xtrr(sp~n(~, I)) =c~(~, I t r F ( f ) ) The i n t u i t i o n should be clear. D e f i n i t i o n 3.2. Suppose we have a group of covariant functors

[3

F ~ j ( X i , - . . , X , ) : Cix . . . x C , - - - + C j , where 1 < i < n and 1 <_ j ~_ n~. A n / " - a l g e b r a is a tuple ( ( ; z l , . . . , ~ , ) , I n i , i , ' "

,In . . . . ) where

In~,j : F ~ , ~ ( ~ I , - - - , ~ ) - - + ~ for all possible i and j . A n initial I-algebra is such that if ((C~, . . - , C,,), ci,1, " " , c~,,~,) is any other I-algebra, then there is a unique tuple (lzl ~-~ C i , - " , l z , ~ ~

C,,) such that

e, d o F ~ ( I t r i , - . - , Itr,,) = ttri o tn~j

for all possible i , j . I f we drop the uniqueness requirement, we get a weakly initial I-algebra. Now suppose Pij(-X'),. for 1 < i < n a n d 1 _~ j < n l , are type constructors with positive type variables. We define/~i and I n i j as follows:

~'(.~) ~ f (P~,~ ( 2 ) ~ x i ) x . . . • (P~.,,~ ( . g ) ~ z ~ ) x.-- x (P,,,~ ( ~ ) ~ x , , ) x . . . x (P,,,,,, (.~)~x,,),

m-~.'P(~) ~*' v.2.p(2)~x. i

def

--

-

-

eta = A X . A p : 7 9 ( X ) . A w i : l a i . w i X p : VX.P(X)--+I..q-->XI,

t,i,.i d.=~A t : p i j ( f i ) . a ~ . A p : 7 ~ ( j ~ ) . ( r i , i p ) ( 7 ~ j f i ~ ( , ~ 2 p ) . . .

(,,~)~p)t) : Pij(/~X.~(X))-+/~-~.'P(-~).

Proposition

3.3. ((pi," - ' , ~,~), [ h i , i , ' . . , In . . . . ) is a weakly initial I-algebra. Proof. Let ( ( C 1 , ' - ' , C,~), c L i , ' " , c . . . . ) be a n o t h e r l-algebra. We define

Itri a,j e~,C(cl,1 . - - c . . . . ) = Aw~:/~i.wiC(cl,1--- c~,,,,) : ~ - + C ~ for i ~ { 1 . - - n } . It is easy to see t h a t Itr~ o [n~,~ =c~,~ o P ~ , i ( I t r ~ , . . . , Itr~) holds. Example 3.4. C o n t i n u i n g the example of trees a n d forests, we see t h a t P(X, Y) =(A xY-+X) x (1--+Y) x (X x Y-~Y), T =VX.YY.P(X, Y)--+X,

F =VX.~r'.7~(X, Y)-+Y, span(a, I) =AX.AY.Ap:P( X, Y).(,q )(a, f XVp),

O

No.6

583

Structures Definable in Polymorphism

empty =AX.A Y.Ap:TP(X, Y).(#r2)(*), join(t, f) =AX.AY.Ap:TP( X, Y).(zr3)(/ X Y p , f X Y p ) . Suppose ((C~, C2), c~, c2, c3) is another/-algebra.

ItrT(span(a, f ) ) =c3(a, fC~ Ce(cx, c~_,ca)), ItrF( e m p t y ) =c~(*),

t t r F(join( t, f ) ) =ce ( tCz C2 ( cz , c~, c~), f C~ C~ ( cz , c~, ca>). {:1

They are exactly what one would expect.

4

Weak

Recursion

Let N be the type of natural numbers and C an arbitrary type. Given closed terms c : C and f : N x C - - + C the recursion defined by c and f is a term Rec(c, f ) : N - + C satisfying

nec(c, :)(0) = c,

(1)

Rec(c, f ) ( s u c c ( n ) ) = f ( n , Rec(c, f ) ( n ) ) ,

(2)

where (2) holds for all terms of type N (for instance a variable of type N). This is the type theoretical formulation of recursion in Peano arithmetic. But the polymorphic encoding verifies only a weak form of recursion. The rest of this section is devoted to an abstract account of this fact. Suppose X 1 , . . . , X ~ are all positive in P i j for i , j . Let t l , . . . , t , , be closed terms of types /zl,.. -, #,, respectively. We have P ~ j ( A x : l . t t , . . . , Ax:l.t~) : P i j ( f ) - + P , j ( f i ) . By abuse of notation we will write P ~ d ( t l , . . . , t~) instead. The equation in the proof of Proposition 3.3 implies

ttr, o In,,j o Pg~(t~,---, t~) = c,,j o P~AI~r~(t~),--., t~r~(t~)). D e f i n i t i o n 4.1. Suppose P i j ( f ) E I s o ( 1 ) for all possible i , j . A term t : t~ is said to be a canonical term of type t~i if it is (i) I n i j ( * ) when P i j ( ~ : ) --- 1 or (ii) I m d ( P ~ . i ( t l , " " ,t,)!p(f)) where 1p(f) is the canonical representative of type P i j (1) and tl, -. . , t,, are canonical terms. Clearly canonical terms are closed. Suppose we have terms fi,j : P~.i (#1 x C , , . . . , / ~ , , x C,~)-+Ci for all possible i and j. Then

((,1 xC1,-..,/z,,, x C,.,), (P~,, (~); Im.j., ft,1),...,

(P:.,., (~); In .....

f,., .,.,,., ))

is a n / - a l g e b r a . By Proposition 3.3 one hem, for each i E { 1 , . . . , n}, a morphism (?{, Reck) : #~ /zi x Ci such that

P~j((%, a e ~ ) , . . . ,

(?~, Reck)); (P~j(~); In,.j, Y,.A = r,,,~ ; (?,, aec,),

(3)

We can define a weak form of recursion by extracting the second component of the iterators in (3). It is the consequence of the weakness of the initiality that we cannot prove ?i ----I d ~ for any i E { 1 , . . . ,n}. So we only have Rec, o In, j = fi,~ o P ~ ( ( ? l , R e c t ) , . - . , (?,,Rec,,)), which is not quite what we would like to have, however a weak form of recursion does hold. P r o p o s i t i o n 4.2. Suppose P~,j(1) e I s o ( l ) for all possible i and j . Then Rec~ o Inqj o P~j ( S t , . - . , t,,) = f i j o P~ Recl ( t x ) ) , . . . , (t,,, Rec,,(t,,))) if t l , . . , t,, are all canonical terms of types lzl , 99 9 #,, respectively. Proof. Notice that ?~ o In~j -- In~,j o P~j ( ? ~ , . . . , ?~) by projecting out the first component of (3). Notice also that ff P~j(fi) is 1, (3) becomes ?~(In~j(*)) -- Ini,j(*). It follows that for a canonical term ti : / ~ i ,

?i (tl) =?'i (Ini,j (P~j (s I , ' " ") sa )!Pi,i (I))) = Ifll,3 (P~)J (? 1 ( S l ) ) ' " ) ?7%(sa))!Pi ,j (i)) . . . .

584

J. of C o m p u t . Sci. & Technol.

= I n i d ( " ' , ?l(Int,q(*))," ") = Ini,j(..., lnl,q(*),...) . . . . .

Vo1.13

In, o (P~,~ (Sl, 9

.

o

.

.

.

.

, s n ) . p i j ( l ) ) = ti. !

.

Now by definition (?,, Rec,) o (A~:l.ti) = A x : l . ( ? i t i , Reci(ti)} for i e { 1 , . . . , n}. Therefore Recl o Inid o p~o ( t l , . " , t~) = fi,j o p~O,j((?1, R e c x } , . . . , (?~, R e c k ) ) o p~oj ( t l , - . - , t,~) = f,,~ o PiO~((?a (t~), R e c k ( h ) ) , . . . ,

= lid o P~~

(?,(t, 0, Rec,(t~)))

R e c k ( t O ) , . . . , (t~, Recn(t,,))).

This completes the proof. In the case of first order free pure structures, the above equation looks much more familiar:

~ec,(~n,,~(t~,..., t~)) = f,,~(t~, ~ec~(tO,. W h e n applying this result to the encoding given in Example 39 the b e g i n n i n g of this section.

5

First

Order

Free

, t~, ~ec~(t~)) we get what we have described at

Structure

A first order signature contains no higher order functions like f : (sl--+s2)x s--~s. By "pure" we m e a n there is no equational theory. Now fix a first order finite signature Sig = (sl, . . . , s,,, f ~ l , ' - ", f,~,,,), where flj : s q x ... x s i ~-+si; its free structure (term model) can be perfectly coded by a weakly m m a l / - a l g e b r a in polymorphism. Notme t h a t m fij : sq x -.. x si,,.--+si, the subscript m j depends on 3. We will nevertheless omit j m m j for simplicity and let the dependence be implicit. T h r o u g h o u t this section we fix, for each pair i , j , P i d ( X ) = Xi~ x -.- x X i , , . It is easily verified t h a t P~~d = A X . A Y . A f : X - + Y . A h : X i z • • Xim. (fin (Trlh),.--, f i ~ (Tr,~h)). Therefore 9

.

o

~ )

9

9

.

9

9

"

J

Inid = At:Pi,j(lz).AX.Ap:'P( )~).(Iri,jp)(ep XpOrl t), . . . , eT~ Xp(zrmt)} = At:Pi,j (Iz).A.X.Ap:TP(X).(ri,jp)((lrlt)ff~p,.--, (Tr,~t))(p). Consequently Ini,j (*) = A~'.Ap:TP(X).(Tri.jp)* a n d rni,~(t~,..., t,~) =

h)?.~p:~()?).(~,jp)(t~:?p,..., t,,~p) = I~,j(P~j(t~ ..... t,~)!e,.j(f~),

where t l , - - ' , t,~ are canonical terms of t y p e s / z l , - - - , / ~ , ~ respectively. This corresponds precisely to the so-called A-programmes in [2]. T h e only difference is t h a t here we use p r o d u c t types. In ioc.cit., elements in a free structure are represented by equivalence classes of A-terms; here they are coded by the uniformly constructed ground terms. For this encoding to work, p r o d u c t types are necessary. L e m m a 5.4 would fail if the only logical operators we use are V a n d --+. To see this, consider again t h e afore-mentioned encoding V X . ( X - - ~ X ) - + X - ~ X of n a t u r a l numbers. The ground terms are A X . A f : X - ~ t X . A z : X . f " x . But A X . ) ~ f : X - + X . A z : X . f x is not normal. D e f i n i t i o n 5.1. A term of type lz~ is a ground term / f ( i ) it is A)( Ap 7)(X).(rri,jp)* when Pi,j (.~) -- 1 or (ii) it is h 2 . ~ p : 7 : ' ( ~ ) . ( ~ , , j v ) ( t ~ ( 2 , p ) , . . . , t , ~ ( X , p ) ) when ~r,,~p is of type m , • • I-ti.~ -'+#i and AX.Ap:'P ()~').tl ()(, p), - 9 9 A X . A p : ~ ( X ) . t m (.~, p) are ground terms of types , i x , . . . , Izi~ respectively. By induction, one can easily show t h a t g r o u n d terms are closed a n d normal. L e r m - n a 5.2. The canonical terms of Izi are in bijective correspondence with the ground terms olin. P r o p o s i t i o n 5.3. There are one-to-one correspondences between 1. the set { s l , . . . , s ~ } of sorts and the set { # x , . . . , P ~ } ; 2. the set of function symbols fi,j and the set of terms Inid; 3. the set of elements of sort sl in the free structure and the set of canonical terms of type I~. L e m m a 5.4. The closed normal terms of V)(.79(P~)--+Xi are precisely the ground terms. Proof. The proof is adopted from [2]. Let s :/zi be a closed normal term. T h e n s m u s t be of the form A.~.)~p:79(X).t(.~,p). We are going to work out the structure of t(P~,p) where p is a variable of type 7~()~). We first introduce the n o t i o n of degrees. Suppose A is a type. T h e degree of A is (i) 0 if A is either a c o n s t a n t type or a type variable (ii) the m a x i m u m of the degrees of its components

No.6

S t r u c t u r e s D e f i n a b l e in P o l y m o r p h i s m

585

w h e n A is a p r o d u c t t y p e (iii) 1 + m a x { t h e d e g r e e o f A l , t h e d e g r e e o f A2} w h e n A = A1--+A~ (iv) l§ d e g r e e o f B ( X ) w h e n A = V X . B ( X ) . T h e d e g r e e o f a n o b j e c t is t h e d e g r e e of its t y p e . I n t h e f o l l o w i n g p r o o f , we do n o t r e g a r d a t y p e v a r i a b l e as a s u b t e r m .

1. t(X,p) must be .normal and the only variables it contains are X 1 , . . . , Xn and p. 2. t(ff~,p) cannot be of introduction form as Xi, the t y p e of t(.X,p), is a type variable. 3. tf s is a s u b t e r m of t(3~,p) and is abstraction-free, i.e. s contains neither A nor )~, t h e n the degree of s is at most one. We now prove this fact by induction on the s t r u c t u r e of. s. Clearly s m u s t be either * whose degree is 0, or p whose degree is 1, or a tuple, or ~rst or s l s 2 . In t h e third and fourth cases we resort to the induction hypothesis. The degree of sis2 m u s t be zero as by induction hypothesis the degree of s l is no more t h a n 1. 4. t()~,p) does not contain any abstraction. S u p p o s e otherwise. Take the left-most such s u b t e r m t J. In view of 1 and 2, t I can only be a s u b t e r m of an application f l . t l or a c o m p o n e n t of a tuple t ' . T h e former case is impossible because by hypothesis fl is abstraction-free and therefore by 3 the degree of f~ is less t h a n 1. In the latter case, t " c a n n o t occur in 7rt~, nor can it occur in any abstraction because t r is the left-most such term. t " cannot occur in g-t u because of 3. T h e only case left is t h a t t u is a c o m p o n e n t of a n o t h e r tuple. But then we can repeat the a r g u m e n t to show t h a t is impossible. 5. It follows from 3 and 4 t h a t t(P(,p) does not contain any s u b t e r m with degree more t h a n 1. 6. If .f.a is a s u b t e r m of t ( . ~ , p ) , then f must be either 7rp or p and therefore the type of f.a is a variable. ~Ve prove this by s t r u c t u r a l induction: (i) f is a variable, t h e n it can only be p; (ii) f cannot be an application because of 5; (iii) f cannot be an a b s t r a c t i o n due to 4; (iv) f is lrb. T h e r e are these cases: (a) b c a n n o t be an application because by induction hypothesis the t y p e of b would be a variable; (b) b c a n n o t be a tuple by 1; (c) b cannot be 7rtbI because by induction hypothesis on 7, 7r~bp is of an arrow type; (d) b m u s t be p. 7. If ~ra is a s u b t e r m of t(.~, p), then it m u s t be rcp a n d therefore of an arrow type. T h i s can be proved as follows: (i) a c a n n o t be an application by induction hypothesis on 6; (ii) it c a n n o t be rr~a' by induction hypothesis; (iii) nor can it be a tuple by 1; (iv) therefore it m u s t be p. Notice t h a t cases 6 and 7 are proved by simultaneous induction. 8. From 4, 6 and 7, we can infer t h a t if a s u b t e r m of t ( ~ ' , p ) has a p r o d u c t type of degree zero, then it m u s t be a tuple. 9. We conclude t h a t t ( ~ , p ) m u s t be f.a. By 6, f m u s t be 7rp or p. So the t y p e of a is either 1 or Xil • 999 • Xi,~ (say) or a type variable. In the first case a = * as f . a is in n o r m a l form. In the second case, we infer from 8 t h a t a m u s t be a tuple (tiz," "", tim >. But t h e n AP~..kp:79(.~).tij : VX.79()~)-+Xij for j = 1, - 9-, rn and we can repeat the whole a r g u m e n t for each ti~. T h e third case is simpler t h a n the second case. So t n m s t Theorem

be a g r o u n d term. 5 . 5 . For each i E { 1 , . . . , n } ,

O

let S N ( # , ) denote the set of closed normal terms of type t~. The structure ( S N ( p ~ ) , . . . , S N ( ~ , ) , In11,..., In~,~) is isomorphic to the free structure of Sig. Proof. T h e r e s u l t n o w follows f r o m L e m m a 5.2, P r o p o s i t i o n 5.3 a n d L e m m a 5.4. T h e t h e o r e m c a n n o t b e e x t e n d e d t o h i g h e r o r d e r c a s e s for a t l e a s t t w o r e a s o n s : (i) t h e m e t h o d c a n n o t c o p e w i t h c a s e s w h e r e a s o r t is n e g a t i v e as in f : (s-+s)--+s; (ii) e v e n t h o u g h we p r e t e n d we c a n t r e a t n e g a t i v e a p p e a r a n c e , o u r m e t h o d p r o d u c e s m o r e t e r m s t h a n w a n t e d . F o r i n s t a n c e , s u p p o s e we h a v e a s i g n a t u r e Sig = (sl, s2, fo : sl, f l : s l - - + s l , f2 : ( s l - + s l ) - - ~ s 2 ) . L e t #1, #2 a n d I n d e n o t e r e s p e c t i v e l y t h e e n c o d i n g s o f s l , s2 a n d f~ in ~'. T h e n [n(Ax:l~l.x) d o e s n o t c o r r e s p o n d t o a n y e l e m e n t in t h e free s t r u c t u r e of Sig.

6

Coinductive Type in Polymorphism

T h e c o i n d u c t i v e t y p e s a r e n o t a s f a m i l i a r as t h e i n d u c t i v e o n e s . T h e p u r p o s e o f t h i s s e c t i o n is t o c a r r y o u t t h e c o n s t r u c t i o n s d u a l t o t h e o n e s g i v e n in S e c t i o n 3. H a g i n o ' s d u a l c o n s t r u c t i o n is this:

~X.Q(X) = p r o d u c t X w i t h d e s t r u c t o r s out1 :

X---+QI(X);

586

J. of Comput. Sci. & Technol.

Vol.13

out~ : X--+Q,,(X) end. Again we require that X is positive in all Q~(X) for i - 1 , . - - , n . Now the natural thing to do to code the above construction in polymorphism is to explore the duality of 3 and V. In [28], the author uses the representation of 3 by V. So a kind of 'double encoding' is present. In this paper we code coinductive types by S directly. The encodings are:

Q(2) %f (xi-+Ql~(2))x-.. x(X~-+Ql~,(~7))x .-.

x(X.~Q.~(.7))x..,

x(X~-+Q~. (2)),

,,,~7.e(2) %~s2.Q(2)xX,, i

def

AX.Aq:Q(X).Ax:Xi.5(X1,5(X2,

. ,5(Xn, ( q , x } ) - . . ) ) : V X . Q ( X ) - - ~ X I - + u , X . Q ( X ) ,

otltlj def " . At:v~X.Q(X).E(t; . . (X,q).Qi~XvO?~X(~r~q)) . ~ "~ 1

(rl~X(v:~q))(~r,j(~hq)(~r2q))) : v,--eQ~(vi). '~ "

o ~ (,~X( 1 ~ 7r ~ q ) ) . . - ( ' ~ ( ~ l q ) ) ( ~ ( ~ l ~ ) ( ~ q ) ) Abbreviate Q,~X to ~ , and the right hand side of the

last definition stands for E(t, (X1, t l ) . E ( t l , (X2, t 2 ) . " - E ( t ~ _ ~ , ( X ~ , q ) . r by the following derivations.

t,~-I :~X,~.Q(X)•

Q(.X)xX.i 1- r

: Qij(yi)

t,,_~ : 3x,,_l~x,,.~(2)xx~, t~_~ : ~ x ~ . ~ ( ~ ) x X ~ t.-2 : 3X._13X..Q(2)xx~

which is obtained

~ ~(t~_~, ( x ~ , q).r e E ( t . - 2 , (X~_~, t . - 1 ) . E ( t . - 1 , ( X . , q).r

: Q~(~) : Q~(~)

t : 3X~ . . . . 3X..Q(:f)xX~, h : 3X2...-3X~.Q()~)xX~ ~ E(tl, (X2, t2).--. E ( t . _ ~ , ( X . , q).r t : ~ e E(t, (Xl, t 0 . E ( t l , (X2, t2) . . . . E ( t . - i , ( X . , q).r ")) : Q~j(~) P r o p o s i t i o n 6.1. ((Vl)~.Q(3~),...,v~X.Q(X)), outll,...,out,~,,,) algebra. Proof9 Given a n / - a l g e b r a <(D1,..., D , ) , d l t , . . . , d ~ , > . Let

9.)

is a weakly terminal I-

CoItr, ~ f Ax:D,.5(DI, 5(D2 . . . . ,5(D,~, ((dl~ .... , d,,,.), x ) ) . . . ) ) . It"is easy to show that CoItrq o u t i j = d~.j; Q~j(CoItr) ~ holds for all possible i and j . Example 6.2. The data type of streams is defined as follows:

[]

Stream(A) = p r o d u c t X with destructors head : X---+A; tail : X---+X end. It corresponds to the following type and terms in bY:

vX.Q(X) %f 3X.(X--+A)x(X-+X)•

t~il(~) ~ E(~, (X, q).~(X, <~q, ~(~lq)(~2q)))). One should compare this example to the encoding via V. [] We should mention that these dual encodings are far less satisfactory than those in the inductive case. It remains to be seen if they axe of any use.

No.6

Structures Definable in P o l y m o r p h i s m

587

References [1] Barendregt H. The Lambda Calculus--Its Syntax and Semantics. volume 103 of Studies in Logics. North-Holland, 1984. [2] BShm C, Berarducci A. Automatic synthesis of typed A-program on term algebras. TheoreLical Computer Science, 1985, 39: 135-154. [3] Cartmell J. Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic, 1986, 32: 209-243. [4] Coquand T, Huet G. Constructions: A higher order proof system for mechanizing mathematics. In EUROCAL85, LNCS203, 1985, pp.151-184, Springer-Verlag. [5] Di Cosmo R. Isomorphisms of Types. PhD thesis, Dipartimento di Informatica, Universits di Pisa, 1993. [6] Curien P-L, Di Cosmo R. A confluent reduction system for the A-calculus with subjective pairing and terminal object. In ICALP'91, Leach, Monien, and Artalejo (eds.), pp.291-302, Springer-Verlag. [7] Dybjer P. Inductively defined sets in Martin-L6f's set theory. In Proceedings of the Workshop on General Logic, Edinburgh, 1988. ECS-LFCS-88-52. [8] Freyd P. POLYNAT in PER. In Categories in Computer Science and Logic, Gray J and Scedrov A (eds.), June 1989, pp.67-68, Boulder, A.M.S. [9] Fu Y. Some semantic issues in type theory. PhD thesis, Department of Computer Science, University of Manchester, May 1992. [10] Fu Y. Understanding inductive types in constructions. Technical Report UMCS-93-6-5, Department of Computer Science, University of Manchester, June 1993. [11] Fu Y. Recursive models of general inductive types. Fundamenta Informaticae, 1996, 26: 115-131. [12] Fu Y. Categorical properties of logical frameworks. Mathematical Structures in Computer Science, 1997, 7: 1-47. [13] Fu Y. Constructive sets in computable sets. Journal of Computer Science and Technology, 1997, 12: 425-440. [14] Girard J, Lafont Y, Taylor P. Proofs and Types. Volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. [15] Goguen H, Luo Z. Inductive data types: Well-ordering types revisited. Technical report, LFCS, University of Edinburgh, April 1992. [16] Hagino T. A Categorical programming language. PhD thesis, LFCS, University of Edinburgh, 1987. [17] Hagino T. A typed lambda calculus with categorical type constructions. In Category Theory and Computer Science, Pitt D, Poign~ A, Rydeheard D (eds.), LNCS 283, 1987, pp.140-157, Springer-Verlag. [18] Hyland J, Pitts A. The theory of constructions: Categorical semantics and topos-theoretic models. In Categories in Computer Science and Logic, Gray J and Scedrov A (eds.), June 1989, pp.137-199, Boulder, A.M.S. [19] Hyland M, Robinson E, Rosolini G. Algebraic types in per models. In Mathematical Foundations of Programming Semantics, Main M e t al. (eds.), LNCS 442, 1990, pp.333-350, Springer-Verlag. [20] Mendler N. Inductive definition in type theory. PhD thesis, Cornell University, 1987. [21] Mendler N. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 1991, 51: 159--172. [22] Mendler N. Predicative type universes and primitive recursion. In Proceedings of the Sixth Symposium on Logic in Computer Science, IEEE Computer Science Press, July 1991, pp.173-184. [23] Mitchell J, Plotkin G. Abstract types have existential type. In ACM TOPLAS, 1988, pp.470-502. [24] Ore C. The extended calculus of constructions (ECC) with inductive types. Information and Computation~ August 1992, 99: 231-264. [25] Pfenning F, Paulin-Mohring C. Inductively defined types in the calculus of constructions. In Mathematical Foundations of Programming Semantics, Main M et al. (eds.), LNCS442, 1991, pp.209-228. Springer-Verlag. [26] Phoa W. Two results on set-theoretic polymorphism. In Category Theory and Computer Science, Pitt D, Curien P e t al. (eds.), LNCS 530, September 1991, pp.219-235, Paris, Springer-Verlag. [27] Prawitz D. Natural Deduction. Almqvist and Wiksetl, 1965[28] Wraith G. A note on categorical datatypes. In Category Theory and Computer Science, Pitt D, Rydeheard D et al. (eds.), LNCS 389, September 1989, pp.21~-223, Manchester, Springer-Verlag. For the biography of F u Y u x i please refer to P.208, No.3, Vo1.13 of this Journal.