Does an ADT have multiple or only one representations/implementations?

Question

Section 24.2 in Types and Programming Languages by Pierce defines ADTs in existential types:

A conventional abstract data type (or ADT) consists of (1) a type name A, (2) a concrete representation type T, (3) implementations of some operations for creating, querying, and manipulating values of type T, and (4) an abstraction boundary enclosing the representation and operations. Inside this boundary, elements of the type are viewed concretely (with type T). Outside, they are viewed abstractly, with type A. Values of type A may be passed around, stored in data structures, etc., but not directly examined or changed—the only operations allowed on A are those provided by the ADT. ... We first create an existential package containing the internals of the ADT:

counterADT =
{*Nat,
{new = 1,
get = λi:Nat. i,
inc = λi:Nat. succ(i)}}
as {∃Counter,
{new: Counter,
get: Counter→Nat,
inc: Counter→Counter}};

> counterADT : {∃Counter,
{new:Counter,get:Counter→Nat,inc:Counter→Counter}}

We can open it for example

let {Counter,counter} = counterADT in
counter.get (counter.inc counter.new);
> 2 : Nat

Does the highlighted sentence in the following quote say that a ADT can have multiple representations/implementations?

A key property of the kind of information hiding we are doing here is representation independence. We can substitute an alternative implementation of the Counter ADT—for example, one where the internal representation is a record containing a Nat rather than just a single Nat,

counterADT =
{*{x:Nat},
{new = {x=1},
get = λi:{x:Nat}. i.x,
inc = λi:{x:Nat}. {x=succ(i.x)}}}
as {∃Counter,
{new: Counter, get: Counter→Nat, inc: Counter→Counter}};

> counterADT : {∃Counter,
{new:Counter,get:Counter→Nat,inc:Counter→Counter}}

in complete confidence that the whole program will remain typesafe, since we are guaranteed that the rest of the program cannot access instances of Counter except using get and inc.

Do the highlighted sentences in the following two quotes say that an ADT can have only one representation/implementation?

On p377:

In summary, the single representations of ADTs directly support binary operations, while the multiple representations of objects give up binary meth- ods in return for useful flexibility. These advantages are complementary; nei- ther style dominates the other.

From a reply to my previous question:

ADTs are entirely public about their unique representation. Belonging in the ADT means satisfying said representation, and so binary methods can rightfully assume that both operands have that exact representation.

Why is the inconsistency?

Thanks.

Answer 1

ADT is a specification. It can have many implementations. For an example, see this answer.

Answer 2

The book clearly states that an abstract data type consists of four things, two of which are concrete - the representation and the implementation of the associated functionality.

The quotes you've posted do not specify when two abstract data types should be considered "equal" or "equivalent", but the quote from page 377 does clearly answer your question that an abstract data type has a single representation.

I think that the phrase "We can substitute an alternative implementation of the Counter ADT" is indeed a mistake or inconsistency on the part of the author, or at least is in need of clarification and synthesis by the author. The author should have said "an alternative Counter ADT with the same type name and abstraction boundary" - that is, the same public-facing interface. It is certainly better to acknowledge this very small mistake or inconsistency and rectify it than to say that these details don't matter, where the author has clearly taken great pains to be precise in the rest of the book. It obviously diminishes the work far more to say that none of the details in the book matter than to say that there is an inconsistent choice of wording on line 32 of page 429.