work on HLL

Fare Rideau
Wed, 7 May 1997 13:06:14 +0200 (MET DST)

>: David Manifold

Dear David,
   thanks a lot for forcing me to explain the dark parts of Tunes.
It helps us all understand what we want to do.


> What is an attribute?  I can't seem to figure out the difference between
> this and a function.  You say the implementation may make the difference
> meaningless; but I don't quite understand the theoretical difference.
An attribute can be conceptually thought of as a memoized function:
you have a function that associates some abstract value to some objects,
but want to remember that value permanently without having to recompute it.
* If the function is pure, then there is no semantical difference
 between an attribute and a function
* If the attribute gets garbage collected,
 then all the individual memoized information gets garbage collected;
 if an object gets garbage collected, its attribute disappears, too.
* If you want to be able to associate varying values to objects,
 then use a reference as the attribute;
 that's the ML way of making side-effects orthogonal to other computations.
* You don't want people to read an attribute?
 Just don't export the attribute reader to anyone's scope.
* The exact implementation of attributes is undefined;
 might be fields added to the object's representation;
 might be information nodes inserted in the structure;
 might be a centralized or decentralized association list or hash table;
 might be just anything you can imagine,
 as long as the overall abstract semantics is the same.
 the responsibility is left to implementers (with programmers' hints welcome).

Let's take some usual examples:
* You've got a structure that you'd want to pretty-print, display, or edit.
 Then, you're going to define for every "node" in the structure
 attributes that describe where and how it will be displayed
 (font, indentation, size, color, whatever).
* the system has a concept of "user", built in some module.
 You want to add some accounting/logging information about users.
 No need to rewrite the module that define users.
 Just define a new attribute of users.
 Same goes with password systems, etc.
* you want to type a program. Give each node a type attribute.
 [Note: programs are stored abstract structures, not ASCII]
* you are not satisfied with the way the pretty printer manages
 parts of your program; you ask it to remember the layout,
 or particular layout tactic to use for such parts of the program.
* you want to comment a program.
 Annotate its structure with comments in french, german, chinese, martian.
* you want to translate a program.
 Annotate each node with all the meanings you could find about it,
 before you can understand it and synthetize a translation.


> Does an object have one "real" context, with all the other contexts being
> just views onto the "real" context that limit and restrict (by removing
> some semantics)?

I think that the very principle of reflection is
that there is no "real" context.
This would imply one "real" implementation.
Rather, every object has well-defined semantics
in the context in which it is accessed,
but has some floating implementation:
you can then migrate the implementation
("hey, there's an idle Alpha workstation, let's speed up computations!").
So basically, there are only views on objects.
Of course, if you manage to get a very low-level view on the object
("how does this object run on *this* host using *this* encoding),
then you can be fairly sure that it's "real";
however, as soon as you stop looking at it,
the object might migrate away.


> Does an object have one "definition" meta-object that defines
> specifications for the object?  Is this the same as the "real" context?

Well, a "same" object may have lots of different meta-objects,
as long as they are compatible with each other.
An object gets started by a definition inside some theory;
then meta-object can be specified that refine the abstract semantics
of the object into more concrete operational semantics,
until we get to the bare-bones level where the object is executed.

For both security and efficiency reasons,
not everyone is allowed to arbitrarily manipulate meta-objects:
meta-objects control the internals of the object;
i.e. not everyone can intercept the keystrokes on a terminal
by adding a meta-object to the terminal handler.
Adding an attribute to an object might involve adding a meta-object;
hence not everyone can add every kind of attribute to an object.


> Do you refer to "type-system" and "context" to be the same meta-object,
> that defines semantics of the object?  Are these words interchangeable?

Surely, the issues of typing are important to the semantics of the system,
hence the type system is one of those "meta-objects".

Well, I feel that "meta-object" is too vague a term,
as anything that's at a "meta" level seems to be called that way.
Maybe we should coin new terms to describe precisely what we mean.


> At what point is an object under scrutiny of correctness; i.e. when is it
> proven?  Never, until user requested; or automatically, when created or
> defined?

Well, the system will have user-defined invariants,
and every "context" will include its set of invariants.
The system will guarantee that these invariants are always enforced.
So that when an object is used in a context where correctness of the
object wrt to some specification is part of the invariants,
then you can be fairly sure that the object correctly implements
its specification.
Of course, the system may be unable to enforce some invariants,
but then, it won't provide you the context you want;
only by giving the system the proper hints, you may achieve what you want.

Hence, you write a specification, then ask the system
"instantiate this specification for me", giving it a tactic/meta-object,
or letting the default tactic run.
The system will either manage to instantiate the specification, or fail
(or you may stop it when it still hasn't answered and you are bored).
*Of course*, the instantiation tactic may involve interactive computations
and proofs.


> Is this an example of abstraction: taking an integer addition function and
> abstracting it to work with floats?

If the addition function is used in a context such that
the fact that the numbers are integers rather than float
does not intervene, then it is a valid to abstract the number
type into something more general than integers.
You reapply the said abstracted object to the float number type,
but the result is not the abstraction itself;
If the overall abstract semantics of the new object are the same
as those of the original one (i.e. you were doing computations on integers,
and are now using the FPU to speed them up),
then it is what I called a "migration" of the original object.

Hope this helps,

== Fare' -- -- Franc,ois-Rene' Rideau -- DDa(.ng-Vu~ Ba^n ==
Join the TUNES project for a computing system based on computing freedom !
                TUNES is a Useful, Not Expedient System
URL: ""