[bitc-dev] Value restriction and type classes

[Swaroop Sridhar]

In BitC, we impose the relaxed value restriction proposed by Garrigue.
So, only "dangerous" type variables are not generalized in an expansive 
expression. For example:

In the expression:

(define (id x) x)
(let ((m (nil, (id id)))) ... )

`m' will be given the type:

for all 'a. ((list 'a), (fn ('b) 'b))

and not just:
((list 'a), (fn ('b) 'b)).

Now suppose that we have:

(deftypelass (ABC 'a 'b) ... ))

(let ((m: (forall (ABC 'a 'b)
	    ((list 'a), (fn ('b) 'b)))
          (nil, (id id)))) ... )

At this point, p will be given the type:

forall 'a. (ABC 'a 'b) => ((list 'a), (fn ('b) 'b))

That is, the type is ((list 'a), (fn ('b) 'b)) if the ABC constraint 
holds for all 'a and some 'b. Further, at this point, if the following 
instance exists:

(definsance (ABC 'c, int32) ... )

Then the monomorphic variable 'b will unify with int32 to produce the type:

m: ((list 'a) , (fn (int32) int32))

This case is not a problem for things like:

(define (add1 x)
     (let ((p = 1))
	(+ p x))

The type of p will be (Integral 'a) => 'a (and not forall (Integral 'a) 
=> 'a). Since there is nothing to be generalized, no predicates need to 
be solved at this stage. Hence the constraint will float to the 
definition of add1.

This is not even a problem at the top level define because at this 
stage, all restricted variables are instantiated to dummy types. So,

(define m: (forall (ABC 'a 'b)
	    ((list 'a), (fn ('b) 'b)))
          (nil, (id id))

will fail because of the unsatisfiable type:
forall 'a. (ABC 'a #dummy1) => ((list 'a), (fn (#dummy1) #dummy1))

Haskell does not have this problem since definitions are either 
completely polymorphic, or completely monomorphic (there is no value 
restriction or its relaxation).


Swaroop.