[bitc-dev] Vectors with mutable elements

[Swaroop Sridhar]

Jonathan S. Shapiro wrote:
> On Fri, 2006-05-19 at 02:21 -0400, Swaroop Sridhar wrote:
> 
>>Jonathan S. Shapiro wrote:
>>
>>>Do we want to introduce a type class for each literal type (even if only
>>>conceptually)?
>>
>>I think this is the best way of establishing that a literal can be of 
>>mutable or immutable type.
> 
> 
> Conceptually, I agree. However, I think that these type classes want to
> be "closed".
> 
> At run time, there is no difficulty with extending these classes. The
> difficulty is extending them at compile time. I think that the "reader",
> in general, is not able to execute user-supplied code at tokenization
> time.
> 
> This suggests that the LitChar class should be closed. A user can always
> extend it by introducing a subclass Char.
> 
> I am also concerned that adding the mutable variants to these classes
> will introduce a further difficulty: procedures may become more likely
> to get polyinstantiated. For example, consider a procedure CHAR-CODE,
> that accepts a character and returns the code point. There are two ways
> that this procedure might be typed:
> 
>   CHAR-CODE: (fn (char) uint32_t)   ; argument is constant
>   CHAR-CODE: (forall (LitChar 'a) (fn ('a) uint32_t))
> 
> In this case, the body of the procedure does not require mutation, and
> the "copy on apply" rule ensures that the first version can be used in
> all contexts where the second can be used.
> 
> In the second version, however, the argument is an alpha type. It
> appears to me that this will cause CHAR-CODE to be instantiated twice,
> once for char and again for (mutable char). I am not sure what should be
> done (if anything) to cope with this.
> 
> Of course: the user can control this explicitly by writing the type
> explicitly in the example above, but the need to do this is a bit
> unsettling. We can certainly try it and see what happens. If we *do* try
> it, I think we should impose the following rule:
> 
>   In any situation where type inference yields two possible typings
>   T and (mutable T), the typing ambiguity should be resolved in favor
>   of the non-mutable type.
> 
> Reactions?


Since all functions accepting an argument of type `t' also accept 
(mutable t), it is advantageous -- for reasons of polyinstantiation as 
you have noted -- not to generalize the type of functions like CHAR-CODE as:

CHAR-CODE: (forall (LitChar 'a) (fn ('a) int32))

but to give it the equally powerful type:

CHAR-CODE: (fn (char) int32)

So, let me propose that we write the character class as:

(deftypeclass (LitChar 'a)
	(tyfn () 'a))

;; because of the way the tyfn is written, we can never write an
;; instance for (LitChar 'a)

(definstance (LitChar char))
(definstance (Litchar (mutable char))

Now, the CHAR-CODE will have the type:
(LitChar 'a) => (fn ('a) int32)

and NOT
forall 'a. (LitChar 'a) => (fn ('a) int32)

So, the (LitChar 'a) must be resolved at the definition. At this point, 
we invoke your immutable instances win over mutable instances rule, and 
obtain the type:

CHAR-CODE: (fn (char) uint32_t)


Swaroop.