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 =
{new = 1,
get = λi:Nat. i,
inc = λi:Nat. succ(i)}}
as {∃Counter,
{new: Counter,
get: Counter→Nat,
inc: Counter→Counter}};

> counterADT : {∃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 =
{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,

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?



1 Answer 1


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

  • $\begingroup$ Thanks. Just added more context. Why do the last two quotes seem to say an ADT can have only one representation? $\endgroup$
    – Tim
    Commented Sep 10, 2019 at 21:14
  • $\begingroup$ As I explained in a comment to a past question, I take issue with this kind of close reading of TAPL. $\endgroup$ Commented Sep 10, 2019 at 21:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.