Implicit Recursion

To: types@theory.LCS.MIT.EDU
Subject: Implicit Recursion
From: Andrew Pitts <ap%computer-lab.cambridge.ac.uk@nss.cs.ucl.ac.uk>
Date: Tue, 14 Mar 89 14:57:42 EST
Sender: meyer@theory.LCS.MIT.EDU
Date:     Tue, 14 Mar 89 15:03:50 GMT
>Forwarding to types@theory.lcs.mit.edu from gavinw%uk.ac.sussex.syma

	IMPLICIT RECURSION IN THE POLYMORPHIC LAMBDA CALCULUS

			     Gavin Wraith
		      Department of Mathematics
			 University of Sussex

			       13/3/89





If A(X) is a type expression in poly-\ that is covariant in the
type variable X (upper case for types, lowercase for values),
then it is fairly well known that !X.(A(X)->X)->X is a weak
initial A-algebra. To be more explicit, let

           def :  I =  !X.(A(X)->X)->X

Here ! stands for A standing on its head.

def : phi = \X.\f:A(X)->X.\w:I.w X f : !X.(A(X)->X)->I->X

def : eps = \h:A(I).\X.\f:A(X)->X.f (A(phi X f) h) : A(I)->I

Then for any A-algebra f : A(T)->T we have the term
y=(phi T f) : I->T and eps;y => A(y);f.
So we can say that the 'recursive equation' eps;y=A(y);f has an
explicit (least fixed point) solution. For example
if A(X) = 1+Y*X (so that I=list(Y)) then phi=listrec.

What seems to be less well known is that, dually, we can construct
weakly terminal coalgebras, as follows:

     Def :  F = !Y.(!X.(X->A(X))->X->Y)->Y

where Y does not occur as a free type variable in A(X) and X occurs
covariantly (in fact F=EX.X*(X->A(X)) where E stands for existential
quantifier).

def : psi = \X.\f:A(X).\x:X.\Y.\h:!Z.(Z->A(Z))->Z->Y.h X f x

so that psi : !X.(X->A(X))->X->F,

def : eta = \w:F.w A(F) (\X.\f:X->A(X).\x:X.A(psi X f) (f x))

so that eta : F->A(F). Then given an A-coalgebra f:T->A(T), if we
define y = (psi T f) : T->F we get

y;eta => f;A(y)

So for example, if A(X)=X*Y (so that F=stream(Y)) we get psi=streamrec.

In summary, poly-\ already contains a lot of implicit recursion, i.e.
that which is definable by equations of the forms

           eps;y = A(y);f

or         y;eta = f;A(y)

for A( ) covariant. Explicit fixpoint (least for alg-type, greatest
for coalg-type) operations are not needed for them.

Gavin Wraith 13/3/89