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.
- Context
- An object is never considered alone, but in a context, or space,
that describes the meaningful aspects 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
- Access rights
- Access rights are implemented through HLL context and scoping. No need for
such things as capability list or passwords (though you can still use those if
you're masochistic, through proper wrapping).
- You limit the rights by just wrapping the object. The compiler/run-time
should inline the wrapping code, so this is no performance hit.
- In particular, read-only objects are encouraged (by not publishing any way
to modify the object in any context).
- 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".
- Typing
- Each object has a type (or many types), as associated by type attributes.
Types specify objects' properties.
- Using the Curry-Howard isomorphism, we automatically have proof checking
as type checking, if we use a good type system
- Two objects can connect only if, by some way, they can typecheck/proof
check (static proofs are possible).
- A proof can be an actual logical proof, or just a RSA signature checking.
- As a particular case of access rights, you cannot modify a type attribute
if you do not have enough rights. You needn't have full rights to add personal
annotations to the typing, though.
- .....
Standard Basic constructors
- Applying Functions
- As in SELF or LISP, the basic constructor will be applying an
attribute/function to an object.
- As in Scheme, and unlike SELF or LISP, the attribute/function is 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.
- 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.
- 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.
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
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