Why are ADT packages opened immediately after they are built, while existential objects opened as late as possible?

cs.stackexchange https://cs.stackexchange.com/questions/113429

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

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;

where:

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?

Thanks.

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top