[tlug] Re: Y Combinator

[John Fremlin <john@example.com>]

Stephen J. Turnbull wrote:
> John Fremlin writes:
>
>  > > fix :: (a -> a) -> a
>  > > fix f = let x = f x in x
>
>  > The main thing that puzzled me is that the type of fix is
>  > 
>  > fix :: (a -> a) -> a
>  > 
>  > but "a" must in fact have type
>  > 	b -> b
>  > because it's used as a function.

> Is that a question, or does the past tense mean you got it?
>
> Of course f is used as a function and thus must have a type of the
> form (a -> b), to have a fixed point it must be that a = b, and the
> fixed point itself must have the type a.  Ergo
>
> fix :: (a -> a) -> a

Yes, you are quite correct.

I was wrong to say that a must have type b->b in general. In fact there 
is no requirement for this. Thank you for explaining that.

I was confused, because I cannot see any reason for fix f, if f is of 
type a->a and the value returned by f depends only on its arguments, 
because either it must ignore its argument (and therefore be a constant) 
or fix f will not terminate.

To be concrete it is in fact possible to write this

Prelude> fix (\x -> 1)
1

Or even

Prelude> :t fix id
fix id :: t
Prelude> fix id
^CInterrupted.

In general, it is also possible to use multiple arguments, and they 
could even be of different types.

Prelude> fix (\x n -> if n == 0 then "zero" else "not zero") 0
"zero"
Prelude> :t fix (\x n -> if n == 0 then "zero" else "not zero")
fix (\x n -> if n == 0 then "zero" else "not zero") :: (Num a) => a -> 
[Char]



Prelude> fix(\x n y -> if n == 0 then y else n * y * (x (n-1) y)) 5 1
120

where
Prelude> :t fix(\x n y -> if n == 0 then y else n * y * (x (n-1) y))
fix(\x n y -> if n == 0 then y else n * y * (x (n-1) y)) :: (Num a) =>
                                                            a -> a -> a
Prelude> :t \x n y -> if n == 0 then y else n * y * (x (n-1) y)
\x n y -> if n == 0 then y else n * y * (x (n-1) y) :: (Num a) =>
                                                       (a -> a -> a) -> 
a -> a -> a