A note on internal interfaces

Dinesh Katiyar

This document discusses the subtleties involved in adding a particular language feature to an existing framework. The target language is an object-oriented language which has a module system fairly similar to that of Standard ML, and a typing discipline that includes subtyping. The feature is what we call “the internal interface”, and this is described in a later section.

1 The language

We describe the language by presenting the abstract syntax of the terms and types of the language. The expressions of the language can be described by the grammar below. The language contains specifications which are basically like the Standard ML signatures, and modules which provide implementations for these specifications.

e : : = x  (variable)
| λx: T.e  (abstraction)
| ee′  (function application)
| (i_{ext}, i_{int})  (module)
| e.l  (module constituent selection)
| Λt <: T.e  (polymorphic term)
| eT  (type application)
i : : = ⟨ℓ_{1} = e_{1}, …, ℓ_{n} = e_{n}⟩ (submodule)

The type system has the following types.

T : : = a  (basic types)
| T → T′  (functions)
| (I_{ext}, I_{int})  (specifications)
| ∀t <: T.T′  (polymorphism)
I : : = ⟨ℓ_{1}: T_{1}, …, ℓ_{n}: T_{n}⟩

2 The feature

Probably the most unusual aspect of the language above is the fact that specifications have two components instead of one. We shall refer to these as the external interface and the internal interface. The latter is the feature that we shall inspect closely. This complexity naturally reflects in the structure of modules as well. The external interface describes the components of the specification which are visible to the external world. This corresponds to the familiar notion of methods of a class in an object-oriented world. The internal interface describes components that are visible to other instances of that specification, and instances of its subtypes. This concept is similar to that of friends in C^{++}.

As one would expect, a subtype of a specification can refine existing components and can have extra components in either interface. Less obviously, a subtype can also move components from the internal interface to the external. This makes sense because the subtype provides all the components of the supertype, except that it is less secretive about which of those can be seen by the external world. The subtyping rule is

\frac{A_{i} <: A′_{i}  B_{j} <: B′_{j}  C_{k} <: C′_{k}}{( ⟨a_{i}: A_{i}, b_{j}: B_{j}, e_{n}: E_{n}⟩, ⟨c_{k}: C_{k}, d_{m}: D_{m}⟩) <:( ⟨a_{i}: A′_{i}⟩, ⟨b_{j}: B′_{j}, c_{k}: C′_{k}⟩)}

A very immediate use of this rule is that it allows one to provide a single implementation for different “views” of the same structure. For instance, given some basic structure with components a, b and c, one might want a type which allows only a and b to be visible to the external world, and another which allows only b and c to be visible. Such types would be very useful for providing restricted access to different users in many database applications. This could be easily achieved by declaring the following types :

V_{1} = ( ⟨a: A, b: B⟩, ⟨c: C⟩)
V_{2} = ( ⟨b: B, c: C⟩, ⟨a: A⟩)
V = ( ⟨a: A, b: B, c: C⟩, ⟨⟩)

Now V is a subtype of both V_{1} and V_{2}, and so instances of V can be used as instances of either V_{1} or V_{2}, and would accordingly provide different extents of visibility.

3 The pros

It is often very convenient to be able to impose certain constraints on all implementations of a specification. This becomes fairly apparent in the implementation of operations that need an argument of the same type (binary operations, essentially). The object-oriented style of operations, where we have x_{1}.bin op(x_{2}) instead of bin op(x_{1}, x_{2}), imposes an inherent asymmetry on the two arguments of the binary operation. Only the internal representation of x_{1} is available for the implementation of bin op and no assumptions can be made about the representation of x_{2}. The internal interface is a mechanism that allows the implementation of a specification to make available some more information about itself to instances of that specification and its subtypes. This information is exactly the set of components that are in the internal interface. This also makes it easier for different implementations of the same specification to interact, since the internal interface provides a sort of peephole into the internal representation. The following examples motivate this concept further.

3.1 Time-stamped events

Consider time-stamped events. A specification for these might look as follows:

Specification time stamped event is

( ⟨event name: string, precedes: time stamped event → bool, …⟩, ⟨⟩)

Our implicit intention is that each structure of type time stamped event will have a local real variable which stores the time of the event. Since the only time-related operation on time-stamped events is precedes, this variable is not part of the external interface. However, if ev1,ev2:time stamped event are two events, then ev1.precedes(ev2) should compare the times of the two events, returning a boolean value. This requires ev1 to have access to the time of ev2. If the function precedes must be implemented using only public operations on its argument, then the only solution is to make the time of an event public. This seems undesirable, since only other time-stamped events need to see the time of an event. The internal interface solves this problem appropriately by letting us specify that every time-stamped event must have a time component. By putting this requirement in the internal interface, we make the time component of one event accessible to the function components of other events, without making time generally available. With an internal interface added, the specification will now appear as follows:

( ⟨event name: string, precedes: time stamped event → bool, …⟩, ⟨time: real⟩)

3.2 Sets with union

Suppose we wish to specify and implement a class of set objects with a union operation. In object-oriented style, the union of two sets is computed by sending one set as an argument to another.

SET = λt.( ⟨ empty : bool, element : t → bool, insert : t → SET(t), delete : t → SET(t),

                               union : SET(t) → SET(t),

intersect : SET(t) → SET(t) ⟩ , ⟨ ⟩ )

If we try to implement the above specification, we run into difficulties with union(s:SET(t)). The problem is that the natural, efficient implementations of union need to iterate over the list of the elements in the argument s, but there is no apparent way to do this using only the public operations allowed on s. One not quite satisfactory approach is to implement sets in a lazy style. While this makes union easy to compute, it becomes difficult to implement empty properly in the presence of intersection. A more realistic approach is to extend the external interface with a function element list which returns a list of all the elements in the set. This has the undesirable effect of making more operations public than required. A more subtle reason for keeping element list out of the external interface is that we expect equality to be a congruence relation, but we do not require equal sets to have the same ordered element list. We may solve this problem using internal interfaces. An internal interface requiring an element list function forces each set to define a function element list. However, this function is not publicly visible – it may only be used by other set objects. So our specification would be as follows.

SET = λt.( ⟨ empty : bool, element : t → bool, insert : t → SET(t), delete : t → SET(t),

                               union : SET(t) → SET(t),

intersect : SET(t) → SET(t) ⟩ , ⟨ element list : List(t) ⟩ )

4 The cons

The internal interface seems to provide a clean and reasonable mechanism for revealing as many details of the internal representation as may be useful for the implementation of the operations. However, a closer study reveals that everything isn’t quite as nice as it seems. The structural approach to subtyping that we adopt leads to some unexpected behaviour with respect to internal interfaces. Consider the following example.

S_{1} = ( ⟨e_{1}: T_{1}⟩, ⟨i: T_{i}⟩)
S_{2} = ( ⟨e_{2}: T_{2}⟩, ⟨i: T_{i}⟩)

Now some module M_{1} implementing S_{1} can actually access the i component of any instance of S_{2}. This happens because both S_{1} and S_{2} are subtypes of the specification S.

S = ( ⟨⟩, ⟨i: T_{i}⟩)

This implies that any instance of S_{2} is also an instance of S and therefore, its internal interface is visible to all instances of the subtypes of S, M_{1} being one such instance. So even though S_{1} and S_{2} can be radically different specifications, every common component in their internal interface is visible to instances of each other. This gets even more surprising when one uses the fact that a subtype can move components to the external interface. Consider the following.

S_{3} = ( ⟨e_{3}: T_{3}, i: T_{i}⟩, ⟨⟩)

Now a module M_{3} implementing S_{3} can access the internal i component of any instance of S_{2} just because it happens to have an i component itself. While this may be put off as one of the accidents that one would expect from structural subtyping, it does seem to be undesirable. Another problem with using the internal interface is related to type inference. There is a certain degree of circularity here. To infer the type of an interface, one needs to infer the types of the components. But the components can involve the selection of components from the internal interface of some other module, and the well-formedness of this depends on the type of the interface, which is what we were inferring in the first place.

A Typing rules without the internal interface

The rules are fairly simple in this case. The subtyping rule allows for specialisation of existing components and addition of extra components. The typing rules for the specification and for component selection use the types of the components in a straightforward way.

(spec subtype)  \frac{⊢ A_{1} <: A′_{1}  …  ⊢ A_{n} <: A′_{n}}{⊢ (a_{1}: A_{1}, …, a_{n}: A_{n}, …) <:(a_{1}: A′_{1}, …, a_{n}: A′_{n})}

(spec type)  \frac{Γ ⊢ e_{1}: A_{1}  …  Γ ⊢ e_{n}: A_{n}}{Γ ⊢ (a_{1} = e_{1}, …, a_{n} = e_{n}): (a_{1}: A_{1}, …, a_{n}: A_{n})}

(comp selection)  \frac{Γ ⊢ e_{i}: A_{i}}{Γ ⊢ (a_{1} = e_{1}, …, a_{n} = e_{n}).a_{i}: A_{i}}

B Typing rules with the internal interface

The rules here are more involved. The subtyping rule allows for the “externalization” of internal components. One has to use the type of a specification in typing its components. So the environment now is a pair (Γ, T_{I}) where Γ is the usual environment consisting of assertions of the form x: T and t <: T, and T_{I} is the type of the smallest enclosing module. And the selection of an internal component has to make sure that it is allowed, by looking at the types of the “caller” and the “callee”. For brevity of the rules, we use the abbreviations

\begin{aligned}X & ≡ & ( ⟨l_{1}: E_{1}, … l_{j}: E_{j}⟩, ⟨m_{1}: I_{1}, … m_{k}: I_{k}⟩) \\ x & ≡ & ( ⟨l_{1} = e_{1}, … l_{j} = e_{j}⟩, ⟨m_{1} = i_{1}, … m_{k} = i_{k}⟩) \end{aligned}

(spec subtype) \frac{⊢ A_{i} <: A′_{i}  ⊢ B_{j} <: B′_{j}  ⊢ C_{k} <: C′_{k}}{⊢ ( ⟨a_{i}: A_{i}, b_{j}: B_{j}, e_{n}: E_{n}⟩, ⟨c_{k}: C_{k}, d_{m}: D_{m}⟩) <:( ⟨a_{i}: A′_{i}⟩, ⟨b_{j}: B′_{j}, c_{k}: C′_{k}⟩)}

(spec type)  \frac{\begin{matrix}(Γ, X) ⊢ e_{1}: E_{1} … (Γ, X) ⊢ e_{j}: E_{j} \\ (Γ, X) ⊢ i_{1}: I_{1} … (Γ, X) ⊢ i_{k}: I_{k} \end{matrix}}{(Γ, T) ⊢ x: X}

(ext comp selection)  \frac{(Γ, X) ⊢ e_{i}: E_{i}}{(Γ, T) ⊢ x.l_{i}: E_{i}}

(int comp selection)  \frac{\begin{matrix}(Γ, X) ⊢ i_{i}: I_{i} \\ ⊢ T <: X \end{matrix}}{(Γ, T) ⊢ x.m_{i}: I_{i}}