[bitc-dev] Value types and the Value restriction

[Swaroop Sridhar]

According to Jacques Garrigue's relaxed value restriction [1]:
In an *expansive* expression `E' with type `t', the generalizable type
variables in the type-scheme `sigma' are given by:

GEN(sigma) = FTVS(t) \ FTVS(gamma) \ V(t)

where,
FTVS(t) is the set if all the free type variables in t,
gamma is the environment that maps names to type-schemes,
FTVS(gamma) is the set of all type-variables already bound in the
      environment.	
V is the function Garrigue calls V- (V minus), which removes "dangerous"
      type variables from the set of generalizable ones, and is defied as
      follows:

V('a) = {}
V((mutable t)) =  FTVS(t)
V((fn (t1) t2)) =  FTVS(t1) U V(t2)
V((some-struct-union t1 ... tn)) =  V(t1) U V(t2) U ... V(tn)

That is, all type-variables wrapped by a mutable constructor and those 
occurring at contrapositive positions of function types are removed.

However, in a language that has unboxed mutability and unboxed composite
values, this restriction turns out to be insufficient to ensure
soundness. For example:

(defunion (optional 'b):val  none (some it:'b))

(define p:(mutable bool, 'a) (#t, none))

According to the above algorithm, we see that the value constructor none
has the type (optional 'a) and the type variable 'a occurs in
non-contrapositive position, and can this be generalized. Now, if we
give p the type:

p: (mutable bool, (optional 'a))
;; note that this is actually the type
;; (forall ('a) (mutable bool, optional 'a)))

we can then write:

(let ((r1:(optional int8) p.snd)
       (r2:(optional double) p.snd)) ... )

which is clearly not OK because r1 and r2 have different sizes and this
requires the polyinstantiation p.snd and thus its container p, which has
other mutable components.

If the problem is not clear from the above example (as it might seem
that `none' (optional any-type) might have the same representation),
consider:

(let ((r1:(mutable (optional int8)) p.snd)
       (r2:(mutable (optional double)) p.snd))
   (set! r1 (some 25))
   (set! r2 (some 25.0)) )

Therefore, we cannot give p a polymorphic type here.

So, we will have to revise Garrigue's restriction to take into account,
the issue of value types in mutable contexts. We will have a new
function V2 which takes a type and a mode parameter. The mode can be one
of remove or keep depending on whether we come from a value type or a
reference type context.

GEN(sigma) = FTVS(t) \ FTVS(gamma) \ V2(t, remove)

V2('a, keep) = {}
V2('a, remove) = {'a}
V2((mutable t), mode) =  FTVS(t)                   ;; any mode
V2((fn (t1) t2), mode) =  FTVS(t1) U V2(t2, mode)
V2((ref-struct-union t1 ... tn), mode) =           ;; see [*] below
                V2(t1, keep) U V2(t2, keep) U ... V2(tn, keep)
V2((val-struct-union t1 ... tn)) =                 ;; see [*] below 

                V2(t1, remove) U V2(t2, remove) U ... V2(tn, remove)
V2((array t), mode) =  V2(t1, remove)
V2((vector t), mode) = V2(t1, keep)
V2((ref t), mode) = V2(t1, mode)

[ [*] WARNING: These two rules assume that the reference type will never 
be unboxed. If this does not hold, these rules must also be treated like 
value-types. The polymorphism in examples 2,3,4,5 below apply only to 
reference types that will never get unboxed. Please see the alternate 
note after the examples marked [**]. ]

Now, the above example is properly typed:

(define p:(mutable bool, 'a) (#t, none))
;; p gets the type for-some-monomorphic 'a, (mutable bool, optional 'a)
;; and the 'a is then force to a dummy type as we are at the top-level
p: (mutable bool, (optional #X123))

To consider some more examples:

EXAMPLE 2:
All the permissible cases in original (Garrigue) rules are still
preserved for reference types :

(define p2_1:(mutable bool, (list 'a)) (#t, nil))
p2_1: (mutable bool, (list 'a))

(define p2_2:(mutable bool, (list 'a)) (#t, (lambda () nil)))
p2_2: (mutable bool, (fn () (list 'a)))

EXAMPLE 3:
Type-variables wrapped in a reference type are OK even if they lie
within an encompassing value type. Recall that list is a reference type.

(define p3:(mutable bool, 'c) (#t, (nil, nil)))
p: (mutable bool, ((list 'a), (list 'b)))

EXAMPLE 4:
Type-variables wrapped in a value type must be removed even if they lie
within an encompassing reference type.

(define p4:(mutable bool, 'b) (#t, (vector none)))
p: (mutable bool, (vector (optional #X345)))

Otherwise, one could write:

(let ((r1:(optional int8) (vector-nth p.snd 0))
       (r2:(optional double) (vector-nth p.snd 0))) ... )

EXAMPLE 5:
Accessor-like functions will work OK for reference types but will not 
work for value types.

(define (car x:(list 'a)) ... )
car: (fn ((list 'a)) 'a)
(define p5_1 (car (cons nil nil))
p5_1: (list 'a)  ;; OK polymorphic

(define (fst x:('a, 'b)) x.fst)
fst: (fn (('a, 'b)) 'a)
(define p5_2: (fst (nil, nil))
p5_2: (list #X456)

The right thing to do in this case is to define car and fst as terms and 
not ordinary-functions.

EXAMPLE 6:
Literals: This algorithm seems to do the right thing for literals.
(define p6_1:(mutable bool, 'b) (#t, 25))
p6_1: (mutable bool, #X234)
;; and not (forall ((IntLit 'a)) (mutable bool, 'a))

The literal is not given a polymorphic type because we start out with
the remove mode. If this is not done, inconsistencies similar to the
above example will arise.
(see: http://www.coyotos.org/pipermail/bitc-dev/2006-July/000722.html)

However it is customary that the literals should create extra problems.
If we have:
(define p6_2:(mutable bool, 'b) (#t, (vector 25)))

the above algorithm will not do the right thing. The fix is to say that 
the type of such literals is understood to be wrapped by a (Integer 'a) 
constructor, and add the additional rule:
V2((Integer t), mode) = V2(t1, remove) ;; similarly for floats.

This just expressively indicates the unboxed-ness of primitive 
integer/floating point types.

[**]
If we allow unboxing of reference-union/structure types, then we must 
change the corresponding V2 rule to:
V2((ref-struct-union t1 ... tn), mode) =           ;; see [*] below
                V2(t1, remove) U V2(t2, remove) U ... V2(tn, remove)

That is, this rule must be made exactly similar to
(ref (value-union-struct)).

At this point, vector is the only type that seems to benefit from the V2 
  algorithm and I think we should revert back to the SML rule that 
advocates that all type-variables within an expansive expression will be 
monomorphed. All hope is not lost, however, because we can define 
commonly used functions (like accessors) and other things we know are 
deeply immutable as `terms', and these restrictions do not apply if the 
expression is not expansive.


[1] GARRIGUE , J. Relaxing the value restriction. In In International
Symposium on Functional and Logic Programming {2004).
http://www.kurims.kyoto-u.ac.jp/home_page/preprint/PS/RIMS1444.pdf