[bitc-dev] Rationale for unboxed mutability in BitC?

[Swaroop Sridhar]

David Hopwood wrote:
> I hope that boxing in a language's semantics is not being confused with
> boxing in a language's implementation. In the latter, it is of course
> possible to "inline" ref cells into the representation of a structure or
> array, and this seems to give the performance advantages of unboxed
> mutability, while still allowing to use a well-understood ML-style type
> system. Or is there some other argument for unboxed mutability in the
> semantics that I'm missing?

On the necessity of exposing unboxed representation:

As Sam Masson has already said, this is a matter of expressiveness in 
the language. Otherwise, we will have to appeal to external systems (C) 
to express or update such data-structures. This approach is taken by the 
Hello operating system written in SML, and House/OsKer written in 
Haskell. I have learnt from Iavor that efforts are on to integrate more 
expressiveness about low-level representation into GHC, which can be 
used for writing systems programs. One of the design goals of BitC is to 
give the programmer precise control over data-structure representation.

The effect of this is that we may get better performance due to 
unboxing, and the fact that we don't need any marshalling / 
unmarshalling while interfacing with outside code.

However, the compiler is -- in general -- not free to convert between 
boxed/unboxed representations albeit for the sake of performance. I 
think that the tech report must clarify this point.

> Why do you argue that 'high-performance "systems" codes' require *unboxed*
> mutability, in particular?

The need for updating unboxed cells is also a matter of expressiveness, 
which we need in the language. However, for the purposes of type 
inference, it is possible to think of mutation as if it were to be 
updating a ref cell, and accessing a variable, fetching that value. This 
preserves principal types, but will constrain the freedom in 
compatibility of types at a copy-boundary.

> My impression is that this choice seems to be imposing a great deal of
> complexity on BitC's type system, ...

I think much of the complexity in that type-system is due to the 
inference-hints. The rest of the type system (maybe types) is a matter 
of simple sub-typing and we can infer principal types for all 
monomorphic types. However, with the introduction of polymorphism, we 
need to make a decision about the mutability of the _copy_ of a value, 
and in the absence of explicit annotation, there is no perfect answer. 
The hint scheme is an attempt to ``guess'' the user's intension based on 
the flow of types in the system. If there is a better way of inference 
or formalization for this issue, I would like to learn about it.

Swaroop.