On 2/12/11 1:55 AM, Jonathan S. Shapiro wrote:
> On Thu, Feb 10, 2011 at 9:57 PM, wren ng thornton<[email protected]> wrote:
>
>> My other thought on the whole issue is that, instead of thinking about
>> C-style pointers, it may be prudent to consider the constructor tag for
>> unions as part of the reference rather than as part of the referent....
>
> In an impure language where a union's content can be overwritten by another
> value of compatible type, this implementation isn't correct - which is why
> I'm looking from the other point of view.
Perhaps, but that's only the case because you have already assumed
C-style unions.
Get rid of the unions and think of constructor choice as a type-level
operation, and you don't have that problem--- impure language or no.
That is, if you think of the type
data IntList = Nil | Cons Int IntList
as meaning (pseudo C):
typedef union{
struct{} fromNil;
struct{ int head ; IntList* tail } fromCons
} IntList;
then naturally you're correct. However, there's no reason to assume
that's what it means. It's equally valid to say that it means something
more like (really not C):
typedef struct{} IntList$Nil;
typedef struct{ int head ; IntList* tail } IntList$Cons;
typedef (Nil | Cons)* IntList;
Which is to say, that there is a storage representation for things
constructed by Nil, and there's a storage representation for things
constructed by Cons, but that doesn't say anything about the storage
representation of IntList. A boxed IntList is just a Nil or a Cons, plus
whatever tagging information it takes to know which it is. It's
perfectly fine to overwrite the pointer to point to something else. But
the thing pointed to ---after you've unpacked the type tag and traversed
the pointer--- is not of the same type as the pointer is. Looking at the
type tag has given you extra information in exactly the same way that
case analysis in dependently typed languages gives you extra
information. You're assuming that the most-general type of Nil and the
most-general type of (Cons x xs) are identical, rather than that there
exists a most-general type containing both values. That's not true in
general.
Taking the perspective that the constructor tagging information belongs
to the reference rather than to the referent, the only time you'd run
into the problem you mention is if you wanted to unpack the definition
of IntList into another type definition (ala the {-# UNPACK #-} pragma
in GHC Haskell). In that case, sure, you'd have to resort to C unions---
but that's just saying that unboxed/unpacked values do not have the same
representation as the thing pointed to in boxed values (namely, the
unpacked version may take up more space and may have more stringent
alignment requirements).
--
Live well,
~wren
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
