Jonathan S. Shapiro wrote:
> I still think that my decision about making /mutable/ the keyword
> (rather than /immutable) was the right call -- if we want to build
> robust stuff, we need to encourage value-stable programming idioms. 

I strongly agree. We should keep immutability the default.

> But I also think that mutability is inevitable, and your path-based rule may
> turn out to be a good pragmatic compromise.

Here is my understanding of the final resolution:

There are actually two views of mutable types in the system: the type
system's (theoretical) view and programmer's view.

In the type system's view, mutable structures can only contain mutable
fields up to a reference boundary. That is, if p has type
(mutable (pair t1 t2)) then t1 and t2 must be shallowly mutable.

However, from the programmer's view, mutability can be described
pathwise. That is, it is legal to write

(defstruct iPair:val fst:(mutable int32) snd:int32)

and create mutable values of iPair.

(define ip:(mutable iPair) (iPair 10 20))

All of the assignments

(set! ip ip)
(set! ip.fst 15)
(set! ip.snd 25)

are legal since the type system sees all these as mutable.

In this sense, the original structure definition of iPair was actually a 
shorthand for

(forall (copy-compat 'a int32)
    (defstruct (iPair 'a):val fst:(mutable int32) snd:'a))

Since the type system propagates mutability inwards, the second field
will be forced to be mutable by the type system.

My understanding is that you wanted to permit the assignment
(set! ip.snd 25) since ip.snd is really mutable, and we don't want to
impose extra copy burden on the programmer. If this is not the case,
we can treat the above definition as a shorthand for

(forall (copy-compat 'a int32)
    (defstruct (iPair 'a) fst:(mutable int32) snd:(const 'a)))

where the interpretation of const is that we disallow mutation through
the field snd.

In the case of parametric structures such as pair, the definition is

(defstruct (pair 'a 'b):val fst:'a snd:'b)

Now, if we create a value p,

(define p:(mutable (pair int32 int32)) (pair 10:int32 20:int32))

 From the type system's point of view, the annotation of p is actually a
shorthand for (mutable (pair (mutable int32) (mutable int32))),
where mutability propagated inwards pathwise. Again, all assignments to
p, p.fst, p.snd will be permitted.

If my understanding is correct, I can go ahead and implement it in the 
compiler.

Swaroop.

_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to