[bitc-dev] Relaxed value restriction and Literal polymorphism

[Jonathan S. Shapiro]

I think that the issue here is not a problem with the logic of
generalization of typing. It is a problem with value types (i.e. unboxed
types). The contagion you describe is a consequence of needing to know
the representation of the object, not a consequence of the typing rules.

The resolution seems straightforward, but I may be missing something:

  The value restriction, when applied, extends to the entire unboxed
  unit. In consequence, a value restriction applied to some constituent
  of a type (e.g. a field) must be applied to the type as a whole.

Note, however, that this rule is conservative. In your example below, if
the integer were replaced by a reference type, you would know the
representation and there would be no problem.

In this case, it is better to have a simple conservative rule instead of
a complex rule. Therefore, I would not try to make the rule be
conditional on the sizes of fields. Simply declare that the restriction
applies to the aggregate.

shap


On Wed, 2006-07-05 at 19:29 -0400, Swaroop Sridhar wrote:
> 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.
> _______________________________________________
> bitc-dev mailing list
> bitc-dev at coyotos.org
> http://www.coyotos.org/mailman/listinfo/bitc-dev