Y combinator

Dr. Mark E. Hall mehall@mut.ac.th
Fri, 10 Dec 1999 20:00:15 +0700 (ICT)


> > You cannot write the Y combinator in any strongly-typed (Hindley-Milner-like)
> > language - it has an infinite type in such typing schemes
> > 
> > Y : x -> x -> x -> x -> x -> ....
> 
> Dear Andrew.
> I still have a question. If I cannot write the Y combinator in any 
> strongly-typed (Hindley-Milner-like) language, how can I write 
> it in ML? After all, ML is the first language to use Hindley-Milner 
> algorithm. The code below works perfectly well in ML:
> 
> datatype 'a t = T of 'a t -> 'a
> 
>  val y = fn f => (fn (T x) => (f (fn a => x (T x) a)))
>                    (T (fn (T x) => (f (fn a => x (T x) a))))
> 
> val fat y (fn again => (fn x => if x<1 then 1 
>                                            else (x*(again (x-1))  )))
> 
> Isn't it possible to write similar code in Clean? Why not?
> 
> Eduardo Costa

Yes, you can write similar code in Clean. The following should work just
fine (I haven't had time to re-install Clean since upgrading my hardware
recently, so I haven't tried it):

:: D a = Disguise (D a -> a)

yCurry :: (a -> a) -> a
yCurry f = let
		g (Disguise x) = f (x (Disguise x))
	in g (Disguise g)

I have written it using a local definition to make its structure clearer.
As with the ML code above, it works because of the parametrized algebraic
data type D a ('a t in the ML code), which allows you to disguise a
function D a -> a as a value of type D a, at least as far as the type
inference and checking is concerned. Your original suggestion,

>
>Y f= ((\f x-> f x x) ((\ f g x->(f (g x))) f))
>              ((\f x-> f x x) ((\ f g x->(f (g x))) f))
>

does not make use of this disguise, and therefore winds up with an
infinite type, as Andrew pointed out. Incidently, the type D a is also
infinite, as you can see if you try to expand it out fully, but its
recursive definition using the data constructor Disguise allows its
true nature to be hidden from the type inference and checking mechanism.

In any case, I would agree with Andrew that if you really need a
fixed-point combinator (for instance, if you were using Clean to write
an interpreter for a language that allowed recursive definitions) then
you would be best off defining it by

y f = f (y f)

(which you also mentioned in your original posting), as this should
compile to very fast, compact code in Clean.

Mark

________________________________________________________________________________

                                  Mark E. Hall
                      Mahanakorn University of Technology
                          Vanit Building 2, 8th Floor
                           1126/1 New Petchburi Road
                            Bangkok 10400, Thailand
                                66-2-6553181--7
                                mehall@mut.ac.th
                          http://www.mut.ac.th/~mehall