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

Actually, you _can_ define a fixpoint combinator in Standard ML, in a purely
functional way, without using recursion.

----------------------------------------------------------------------------
(* Defining a fix point combinator in ML, without using recursion *)

datatype 'a T = K of 'a T -> 'a

fun Y h  = let fun g (K x) z= h (x (K x)) z	(* no recursion! *)
           in g (K g)
           end;

(* An example: the factorial function *)

fun F f 0 = 1
  | F f n = n * f(n-1);

val fac = Y F;
-----------------------------------------------------------------------------

The trick is the definition of the recursive type constructor T.
In the language Fun, you can do it in a similar way:

-----------------------------------------------------------------------------
(* The fixed point combinator Y can be defined without using recursion! *)

rec type R[a]=R[a]->a; (* R is a recursively defined type operator *)

value Y[a](h:a->a):a=(fun(x:R[a]) h (x x)) (fun(x:R[a]) h (x x));

value fac=
  let value F(f:Int->Int)(n:Int)= if n<=1 then 1 else n*f(n-1)
  in Y[Int->Int] F
  end;
-----------------------------------------------------------------------------

The language Fun is described in "On Understanding Types, Data Abstraction,
and Polymorphism", by L Cardelli & P Wegner, in ACM Computing Surveys, Vol 17,
No 4, (Dec 1985).

-- 
Thomas Hallgren
hallgren@cs.chalmers.se