|
|
|
Sponsored Link •
|
Summary
I thought I would share my latest attempt at writing a white paper describing the implicit behavioral subtyping mechanism I am using for the current Heron prototype (yes you can download it at http://www.heron-language.com/ ). Any comments would be appreciated.
|
Advertisement
|
The primary problem with structural subtyping, semantic malformance (e.g. contract violations), can be alleviated by introducing behavioral constraints into the specification of the subtype. This paper describes a mechanism to implement implicit behavioral subtyping, by applying structural subtyping as well as precondition and postcondition assertions to traits.
This work is demonstrated using the Heron programming language. Heron is a statically typed experimental programming language, which is implemented using a Heron to C++ translator, HeronFront. The HeronFront tool translates trait constructs written in Heron to classes with the implicit behavioral subtyping semantics described in this paper. Apart from the introduction of traits and some rather minor syntactic difference, the Heron langauge shares C++ syntax and semantics.
Traits were first described by Schärli et al. [Sch03] as a compositional model for structuring object oriented programs. A trait is a construct similar to Java interfaces in that it is used to characterize the function signatures (sometime described as a method dictionary) for a set of types, and can be used as a polymorphic reference which binds to a conforming object. The Heron trait has similar syntax to traits in Scala 1.0 [Ode05] which has since been replaced by mixin-classes. The function signatures that it provides are known as the required functions, and are sometimes referred to as "super-sends" because they delegate the implementation to the super type. Unlike a Java interface, a trait may also have member functions which call other member functions or one of the required functions. The member functions of a trait are referred to as extension functions to clearly delineate them from class member functions.
Structural subtyping (also known as implicit subtyping, signature based polymorphism, and colloquially as duck-typing), is a method of deducing a subtype relationship at either run-time or compile-time. Trait instances in Heron are associated with super types using a structural subtyping mechanism.
Implicit subtyping has several advantages:
Implicit subtyping can be achieved, rather surprisingly, in the C++ programming language using only template meta-programming techniques [Dig04], and more conveniently with macros [Tur05].
Several dynamically typed languages support structural subtyping but only a few statically typed language provide support for it. The main languages being the various ML dialects. A now discontinued extension to the GCC C++ compiler, did support a similar structure also called signatures [Bau97].
Except where stated, Heron statements have precisely the same syntax and semantics as C++. HeronFront does a literal mapping of most statements from Heron to C++ with no checking.
Heron traits are divided up into four sections (inherits, requires, public, private), and optional template parameters. Heron also introduces two new keywords: _result and _override.
The _result keyword corresponds to a variable which is implicitly declared at the beginning of every non-void function in a trait. Every non-void function in a trait also contains the implicit statement "return _result;" as a last line. A return statement takes on a new meaning in Heron, it assigns the expression to _result, and then jumps to the end of the function, so that the postconditions can still be evaluated.
The _override keyword corresponds to a delegation of the current function to the appropriate function in the super-type. This means that a required function in a trait with no preconditions and posconditions can be written equivalently either as:
trait T {
requires {
def f() : int;
}
}
trait T {
requires {
def f() : int {
_override;
}
}
}
The actual C++ code generated for the _override keyword would resemble more or less:
_result = _get()->f();
The _get() reserved member function returns a pointer to a class which forwards the function to the bound object.
An instance of a trait in Heron can bound to any concrete object which provides the appropriate function signatures, for example:
/*
Heron code which we assume is translated into a C++
header file using HeronFront and #included
trait MyTrait {
require {
def set(int n);
def get() : int;
}
}
*/
class MyClass {
public:
MyClass() : m(0) { }
void set(int n) {
data = n;
}
int get() {
return data;
}
private:
int data;
};
int main() {
MyTrait t;
MyClass c;
t = c;
printf("%d\n", t.get()); // outputs 0
printf("%d\n", c.get()); // outputs 0
t.set(1);
printf("%d\n", t.get()); // outputs 1
printf("%d\n", c.get()); // outputs 1
}
statement ::==
any legal C++ statement
function-param ::==
type identifier
function-return-type ::==
: type
function ::==
def identifier ( function-param* ) function-return-type?
{ statement* }
function-or-type-or-macro ::==
function | class | trait | macro
template-parameters ::==
[ meta-type identifier ]
inherits-section ::==
inherits { type-specifier* }
requires-section ::==
requires { function* }
public-section ::==
public { function-or-type-or-macro* }
private-section ::==
private { function-or-type-or-macro* }
trait ::==
trait identifer template-parameters? {
inherits-section?
requires-section?
public-section?
private-section?
}
Implicit subtyping has the disadvantage that syntactic conformance can occur in types which do not share semantics. An illustrative example can be found when comparing LIFO stacks and FIFO stacks. This is illustrated in Example X.
trait Stack[T : type] {
requires {
def push(T x);
def pop();
def top() : T&;
def is_empty() : bool;
}
}
trait FifoStack[T : type] {
inherits {
Stack[T];
}
}
trait LifoStack[T : type] {
inherits {
Stack[T];
}
}
The problem occurs when we try to execute some algorithm which expects a FifoStack, but instead receives a LifoStack.
The proposed solution to the problem of structural conformance with semantic malformance, is to introduce contract verification, in the form of precondition and postcondition assertions. In other words implicit behavioral subtyping.
A contract is the name collectively given to the preconditions, postconditions, and invariants, which a type is expected to satisfy. A contract can be used to characterize the behavior of a type [Mey97], [Lis99]. Rather than creating a brand new syntax, including keywords, Heron relies solely on the C++ language facilities to enable the programmer to define how they choose to verify the preconditions and postconditions.
Contract verification can be achieved by writing the required function using the explicit syntax and the _override keyword, and inserting precondition and postcondition checks before and after respectiviely the _override call, as follows:
How the pre and post functions are implemented is up to the programmer, but they can be implemented as macros create two new macros as follows:
#define pre(expr) assert(expr && "precondition violation") #define post(expr) assert(expr && "postcondition violation")
Implicit behavioral subtyping is a stronger form of structural subtyping which introduces precondition and postcondition assertions into the verification. The following example shows the differentiation between a FIFO stack and LIFO stack
trait Stack[T : type] {
requires {
def push(T x);
def pop();
def top() : T&;
def is_empty() : bool;
}
}
trait FifoStack[T : type] {
inherits {
Stack[T];
}
requires {
def push(T x) {
if (!is_empty()) {
T old = top();
_override;
post(old == top());
post(!is_empty());
}
else {
_override;
post(!is_empty());
}
}
def pop() {
pre(!is_empty());
_override;
}
def top() : T& {
pre(!is_empty());
_override;
}
}
}
trait LifoStack[T : type] {
inherits {
Stack[T];
}
requires {
def push(T x) {
_override;
post(!is_empty());
post(x == top());
}
def pop() {
pre(!is_empty());
_override;
}
def top() : T& {
pre(!is_empty());
_override;
}
}
}
The difference in behavior between the two kinds of stack ADT's, can be expressed as whether or not push affects the status of the top, in the case of a non-empty stack. This is a non-trivial assertion, and to express it we need the full the range of the language. To achieve this, Heron allows any C++ statement to be used before or after the super-send (i.e. the _override keyword).
Heron currently provides no convenient syntax for verifying invariants, however this should change in the next major release of HeronFront. See the section "Future Direction" for more information. For the time being an invariant can be simply explicitly checked after each required function along with the postconditions.
Common OOPL implementations implement runtime polymorphism using the mechanism of virtual functions. One difference with Heron is that it implements runtime function dispatch externally to the class, rather than through the use of virtual function. This means that a pointer to a function dispatch table is associated with the trait instance rather than the object instance. This approach carries several advantages
HeronFront generates C++ classes which support signature matching semantics. This is accomplished using template meta-programming techniques. Every trait is associated with a single class which has a template constructor, a template assignment operator, and a dispatcher object along with the expected required and extension functions. The dispatcher object is implemented as a concrete subtype inheriting from an abstract supertype which contains a pure virtual function for each required function in the trait. The extension functions are implemented directly in the trait class. Example X contains an example of code generated for a simple trait.
trait Indexable[type Element] {
requires {
def get(uint n) : Element {
assert(n < count());
_override;
}
def set(uint n, Element x) {
assert(n < count());
_override;
}
def count() : uint;
}
public {
def is_empty() {
return count() == 0;
}
}
}
Here is the code generated by the most recent version of HeronFront:
template<class Element >
struct Indexable {
template<typename _T>
Indexable(_T& _x) {
new(&_data) _concrete<_T>(&_x);
assert(sizeof(_concrete<_T>) <= (sizeof(void*) * 2));
}
struct _abstract {
virtual Element get(uint n) = 0;
virtual void set(uint n, Element x) = 0;
virtual uint count() = 0;
};
template<typename _T>
struct _concrete : _abstract {
_concrete(_T* x) : _object(x) { }
Element get(uint n) {
Element _result;
#define _override return _object->get(n)
assert ( n < count ( ) ) ;
_override ;
return _result;
#undef _override
}
void set(uint n, Element x) {
#define _override _object->set(n, x)
assert ( n < count ( ) ) ;
_override ;
#undef _override
}
uint count() {
return _object->count();
}
_T* _object;
};
_abstract* _get() { return reinterpret_cast<_abstract*>(_data); }
_abstract* operator->() { return _get(); }
void* _data[2];
// requires section functions
Element get(uint n) {
return _get()->get(n);
}
void set(uint n, Element x) {
_get()->set(n, x);
}
uint count() {
return _get()->count();
}
// public non-delegated member functions
bool is_empty() {
bool _result;
return count ( ) = 0 ;
return _result;
}
};
This code is quite complex, but the most important characteristics are:
The largest gap in this work is the inability to express a class invariant in a single location. Class invariants currently have to be verified with the preconditions and postconditions (arguably either one is sufficient). A class invariant is an example of a crosscutting concern. Direct support for class invariant verification can be added to a programming language such as Java or C++ with relative ease, but this ignores the more general problem of the inability to express crosscutting concerns. Ideally a language would provide such a mechanism which can then be used to implement invariant verification, along with other crosscutting concerns.
It is the author's desire to introduce an extremely minimal form of aspect oriented programming support [Kic97] into Heron in the form of macros which are automatically inserted around each member function. These macros would be ideally associated with a class, or a module, and can be inherited from one class to another.
There is a possibility of introducing a mutable state into traits in the context of Heron.
Special thanks to Peter Grogono. Thanks also to the many people at Artima.com who have patiently discussed the topics of structual and behavioral subtyping with me.
Have an opinion? Readers have already posted 35 comments about this weblog entry. Why not add yours?
If you'd like to be notified whenever Christopher Diggins adds a new entry to his weblog, subscribe to his RSS feed.
 | Christopher Diggins is a software developer and freelance writer. Christopher loves programming, but is eternally frustrated by the shortcomings of modern programming languages. As would any reasonable person in his shoes, he decided to quit his day job to write his own ( www.heron-language.com ). Christopher is the co-author of the C++ Cookbook from O'Reilly. Christopher can be reached through his home page at www.cdiggins.com. |
|
Sponsored Links
|
Digg
del.icio.us
Reddit