🚀 go-pugleaf

In <2531@wn1.sci.kun.nl> ge@wn3.sci.kun.nl (Ge' Weijers) writes:

>fs@caesar.cs.tulane.edu (Frank Silbermann) writes:

>>C) I've never seen a programming language
>>   based on typed lambda calculus whose typechecking system
>>   permits the user to define a fixpoint combinator
>>   out of more primitive elements.  The type signature
>>   of the necessary lambda expression cannot be written
>>   as a finite combination of the primitive types
>>   (so Y-combinators must be added as primitives).

The self application  (g g)  in Y=\G.(\g.G(g g))(\g.G(g g))
requires a recursive type g:T where T=T->...
You can program Y in SML: "cut the knot" with a constructor.

You program the recursive version of Y in Pascal!
but not the "proper" one as `function' is outside the type system.

The following works in Algol 68:

( # Fixed-Pt Operator, Y, in Algol-68     L.Allison UWA 15/7/85 #

 MODE  INTFN = PROC( INT )INT;

 MODE  RECFF = PROC( RECFF, INT ) INT;

 MODE  FFORM = PROC( INTFN, INT ) INT;

#------------------------------------------------------------------------#
 PROC y = ( FFORM f, INT n ) INT:
  ( RECFF h = ( RECFF g, INT n ) INT:
     ( INTFN b = ( INT n ) INT:
	  g( g, n );

       f( b, n )
     );

    h( h, n )
 );


 FFORM big f = ( INTFN little f, INT n ) INT:
    IF n=0 THEN 1 ELSE n * little f(n-1) FI;


 INTFN usual factorial = (INT n) INT:
    IF n=0 THEN 1 ELSE n * usual factorial(n-1) FI;

 INTFN unusual factorial = (INT n) INT:
    big f( usual factorial, n);

 INTFN odd factorial = (INT n) INT:
    y( big f, n );

#-----------------------------------------------------------------------#

 FOR i TO 5 DO
    print(( usual factorial(i), unusual factorial(i),
	    odd factorial(i), newline ))
 OD
)