[bitc-dev] Resolution: Can boxed types be dropped?

Jonathan S. Shapiro shap at eros-os.org
Wed Feb 9 01:48:32 PST 2011


On Tue, Feb 8, 2011 at 7:41 AM, Sandro Magi <naasking at higherlogics.com>wrote:

> On 2011-02-08 2:29 AM, Jonathan S. Shapiro wrote:
> > But what about #Nil('a)? Well, that certainly /does/ occupy storage,
> > because it is an instance of #List('a), which is an unboxed type having
> > non-zero size. So since /nil/ is now attempting to be syntactic sugar
> > for ref(#Nil('a)), it would appear that Nil('a) now occupies storage.
>
> Absent a guaranteed optimization, which you do specify in the BitC spec,
> yes it could occupy storage for the header.
>

Incorrect. In the explored implementation, Nil('a) is actually
ref(#Nil('a)), and #Nil('a) is an instance of an unboxed type that
*definitely* occupies storage.


>
> > Is dup(#Nil) =eq= Nil guaranteed to be boolean true? If so, is this
> > accomplished by a subtyping illusion or is it accomplished by imposing a
> > constraint on the behavior of dup() when applied to union values
> > corresponding to a nullary constructor?
>
> I think the latter, ie. dup(#Nil) =eq= Nil is true. Semantically, dup
> would be an overloaded function provided by type class, which for Nil,
> is simply the identity. You can provide a specialized implementation in
> the compiler of course.
>

Good. You fell in to my trap!  [As did I]

#Nil is not a unique value! In order for dup(#Nil) to yield a unique value,
dup() is required to examine the value being duped.


> > And if the desired answer is "yes", then is deref(#Nil) =eq= Nil
> > guaranteed to be boolean true?
>
> I would expect "yes".
>

If the goal is to faithfully simulate the behavior of boxed types, I would
expect "yes" as well.


> > I think the answer to this has to be
> > "no", because if a structure contains a field of union type, we may be
> > trying here to capture the address of a field, and we want to be able to
> > use that later for address inclusion testing.
> I'm afraid I don't follow this. Do you have a trivial example
> illustrating this point?
>
struct X {
   l: List(char)
}

def x = X(#Nil(char))

def nilRef = AddressOf(x.l);

// is nilRef EQ to Nil?


> > And finally, consider that deref(ref(someList)) returns an assignable
> > location, so deref(ref(#Nil)) is an assignable location. Which means it
> > must be backed by storage, and further means that two instances of
> > ref(#Nil) probably had better not be Eq.
>
> What is the assignable location here? There is no field in #Nil to
> assign...


True. But deref(ref(someList)) isn't of type Nil. It's of type List('a), and
*that* type *does* have locations.


shap
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.coyotos.org/pipermail/bitc-dev/attachments/20110209/fcf83654/attachment.html 


More information about the bitc-dev mailing list