[bitc-dev] Mutability inference in BitC

[Swaroop Sridhar]

Thanks for your response and comments/spec corrections. I have addressed 
some of the issues you have raised in the following mail.

Jeff Foster wrote:
> Hi.  I read through the BitC manual, and I'm pretty confused about ref 
> types vs. value types and how mutability works in BitC.

reference-types and value-types correspond (respectively) to types that 
have a boxed, or an unboxed representation.

For example:

(defstruct Sref:ref i:int) ;; ref/boxed type
(defstruct Sval:val i:int) ;; val/unboxed type

Values with type Sref will have the representation of a pointer to a 
heap allocated cell containing the structure, where as the values with 
type Sval will reside on the stack (or any other containing structure).

The type (ref t) in bitc stands for reference to type t. This does not 
entail mutability of the location being referenced. In this sense, 
references are pointers that can later be dereferenced.

For example:

(define p (dup #t))
p: (ref bool)

`dup' copies its argument to the heap and returns a pointer (reference) 
to it. The type of p is (ref bool) (and assignments to p will not work).
Currently, we only have references that name (point to) heap cells.

Values with type (ref t) can later be dereferenced using the ^ (deref) 
operator. But other reference types (ex: vectors, Sref above) cannot be 
dereferenced.

> One thing that confused me is that I don't understand why there's a val 
> type constructor. 
> Does your system allow types like val (ref (val (ref int)))?  Does that 
> type make sense?

In BitC's type world, there is no `val' type-constructor. That is, we 
never form types like: (ref (val (ref int)))

The BitC syntax provides a (type-constructor like) keyword `val' to 
obtain the type t from (ref t) and if the user writes (syntactically)
(val (ref (val (ref int)))), it is understood to mean the type int.

The motivation for val was that we had a deftype construct to create 
type synonyms, and the user could then write:

(deftype bPtr (ref bool))
...
(define p (dup #t))
(define pVal:(val bPtr) p^)

But, without the deftype construct, the val construct is probably not as 
useful.

>  There are two approaches I know of to deal with updatable references:
> ML -- everything is in the types.  The left-hand side of an assignment 
> is always a ref, and writing to a ref means updating its contents.  If 
> you want to get the contents of the ref, you need to carry out an 
> explicit operation
> 
> C -- definitions of variables allocate memory on the stack.  Types do 
> not distinguish what can and cannot be updated, but instead there's a 
> separate notion of l-value vs r-value.  Only l-values can appear on the 
> left-hand side of an assignment.  l-values that appear in r-positions 
> (defined syntactically) are automatically converted into an r-value with 
> their contents.  You can convert an l-value into an r-value representing 
> a pointer by using &.
> 
> The BitC approach doesn't quite seem like either of these.  Can you 
> explain it in terms of one or the other, or explain how it's different?

I think BitC's approach is a combination of both of the above, but is 
closer to the C model.

Unlike ML, we don't require that all mutability be encapsulated within 
ref-boxes. We permit assignment to unboxed values.

Like C, we have a notion of expressions that can appear as lvalues.
Section 8.1 (p25) says that the following expressions:

id
(array-nth loc ndx)
(vector-nth e ndx)
(member loc ident)
(deref e)

evaluate to ``locations,'' which are candidates to be the target of a 
set! (assignment). Locations are automatically converted to values 
(rvales) when used in an rvalue context.

However, not all locations are mutable. Only those locations with a 
mutable type can be assigned to. Unlike C's `const' qualification --- 
and like the ML model --- BitC ensures that the types are binding on all 
locations across all aliases.

Therefore, I can probably summarize as:
-- Mutability is decided by the type.
-- Constructs for name binding (lambda, let) and updatable locations are
    not mutually exclusive. Mutable variable bindings also
    create updatable locations (whether on the stack or on the heap).
-- We impose lvalue restrictions like C in order to preserve user's
    intuition of what is getting set!ed.

> p11 - are defstruct and defunion definable from defrepr, or do they need 
> to be special forms?

Once the implementation of defrepr is finalized, it is our intension 
that defstruct and defunion will be syntactic sugar that reduce to defrepr.

> p19 - I found the subsection title ``Value Constructors'' confusing, 
> because make-vector is listed, but on p9 it says there's no value type 
> for vectors.  Is there a difference between being a value and having a 
> value type?

As I said above, value types are just unboxed types and ref-types are 
boxed types. However, all types have some constructor that constructs 
values of that type (value-constructor), regardless of whether that type 
is a value type or reference type. I agree that this terminology is 
confusing, and we should probably shift to calling the types 
boxed/unboxed types instead?

> p26 - Are there restrictions to what you can define in interfaces?  
> E.g., can you define a function?

Currently, an interface may contain all permissible top-level 
definitions. That is, functions or other (immutable) definitions (data) 
are OK in an interface. A stateful interface may also export mutable data.

> Do you have something like a sequence of examples that start simple 
> and show the various aspects of your design?  That would be really helpful.

I have various examples in used in different contexts. I will send out 
another note after consolidating all these examples.

Swaroop.