Type Equivalence

Algol68 allows recursive types. Algol68 uses “Mode” as most language definitions use “type”. I will use C declaration syntax here for it is more familiar and has the necessary structure. The scope of an Algol68 declaration includes the whole block and not just the portion of the block beyond the declaration. Manifestly recursive declarations are thus possible such as:typedef struct{float x; zot * p;} zot; typedef struct{float x; zat * p;} zat;
An immediate question is whether we have defined one or two types here. Algol68 says that these types are in all ways equivalent and equivalent even to zit in:typedef struct{float x; zit * p;} zzz; typedef struct{float x; zzz * p;} zit;
There is one type here with four names.

The first edition of the language defining report ignored the question of how a compiler might test for equivalence. The final Edition (1975) gave a remarkable algorithm which I describe here. It noted that it was then well known, but alas not well enough known. There was no attribution as to source.

The problem arises in asking whether two structures are equivalent. Normally you require that the respective structure fields be equivalent, but that rule leads to the useless observation that zot and zat are equivalent just in case they are equivalent. The provided decision procedure allows, while testing the individual fields in structures A and B, one to assume that A is equivalent to B. This is just short of the familiar bogus logic of saying that it OK to assume X during the proof of X. It is also a bit like valid mathematical proofs by induction. There may be several such recursion hypotheses in effect as the tree of possible equivalences (or discrepancies) is traversed.

This equivalence concept may be described as requiring that the infinite trees produced by such definitions be identical. Such trees do not include type names, but do, in the case of Algol68, include field names.

I don’t know the worst case performance of this algorithm. I wrote it and watched it run and I could not find cases that make it run slowly. Here is the algorithm applied to testing Scheme values that are infinite due to loops in the pointer structures.

Algol68 requires a pointer in any declaration loop thus disallowing types such as:typedef struct{float a; Zot g;} Zot;

The top example in native Algol 68:

MODE ZOT = STRUCT(REAL x, REF ZOT p);
MODE ZAT = STRUCT(REAL x, REF ZAT p);
ZOT o; ZAT a := (3.14, a);
print(x OF a);
o := a;
print(x OF o);
MODE ZZZ = STRUCT(REAL x, REF ZIT p);
MODE ZIT = STRUCT(REAL x, REF ZZZ p);
ZZZ z; ZIT i := (42.0, z);
o := i;
print(x OF o) 
# yields:
3.14 3.14 42. #

C’s notion of type equivalence is much more limited. Gcc and clang both reject the following assignment blaming type mismatch:

typedef struct { int y;} a;
typedef struct { int y;} b;
int main(){a x; b y;
x=y; return 0;}

Some languages (Euclid?) used “new” as a type annotation when the programmer wanted an incompatible type despite structural equivalence.

It is not the mere spelling of the type that C considers:

typedef struct { int y;} a;
a x;
int main(){typedef struct { int y;} a;
a y;
x=y; return 0;}

Again both gcc and clang refuse.