[bitc-dev] Relaxed value restriction and Literal polymorphism
swaroop at cs.jhu.edu
Wed Jul 5 19:29:47 EDT 2006
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.
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.
(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.
More information about the bitc-dev