[bitc-dev] Polyinstantiating local definitions -- take 2

[Swaroop Sridhar]

> The above algorithm works fine for `id' but will lead to many problems
in more complicated cases:
>
> For example:
>
> (define top
>   (letrec ((odd  (lambda (x) (even x)))
>            (even (lambda (x) (odd x) )))
>
>       (even 0:int32):int32))
>
> The original type for both odd and even is (fn ('a) 'b)
>
> When we process the body of the letrec, we see that `even' must be
> specialized for (fn (int32) int32), so we get:
>
> (define top
>   (letrec ((odd  (lambda (x) (even x)))
>            (even (lambda (x) (odd x) ))
>            (even#fn_int32_int32:(fn (int32) int32)
>                               (lambda (x) (odd x) )))
>
>       (even#fn_int32_int32 0:int32):int32))
>
> Now if we RandT this form, we get:
> odd: (fn (int32) int32)
> even: (fn (int32) int32) and
> even#fn_int32_int32:(fn (int32) int32)
>
> since all letbindings are typed and generalized together.
> So, any further usages of (even 200:int64) or (odd #t) will fail.

Here is an alternative algorithm to take 1. Maybe, we should not add
letbindings in place. We should probably introduce an inner letbinding,
that will encapsulate the body. For example:

(define top
  (letrec ((odd  (lambda (x) (even x)))
           (even (lambda (x) (odd x) )))

     (letrec ((even#fn_int32_int32:(fn (int32) int32)
                           (lambda (x) (odd x))))))
        (even#fn_int32_int32 0:int32):int32)))

Now the types at the original letbinding are left unchanged, and the
symbols in the inner letrec are built on a per-use basis. Further
specialization must be careful to emit things to the inner letrec and
not create a new let form for every binding -- especially in the case of
a letrec. Of course, in the end, we will have to carry forward all
non-polymorphic definitions in the original letbinding that were not
already specialized/referenced, and drop the original letbinding.

(define top
     (letrec ((even#fn_int32_int32:(fn (int32) int32)
                           (lambda (x) (odd#fn_int32_int32 x)))))
              ((odd#fn_int32_int32:(fn (int32) int32)
                           (lambda (x) (even#fn_int32_int32 x)))))

        (even#fn_int32_int32 0:int32):int32)))


Swaroop.