[bitc-dev] Relaxed value restriction and Literal polymorphism

[Swaroop Sridhar]

Jacques Garrigue's relaxed value restriction states that, within an 
expansive expression, we cannot generalize type variables if:

  - it is within a mutable-ref
  - it appears in the contravariant position of a function type.

[http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/, 2003.]

That is, in the following expression:

(define p:(mutable int32, (list 'a)) (10, nil))

p can be safely given the type:
p: for all 'a, (mutable int32, (list 'a))

and the fact that the first argument had a mutable type does not affect 
the second argument.

This works fine because the all possible specializations nil have the 
same representation, and we do not have to polyinstantiate p.

For example, the expression

(begin
    (set! p.fst 255)
    (let ((q:(list int32) p.snd)
          (r:(list bool)  p.snd)) ... ))

is fine because the assignment q = p.snd and r = p.snd are safe 
regardless of what type of list we are considering.

However, with the introduction of type classes, we wanted to do 
polymorphism over different kinds integer / floating point types.

For example:

(define p 1)
p: (forall ((Intlit 'a)) 'a) ;; no monomorphism as in Haskell

This requires polyinstantiation of p, but we are fine as long as 
everything is immutable.

But, if we have,

(define p:(mutable int32, 'b) (10, 20))

Now, p cannot be given the type
p: (forall ((IntLit 'b))  (mutable int32, 'b))

because, different usages of 'b have different representations and

(begin
    (let ((q:int32 p.snd
          (r:int64 p.snd)) ... ))

is an error.

Introducing an extra layer of indirection (ref boundary) does not help 
because,

(define p:(mutable int32, (ref 'b)) (10, (dup 20)))

(begin
    (let ((q:int32 ^p.snd
          (r:int64 ^p.snd)) ... ))

leads us to the same situation.

So, I think we have 3 options:

(1) Impose the grand SML rule that if an expression is expansive it is
     totally not polymorphic.

(2) Impose a rule that in the case of an expansive expression all type
     variables created by integer / floating point literals are
     monomorphic.

(3) Go back to the rule that says all literals are expansive.

Note that (2) and (3) are different.

(2) is the least restrictive rule we can impose, I think.

Swaroop.