[bitc-dev] Value restriction and type classes

[Swaroop Sridhar]

Jonathan S. Shapiro wrote:
> On Fri, 2006-05-19 at 01:52 -0400, Swaroop Sridhar wrote:
> 
>>In BitC, we impose the relaxed value restriction proposed by Garrigue.
>>So, only "dangerous" type variables are not generalized in an expansive 
>>expression....
> 
> 
> I'm not sure what question is being answered with this note. Are you
> just archiving the statement?

Well, I wanted note this property and make sure I understand it right.
If people who think and understand this better, confirm the following
behaviour, that would be very helpful.

Thanks,
Swaroop.


> -------- Original Message --------
> Subject: [bitc-dev] Value restriction and type classes
> Date: Fri, 19 May 2006 01:52:48 -0400
> From: Swaroop Sridhar <swaroop.sridhar at gmail.com>
> Reply-To: swaroop at cs.jhu.edu,   Discussions about the BitC language <bitc-dev at coyotos.org>
> To: Discussions about the BitC language <bitc-dev at coyotos.org>
> 
> 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).