Re: IMA vs tree-ssa

[Gabriel Dos Reis <gdr at integrable-solutions dot net>]

Mark Mitchell <mark@codesourcery.com> writes:

| 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

Footnote 46) from the C standard is even more explicit as to what
the intent of type-compatibility is:

       46)Two types need not be identical to be compatible.

meaning you may have compatible types that are not equal.

| 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.

  (1) But C is not C++, and that is NOT quibbling.  You get all kinds
      of troubles when you start applying C++ logic to the C type
      system (but in fact here, it is not even C++ logic). 

  (2) you can apply your reasoning to int and double and conclude there
      is equality between int and double despite the standard
      explicitly saying they are different.

  (3) Suppose a plateform where char is signed.  You can repeat your
      reasoning and conclude there is equality between char and signed
      char.  Yet, the C standard says char is distinct from signed char.
      Ditto if char is unsigned on the plateform.

| You claim that in C two enums can be incompatible even if the
| underlying type is identicial.

I think Joseph is right.

-- Gaby