[bitc-dev] Semantics of unboxed

[Mark Miller]

Mark Miller wrote:
> EricNorthup wrote:
>> MarkM wrote:
>>> Jonathan S. Shapiro wrote:
>>>> If this is really correct, then we can omit all consideration of
>>>> "boxedness" from the language semantics...
>>> Until the language has side effects, EQ, or infinite rational trees
>>> (cyclic containment).
>> Can you elaborate on how side-effects muddle the picture?
> [...]
> struct Bar {
>     final int a;
>     final int b;
> };
> 
> var Bar bar1 = { 3, 5 };     // bar1.a is 3, bar1.b is 5
> 
> final Bar bar2 = bar1;         // bar2.a is 3, bar2.b is 5
> [...]
>     bar1 but .b is 6
> 
> evaluates to a Bar object just like bar1, but with its .b field set to 
> 6; and if we interpret
> 
>     bar1 but= .b is 6
> 
> to mean
> 
>     bar1 := bar1 but .b is 6

In a language in which dynamic allocation may fail (i.e., as Shap points out, 
within any language implementable on physically realizable hardware), the 
supposed equivalences previously pointed out are no longer equivalent. The 
expression

    bar1 but .b is 6

must be assumed to allocate, and therefore to possibly fail. If Bar is 
*explicitly* unboxed however,

     bar1 but= .b is 6

can be known not to allocate, and therefore not to potentially cause a failure 
from memory exhaustion. In a GC-less subset of the language, as would be used 
to write a kernel or space bank, the first should be prohibited, while the 
second can be allowed. We can therefore no longer faithfully explain the 
semantics of the second as equivalent to

      bar1 := bar1 but .b is 6

-- 
Text by me above is hereby placed in the public domain

     Cheers,
     --MarkM