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

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 ﬁrst 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}};

{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}};

{new:Counter,get:Counter→Nat,inc:Counter→Counter}}


in complete conﬁdence 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 ﬂexibility. These advantages are complementary; nei- ther style dominates the other.

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.