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).
>
I agree.
>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
inner/outer.
We should probably call REF as HDBREF (Heap/data/bss ref) :)
>...
>By definition:
>
> (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.
Swaroop.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev