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

and then defines existential objects in existential types:

A counter object comprises two basic components: a number (its internal state), and a pair of methods, get and inc, that can be used to manipulate the state. We also need to ensure that the only way that the state can be queried or updated is by using one of these two methods. This can be accomplished by wrapping the state and methods in an existential package, abstracting the type of the state. For example, a counter object holding the value 5 might be written

c = {*Nat,
{state = 5,
methods = {get = λx:Nat. x,
inc = λx:Nat. succ(x)}}}
as Counter;


Counter = {∃X, {state:X, methods: {get:X→Nat, inc:X→X}}};

We opens it for example:

let {X,body} = c in body.methods.get(body.state);
> 5 : Nat

and compare ADTs and existential objects:

when programming with ADTs, packages are opened immediately after they are built; on the other hand, when packages are used to model objects they are kept closed as long as possible—until the moment when they must be opened so that one of the methods can be applied to the internal state.

  • What does "when programming with ADTs, packages are opened immediately after they are built; on the other hand, when packages are used to model objects they are kept closed as long as possible" mean?

    They are both opened in the binding parts of the let terms, which can be anywhere (not immediately) after they are built. So their timings seem to be the same to me.

  • What are the differences in the definitions of ADT and of existential objects in terms of existential types, which lead to the timing difference of their opening?



1 Answer 1


You can see an instance of the claimed property in the two definitions of add3.

In the ADT style, add3 is defined as:

let { Counter, counter } = counterADT in
let add3 = λ (c : Counter). counter.inc (counter.inc (counter.inc c)) in
counter.get (add3 counter.new);

As you see, in order to call about inc, one must already have opened the existential package. You cannot write the inc3 function in the "ambient scope", as Counter is not an ambient type, but a type encapsulated in the counterADT package.

You could repackage everything after the first call to inc, and re-open the package before the next call, but that would be somewhat pointless.

In the object style, add3 is defined as:

add3 = λ (c : Counter). sendinc (sendinc (sendinc c)))

Here, the client code does not open the existential package themselves. Instead, each call to sendinc will open the package when it needs to run inc, and will repackage the output. The client could just do the same, but that is not the intent of this style (they would be breaking the abstraction).

So, the confusion might be that you understood the sentence as "the packages are open at a given time", as opposed to "a programmer would be expected to open the package at a given time".

The difference in timing comes from the way we want to use these two mechanisms.

The ADT mechanism is one where we have a single representation, that we wish to hide, while giving some actions to perform on that representation. Because there is a single representation, it is perfectly acceptable to unpackage it once and for all.

The object mechanism is one where we want to potentially allow multiple representations that all share some actions to perform on them. Because we want to allow multiple representations, each package should be responsible for knowing how to perform the abstract action on its concrete representation. If we were to unpackage the existential type early, we would locally be restricted to a given representation.

This becomes very interesting when thinking about binary operations over the packaged type: in the ADT style, the two operands are guaranteed to share the same representation, whereas in the object style, each operand could have its own concrete representation and its own way of implementing the binary operation.


^ This paper, "On Understanding Data Abstraction, Revisited", by William R. Cook gives a lengthy explanation of the difference in power between these two approaches, and is, in my opinion, an excellent read.

  • $\begingroup$ Thanks. Could you also consider cs.stackexchange.com/questions/113428/…? $\endgroup$
    – Tim
    Commented Sep 7, 2019 at 1:25
  • $\begingroup$ I am struggling to understand your reply. There seems to be something that I am assumed to know but I don't. $\endgroup$
    – Tim
    Commented Sep 7, 2019 at 11:06
  • $\begingroup$ Thanks. Is prototype approach in javascript the object mechanism? $\endgroup$
    – Tim
    Commented Sep 10, 2019 at 14:27
  • $\begingroup$ Somewhat? Prototypes are used as an alternative to classes, in order to have some notion of inheritance across objects. Prototypes have a somewhat more dynamic nature (objects get their prototype altered while the program is running), whereas classes should be defined statically in your code. Modern JavaScript has retrofitted a class system on top of the prototype system: it eventually gets compiled down to prototype hacking (at far as I know...), so the two definitely have some overlap in their intent and implementation. $\endgroup$
    – Ptival
    Commented Sep 10, 2019 at 23:41
  • $\begingroup$ In the two counter examples quoted in my post, what is the ADT in the first example and what is the type of the existential objects in the second example? Which does the following quote (in the next comment) says that the ADT is: the type variable Counter bound by let, or is the actual type component in counterADT that is bound to Counter by let? Does the quote in the next comment says the type of the existential object is type name Counter, which is bound to {∃X, {state:X, methods: {get:X→Nat,inc:X→X}}}? $\endgroup$
    – Tim
    Commented Sep 11, 2019 at 0:05

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.