🚀 go-pugleaf

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).

I assume that languages like Miranda (TM) and ML are based on typed lambda
calculus. In Miranda the Y combinator can be written as

y f = g
      where
	 g = f g

fac = y fac1
      where
	 fac1 f x = 1, x <= 1
		  = x * (fac1 (x-1)), otherwise

In Algol68 you can also write a Y combinator. The next example is not tested,
as elas no implementation is available to me anymore:

BEGIN
    MODE M = PROC(M,INT)INT;

    PROC fac1 = (M f, INT x)INT:
    IF x <= 1
    THEN 1
    ELSE x * f(x-1)
    FI;

    PROC y = (M f, INT x)INT:
      f (f,x);
    
    print((y(fac1,5), newline))
END

(I hope this is about right, I don't have the RR handy at the moment)

>Therefore, I conclude that typed languages (such as ML)
>must not permit the kind of type-unions necessary
>for definition of self-applicative functions.

I conclude the opposite. 

>	Frank Silbermann	fs@cs.tulane.edu
>	Tulane University	New Orleans, Louisianna  USA

Ge' Weijers
University of Nijmegen, the Netherlands
--
Ge' Weijers                                    Internet/UUCP: ge@cs.kun.nl
Faculty of Mathematics and Computer Science,   (uunet.uu.net!cs.kun.nl!ge)
University of Nijmegen, Toernooiveld 1         
6525 ED Nijmegen, the Netherlands              tel. +3180652483 (UTC-2)