IMA vs tree-ssa

[Mark Mitchell]

Joseph S. Myers wrote:

>On Mon, 8 Mar 2004, Mark Mitchell wrote:
>
>  
>
>>A type system with non-transitive type-equality breaks all the standard 
>>mathematical models for type theory.  (And, yes, I know the C type 
>>system is ugly, but most of it can actually be modeled in pretty 
>>conventional ways.)  The category-theoretician in me is befuddled by 
>>what a non-transitive type-equality model could possibly mean.
>>    
>>
>
>It's not type-equality, it's type-compatibility.  Equality of types also
>exists, and behaves transitively.
>  
>
Well, yes, that's true. 

But the way that the C standard uses compatibility somtimes implies 
something very much like equality.  In particular, the fact that you can 
assign in both directions, for example, is an equality-style 
requirement.  Using enums:

  enum A { x = 6 }; /* Assume compatible with "int" on this system.  */
  enum A a;
  int i;
  
  a = i; /* OK */
  i = a; /* Also OK. */

With a standard partial-order (e.g., for derived/base types in C++) only 
one of those assignments would be valid.  If both are valid, then you 
have type equality between "A" and "i", under most models.

You claim that in C two enums can be incompatible even if the underlying 
type is identicial.  The version of the EDG front end that I have does 
not seem to agree with you, but let's assume that you are right.  (I 
don't really know.)  One type-theoretic way of understanding that would 
be that both enums are subtypes of the underlying type, and that the 
first assignment above is just syntactic sugar for "a = (enum A)i;".  
You also have to adjust the memory-access rules for pointer types in 
some funny, theoretically inconvenient ways, but it could be done.

The incomplete array example, is not nearly so messy.  In that case you 
can think of both "int [5]" and "int [3]" as subtypes of "int []".  
Things are easier because there are no objects of type "int []", 
although there are objects of type "int (*)[]" and so forth.

In any case, with incomplete structure types (Geoff's example), we're 
positing that the standard means for you to be able to complete a single 
type in more than one way.  I don't believe that anyone ever intended that.

This would be the first major case I know of in C where you could write 
code that was valid across translation units that was not valid within a 
translation unit, and I see no evidence that was intended. 

Certainly, things like:

  extern int i[];
  int i[3];

are valid whether within one translation unit or across two.  But, you 
cannot complete the same structure type in two different ways in the 
same translation unit.  The idea that in C you could not validly combine 
all your translation units into a single translation unit (with  
appropriate alpha-renaming of things with internal linkage, and with 
appropriate merger of tentative definitions, if you've adopted that 
(optional) behavior) is, to me, in contradiction with the spirit of the 
language requiring declarations to have compatible types across 
translation units.

In any case, we could probably debate here until we are blue in the 
face: we really ought to ask the C committee and get something 
approaching a definitive opinion.  Would you please do that?

-- 
Mark Mitchell
CodeSourcery, LLC
(916) 791-8304
mark@codesourcery.com