[PRL] Type question...

[Riccardo Pucella]

On Oct 5, 2007, at 7:30 AM, Felix S Klock II wrote:

>
> On Oct 3, 2007, at 11:33 PM, Riccardo Pucella wrote:
>
>>>> (let ((fact (lambda (num)
>>>>                 ((lambda (f n) (f f n))
>>>>                  (lambda (g m)
>>>>                    (if (< m 2) 1
>>>>                        (* m (g g (- m 1))))) num))))
>>>>    (fact 5))
>>
>>> I believe it's the (f f n) and (g g (- m 1)) that shoot you down.
>>> There's no simple type for a function that accepts itself as an
>>> argument.
>>
>> Right; as Carl says, just look at (lambda (f n) (f f n))
>>
>> The best type you could give it is the recursive type:
>>    (\mu Z.( Z x a -> b)) x a -> b
>
> Or a (sufficiently large) intersection type could also type the  
> term, I believe.

Is there a single type you can give f independently of its uses,  
though? I would have expected that f on its own would require an  
infinitely long intersection type, intuitively, the one corresponding  
to all the unwindings of the recursion. (I admit being rusty on  
intersection types.)

Presumably, if you know that you will be invoking (fact 5), you can  
stop recurring the type after long enough. But is that even possible?

  Cheers,
  R