Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!usc!snorkelwacker.mit.edu!ai-lab!zurich.ai.mit.edu!markf
From: markf@zurich.ai.mit.edu (Mark Friedman)
Newsgroups: comp.lang.functional
Subject: Re: A question about types in ML
Message-ID: <MARKF.90Dec5112529@montreux.ai.mit.edu>
Date: 5 Dec 90 16:25:29 GMT
References: <fraser.658398987@melomys> <4906@rex.cs.tulane.edu> <chl.658489695@m1>
	<4953@rex.cs.tulane.edu> <2531@wn1.sci.kun.nl>
Sender: news@ai.mit.edu
Reply-To: markf@zurich.ai.mit.edu
Distribution: comp
Organization: M.I.T. Artificial Intelligence Lab.
Lines: 66
In-reply-to: ge@wn3.sci.kun.nl's message of 5 Dec 90 09:42:56 GMT

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

   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

This is cheating. The interesting property of the Y operator is that
it does not make use of any primitive recursive definition mechanism.
The above definition does this in the expression "g = f g".

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

I assume that you meant "= x * (f (x-1)), otherwise" for that last
line.

   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

This is a red herring. The above y is not the Y operator of interest to
us; it does not create a procedure (i.e. a closure). The difficulties in
writing and type checking the Y operator occur with higher order
functions (i.e.  first class procedures.)  If Algol68 has them, try
writing the "real" Y operator.

Also, I assume you meant "ELSE x * f(f, x-1)".

-Mark
--

Mark Friedman
MIT Artificial Intelligence Lab
545 Technology Sq.
Cambridge, Ma. 02139

markf@zurich.ai.mit.edu


Brought to you by Super Global Mega Corp .com