--* From postmaster%watson.vnet.ibm.com@yktvmv.watson.ibm.com  Thu Dec  9 09:22:07 1993
--* Received: from yktvmv.watson.ibm.com by leonardo.watson.ibm.com (AIX 3.2/UCB 5.64/4.03)
--*           id AA13302; Thu, 9 Dec 1993 09:22:07 -0500
--* X-External-Networks: yes
--* Received: from watson.vnet.ibm.com by yktvmv.watson.ibm.com (IBM VM SMTP V2R3)
--*    with BSMTP id 9949; Thu, 09 Dec 93 09:28:28 EST
--* Received: from YKTVMV by watson.vnet.ibm.com with "VAGENT.V1.0"
--*           id <A.SANTAS.NOTE.YKTVMV.4571.Dec.09.09:28:27.-0500>
--*           for asbugs@watson; Thu, 09 Dec 93 09:28:28 -0500
--* Received: from bernina.ethz.ch by watson.ibm.com (IBM VM SMTP V2R3) with TCP;
--*    Thu, 09 Dec 93 09:28:26 EST
--* Received: from neptune by bernina.ethz.ch with SMTP inbound id <7348-0@bernina.ethz.ch>; Thu, 9 Dec 1993 15:28:16 +0100
--* From: Philip Santas <santas@inf.ethz.ch>
--* Received: from rutishauser.inf.ethz.ch (rutishauser-gw.inf.ethz.ch) by neptune id AA04043; Thu, 9 Dec 93 15:28:11 +0100
--* Date: Thu, 9 Dec 93 15:28:09 +0100
--* Message-Id: <9312091428.AA22434@rutishauser.inf.ethz.ch>
--* Received: from vinci.inf.ethz.ch.rutishauser by rutishauser.inf.ethz.ch id AA22434; Thu, 9 Dec 93 15:28:09 +0100
--* To: asbugs@watson.ibm.com
--* Subject: another version of Y.as which does not compile||run
--* Cc: bronstei, jenks@watson.ibm.com

--@ Fixed  by:  PI   Mon Apr 25 20:50:45 EDT 1994 
--@ Tested by:  none 
--@ Summary:    No more a bug. SSD fixed bug535, and now also bug536 is running. 


--Another version of Y.as which
--(a) does not compile in A# version 33.0 for SPARC (debug version)
--(b) compiles in A# version 32.6 for AIX RS/6000 (debug version)
--    but does not run (reports: function not found)!

--Philip

------------------------------------------------
#include "aslib.as"
SI ==> SingleInteger

Ycomb(S:Type, T:Type): with
     y: ((S->T) -> (S->T)) -> (S->T)
  == add
     YType (Z:Type): with
          yt: (% -> Z) -> %
          ty: % -> (% -> Z)
       == add
           Rep ==> %->Z
           import from Rep
           yt(x: %->Z): % == per x
           ty(x: %): %->Z == rep x

     import from YType(S->T)
     y(f:(S->T)->(S->T)): S->T ==
         --((x:YType(S->T)):(S->T) +-> f ((a:S):T +-> (ty x).x.a))
         --(yt ((x:YType(S->T)):(S->T) +-> f ((a:S):T +-> (ty x).x.a)))
         f1(x:YType(S->T)):(S->T) == f ((a:S):T +-> (ty x).x.a)
         f1(yt f1)


-- example: factorials, fibonacci without recursion:

import from SI
import from Ycomb(SI,SI)

fact(recur:SI->SI)(n:SI):SI ==
      n=0 => 1
      n * recur(n-1)