[bitc-dev] Relaxed value restriction and Literal polymorphism
Jonathan S. Shapiro
shap at eros-os.org
Thu Jul 6 09:50:28 EDT 2006
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.
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
> (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
> (let ((q:int32 p.snd
> (r:int64 p.snd)) ... ))
> is an error.
> Introducing an extra layer of indirection (ref boundary) does not help
> (define p:(mutable int32, (ref 'b)) (10, (dup 20)))
> (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
> (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.
> bitc-dev mailing list
> bitc-dev at coyotos.org
More information about the bitc-dev