Type equivalence

 

The question of when type A is equivalent to type B has been difficult to resolve using other views of what a type is. If, however, types are viewed as sets that merely serve as domain and codomain constraints on functions, there is only one sensible answer: type A is equivalent to type B, if and only if the same set of values make up both type A and type B.

Thus, if we declare

type A = array 1..10 of Int
type B = array 0..9 of Int

we can determine whether types A and B are equivalent merely by determining whether set A is equal to set B.

Of course, the difficult question now becomes the interpretation to be given to type constructors. Most type constructors have straightforward interpretations, as can be seen from the following examples:

set of T =
array R of T =
pointer to T =

We thus can readily conclude that types A and B above are not equivalent since $f\; =\; g$ for all Int and Int. But what about the following types?

type C = record x : Int;  y : Char end
type D = record x : Int;  y : Char end

The question should be familiar to participants in the name equivalence versus structural equivalence debate. By interpreting types as sets, the question is transformed, however, from ``Are types C and D equivalent?'' into ``How does one characterize the set of values represented by a record constructor?''. Neither question has an answer that will satisfy everyone.

Given our convention of interpreting a variable name, such as R, as syntactic sugar for $r()$, it seems reasonable to regard R.x as syntactic sugar for $r()(x$_C) and S.x as syntactic sugar for $s()(x$_D), if R is of type C and S of type D. This requires the following interpretation of type C as a set:

_C, y_C} →Int Char
$$and   f(x_C) ∈Int and  f(y_C) ∈Char}

Thus, if $x$_C = x_D and $y$_C = y_D then types C and D are equivalent. We now have two sensible choices:

1. $x$_C = $x$_D = `x' and $y$<sub>C</sub> = $y$<sub>D</sub> = `y'.
2. $x$_C, $y$_C, $x$_D and $y$_D are distinct values.

Selecting the first choice amounts to a form of structural equivalence that allows the conclusion that type E, below, is also equivalent to types C and D.

type E = record y : Char;  x : Int end

Selecting the second choice amounts to name equivalence.