[bitc-dev] box/unbox take two
swaroop at cs.jhu.edu
Tue Feb 15 23:45:28 EST 2005
Jonathan S. Shapiro wrote:
>In discussions over the past two days, Scott has expressed some
>discomfort with how box/unbox work. I have come to share some of this
>discomfort. In particular, there is a sense in which the relationship
>between BOX (the type constructor) and BOX (the value constructor) is
>somehow uncomfortably different than the relationship between TUPLE (the
>type constructor) and TUPLE (the value constructor).
>Part of the confusion is simply that BOX/UNBOX were lousy names -- we
>keep shifting between adjective and verb and noun. Part of the confusion
>centers on reference types and their relationship to boxing, and part of
>the confusion derives from the fact that (box (box x)) is legal while
>(unbox (unbox x)) is not.
(unbox (unbox x)) is legal, if x is of type (box (box 'a)). Also, I donot
see the confusion here. This is no different from
(lambda x (lambda y ...))
and (apply (apply a b) c)
>Given which, I would like to try to re-state this part of the type
>system in a different way, and see if the restatement is somehow more
>comfortable, and then see if we have merely done a term rotation or
>there is some significant difference that has gotten introduced.
There is some kind of term rotation:
box, the type constructor --> ref
box, the value constructor --> dup
ref --> stack-ref
unbox without copy --> dref
>In the restated type and value system, the keywords are:
> REF STACK-REF DEREF and DUP
This does make a clear distinction of heap/data vs stack, rather than
We should probably call REF as HDBREF (Heap/data/bss ref) :)
> (deref (ref X)) === X ; identically-equals
> (deref (stack-ref X)) === X
By identically-equals, I think you mean location equality.
>If we reframe the type system and value constructors in this way, then
>we also need to look at composite types. For example, given:
>(defstruct S a:int32 b:char)
>S is a value type (which we have previously called an unboxed type), but
>the corresponding value constructor S has type
> S: (tuple int32 char) -> (ref S)
>that is, it constructs its value in the heap. All I am doing here is
>saying the S is the *unboxed* type, because it eliminates some confusion
>about the behavior of DEREF. Note that because S is no longer a
>reference type, we never need to state a type as being (DEREF s), which
>is why DEREF no longer needs to be a type constructor.
I believe that this view will be very helpful.
>The big change in all of this is that
> (ref (ref x))
>is illegal because ref can only be applied to a value type.
This is certainly better than the (box (box x)) === (box x) view.
Otherwise, (box (box (box ... infinite ... x )))))) ... === (box x),
and we will have to type the function
(define (f x) (box (f x))) correctly.
Depending on how the type-system is built, this may introduce a special
case in the loop detection scheme.
More information about the bitc-dev