[bitc-dev] Mutability

[Swaroop Sridhar]

Dr. Shapiro:

You said that there are some cases where the current mutability rules do 
not do the right thing. Are they in the test cases, otherwise can you 
please send me the examples?

The one case we talked about in Ottawa was:

(define Var1 (let ((p 1))
              (lambda (x) (+ x p)))

vs

(define Var2 (lambda (x)
               (let ((p 1)) (+ x p))

These two expressions produce different types for Vars:

Var1: for some Integer 'a => (lambda 'a 'a)

Var2: for all Integer 'a => (lambda 'a 'a)

Of course, the 'a in Var1 will get instantiated to a dummy type as it is 
free at top level.

However, this case is not surprising if we read it right.

Since, when the user writes:

(let ((p 1)) ... )

what he means that there is _one_ location called p with one type,

In the first case:
(define Var1 (let ((p 1))
              (lambda (x) (+ x p)))

The user says there is one p of _some_ integral type, and there is a 
lambda that takes a parameter of any type compatible with this type 
(that is, that type itself) and returns that same type.

However, when the programmer writes,

(define Var2 (lambda (x)
               (let ((p 1)) (+ x p))

he is saying that Var2 is a procedure that takes an argument x, whose 
type could be anything that is compatible with +. And, this procedure 
internally (per instantiation of the procedure) creates a local variable 
p which has exactly one location of _some_ (one) integral type that is 
the same as that of x.

Since these two things are different things, they get different types.

Swaroop.