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

[Swaroop Sridhar]

I will illustrate this scheme with an example. Here is the what the 
compiler currently does:

If we see something like:

(define top
   (let ((id (lambda (x) x))
        (id ())
        (id #t))
   ())
;; starting with a simple case, top has type (), and will never
;; get polyinstantiated itself.

1) polyinst() will first recurse over the let body and then over
letbindings.

2) We come to (id 1), and see that the letbinding (id (lambda (x) x) 
must be specialized. So, we obtain the letbinding:
    (id#fn_unit_unit: (fn (()) ()) (lambda (x) x))

3) This is then added along with the existing let-binding (as we cannot 
type the new binding without context):

(define top
   (let ((id (lambda (x) x)
	(id#fn_unit_unit: (fn (()) ()) (lambda (x) x))
        (id#fn_unit_unit ())
        (id #t))
   ())

Note that the letbinding got added to the AST _immediately_ .

4) Now, hopefully, the types on the RHS of the letbinding
(id#fn_unit_unit:(fn (()) ()) (lambda (x) x))

are fixed up, and we will recurse over (fn (()) ()) and
(lambda (x) x).

5) After processing the other expression (id #t), the letbinding will
look like:

(define top
   (let ((id (lambda (x) x)
	(id#fn_unit_unit: (fn (()) ()) (lambda (x) x))
	(id#fn_bool_bool: (fn (bool) bool) (lambda (x) x))
        (id#fn_unit_unit ())
        (id#fn_bool_bool #t))
   ())

After all polyinstantiation is done, we will look at the unreferenced 
polymorphic lambda binding (id (lambda (x) x)) and drop it.

(define top
   (let ((id#fn_unit_unit: (fn (()) ()) (lambda (x) x))
	(id#fn_bool_bool: (fn (bool) bool) (lambda (x) x))
        (id#fn_unit_unit ())
        (id#fn_bool_bool #t))
   ())


This all works fine, but is unfortunately wrong -- as is customary with 
the first take.

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.


Swaroop.