[bitc-dev] DISCUSS: Name That Type Class!
swaroop at cs.jhu.edu
Sun Jul 20 16:45:05 CDT 2008
Jonathan S. Shapiro wrote:
> On Sun, 2008-07-20 at 17:12 -0400, Swaroop Sridhar wrote:
>> For example, if we want to specify the type of a function that receives
>> a reference to a pair whose components must be of fixed type (say
>> (int32, bool)) but we don't care whether the pair itself is mutable or
>> not. Using top-copy-compat, we can specify a type that is polymorphic
>> over the mutability of the pair type. For example:
>> (define (f x) x^.fst:int32 x^.snd:bool ())
>> f: (forall ((top-copy-compat 'a (pair int32 bool)))
>> (fn ((ref 'a)) ()))
> I cannot figure out what this means, because the syntax is illegal.
> Also, your example involves deep mutability variance, which is generally
> NOT copy-compatible. Can you expand this example more clearly?
Actually what you say is true, the top-mutability compatibility does not
arise directly from a copy operation -- full copy compatibility is
permitted as these positions. It just permits certain variance of
top-level mutability of values.
top-mutability compatibility is only useful within reference types. It
is used to specify functions that are polymorphic over top-level
mutability of certain parameters with reference type.
The above function f requires a parameter x whose type is
i) reference to a pair
ii) the pair itself can be mutable or immutable
iii) the components of the pair must be (int32, bool)
-- copy compatibility does not arise here because x is of
(define (f x)
the function f dereferences x and accesses the two field of the pair
contained within x. Through explicit qualification, it fixes the
type of the components of the pair to int32 and bool. However, since it
does not say anything about the mutability of the pair itself, we give
it the type
f: (forall ((top-copy-compat 'a (pair int32 bool)))
(fn ((ref 'a)) ()))
Now, both the applications
(f y:(ref (pair int32 bool))) and
(f z:(ref (mutable (pair int32 bool)))
are type safe.
More information about the bitc-dev