The Tunes HLL Semantics
General concepts
- Objects
- The language manipulates objects.
- Any identifiable abstraction in the system is an object.
- Attributes
- Among objects, some are attributes, or equivalently, functions.
- Note that these are just particular objects, and thus share other
features with objects.
- Objects and attributes operate on each other, and isomorphically,
you can have functions operate on objects.
- By duality, either the object or the attribute may be considered as the
function, and the other, the argument. Actual implementation may be
object/attribute/object space/attribute space dependent.
- For example, you may define that objects may have a "creation date" as an
attribute, and then define that for such object, it corresponds to a
date-stamp in the file-system, or that you may look it up in a hash-table,
or that it is else undefined.
You can also define the type of an object
(according to such type system).
Anything that associates a value to an object is called indifferently
an attribute or a function.
- Active annotations
- As an example of the power of annotations context, in some metaspaces,
objects may have active attributes, that are evaluated together with
the object
- Trivial examples include scheduling/usage information as call counter
for a function, notification of one's login to others, etc.
- actively annotating objects may be a fairly standard programming technique:
to parse a text, dynamically write annotations it during its being read; active
annotations to the byte reader may correspond to the program's state; it may
then become trivial to write programs that depend on the past and
future of the local input context.
- but this feature should bed made static (i.e. removed from the dynamic
context) whenever not needed, because it ampers good implementation.
- Context
- An object is never considered alone, but in a context, or space,
that describes the meaningful aspects of the object:
the context gives the full semantics of the object.
- Only meaningful constructors may be used on objects; for example, even
if an object could be modified, by considering it in a context where modifying
it is excluded, it is made read-only; by considering an object in a context
which has a modifier method, the object is made read-write.
- The context may also explicitly defines specifications of the object,
so that the system may simplify programs in a way that will keep the
semantics by doing transformations that let meaningful things unchanged, while
limiting resource allocation in unmeaningful dependences.
e.g. if your methods for a list maintain a count of list elements that
you don't need, it may be ripped off automatically by the system if not
declared meaningful somewhere. Note that different views on the "same" object
may consider different things as meaningful...
- Access rights
- Access rights are implemented through HLL context and scoping.
An object is accessible by another object if and only if it is in
that other object's HLL context.
- So an object actually exists in the system if and only if there is a
path of objects that each allows access to the next, beginning from the
boot program, and ending with the considered object.
- You limit the rights by just wrapping the object with evaluators that
will allow access only to parts of existing aspects of the object.
- The compiler or run-time system should inline any frequently evaluated
wrapping code, so this is no performance hit.
- An object that verifies or inlines accesses is called a meta-object.
- In particular, read-only or even constant objects are encouraged
(by not publishing any way to modify the object in any context), because
of their semantics much nicer to express and implement (i.e. much simpler
meta-objects).
- When side-effect functions are hidden from the context, an object may be
completely read-only. Particularly, you can't change an attribute's value if
you don't have the proper "rights".
- There is no such thing in the OS as builtin capability lists or
passwords, but you can still use those lame unsecure mechanisms, if you're
masochistic and paranoid, through proper wrapping.
- Typing
- Being able to access objects does not mean you can combine them blindly.
To actually combine two objects or evaluate one someway, you must
somehow have the system trust such operation may not ever result in a crash.
- Thus, two objects can connect if only if there exists meta-objects that
agrees.
- The set of operations that a meta-object allows for an object is often
called the object's type.
- The meta-object is accordingly called a type system.
- Verifying that objects' type allow them to combine is called
to typecheck the combination.
- An object may have no relevant type in some type system,
and thus not be able to combine with other objects in this type system;
but it may also have types in other type systems, and thus be able to combine
in these.
- Proofs
- When the type-system is simple, there may exist a decidable
algorithm to determine any object's type.
- But when the type-system is rich enough, it is no longer decidable
(or not decidable in any reasonable time), and objects must come with
some externally generated proof that they typecheck.
- We then talk about proofchecking.
- Using the Curry-Howard isomorphism, for example, we automatically have
proof checking of full (undecidable) computational logic as decidable type
checking of proof terms (see the Coq proof environment).
- A proof can be an actual logical proof, some strong type checking,
a RSA signature, a bit capability list, or anything a meta-object may ask,
even just the object having been accessible from some secure one.
- Security
- The weaker the checking, the lower the security.
- The most secure type-system is the one that has got the least holes
and flaws.
- To ensure security, the system must distrust any low security object,
and isolate it from other objects that it might endanger.
- In particular, users do not have access rights to arbitrarily modify
standard type systems and fake security, though these type systems may come
with standard proved tools to extend them.
- You may also create your own type-systems in a context that trusts you
enough (e.g. a context in which you have been isolated from other objects).
Standard Basic constructors
The HLL provides a set of basic constructors.
This set should enable it to emulate any kind of other set of constructors.
- Applying Functions
- As in SELF or LISP, the basic constructor will be applying an
attribute/function to an object.
- As in Scheme or ML, and unlike SELF or LISP, the attribute/function
is not a meta-level symbol, but a zero-level object.
- Abstracting terms
- The next basic constructor is typed abstraction on any sub-object of
an expression, using any type system, which allows to create new functions.
i.e. lambda-expressions from an arbitrarily (but strongly) typed lambda
calculus, which gives something like
lambda (x).sin(2*x+1),
or (using Dylan syntax) method (x) ; sin(2*x+1) ; end method ;
or (using CAML syntax) fun x -> 2 *. x +. 1
or (using Coq syntax) [x:Real](2 *. x +. 1)
- Defining typed constructors
- You can define typed constructor axioms; but they won't be trusted
unless you are trusted too; that is, trusting the axiom creator
is part of any proof.
e.g. If you have access to the Coq-like object "Set" (the type of
constructible data objects, that correspond to actual programs and
their data in Coq).
e.g. you can use standard "compilers" that construct objects from tools;
among them are creations of inductive definitions and suches (see Coq)
or (if you're trusted enough in the context), you can associate low-level
objects to a high-level specification without a proof.
[.....]
- Standard constructors (including all the previous) can be selectively
trusted, so that contexts can be very limited (e.g. only applying functions
among those from a list), or very open (trusting all the inherently secure
constructors plus a list of axioms/trustees)
- Inductive definitions (as in Coq) may be used as a secure way to construct
new types.
- Evaluation strategy
- Objects can be future or actual;
- you can explicitly force or delay objects, or do it implicitly by
just annotating a function object to say that its argument may be future,
or should be actual.
- functions can be pure or impure (without or with side-effects);
in the later case, specifications may include how impure the function is.
- .....
Standard Library of language extensions
- The standard library of extensions provides standard objects for use in
various contexts.
- For the User Interface part, we should collaborate tightly with the UI
subproject.
Semantic Difficulties
- Syntax is definitely NOT a difficulty. A proper system should
be able to simulate any syntax. The problems are in the semantics,
which is quite another thing.
- The most difficult thing (I think) is about administrative, weak
pointers, that are often useful for performant algorithm, but do not count to
determine the object's usefulness. e.g. a device driver or event
handler of any kind must register to the event provider/resource allocator,
which in turn may (or may not) need have pointers back to the handler (e.g.
linked list of handlers); but this back-pointer does NOT represent
that the driver/handler is actually needed.
- Then, there is the problem of the efficiency of dynamic annotations,
all the more when it comes to annotating light objects:
what mechanisms can be used to annotate terminal objects ?
Reserving an annotation list for each object would be quite too costly
(and a C++ like bloat).
And what about annotating annotations ?
It seems that somehow, the system should (dynamically) differentiate
coarse-interfaced objects (including single integers that are being
watched by external humans) from lightly interfaced ones. The former
would have an "annotation" field, while the latter would have a more
expensive mechanism for annotation (e.g. using hashed association tables),
or would have to be annotated through a coarse-object wrapping.
To Do on this page
Make first proposals.
Settle full HLL semantics.
co-develop a (some?) standard syntax(es?) for these.
Find out how multiple type systems can be made compatible...
Find some nice semantics for annotations...
Separate annotation mechanisms from annotation resolving policies...
Find out how to separate or merge the "useful/administrative" or
"in context/out of context" information.
Wait for feedback, as usual.
Back to the Tunes
HLL Subproject.
Page Maintainer:
Faré
-- rideau@clipper.ens.fr