Tunes HLL Semantic Primitives

The HLL provides a set of basic constructors. This set should enable it to emulate any kind of other set of constructors. Editor's Note: we need more reasons than just this to pick a set of pseudo-primitives.

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 (first-class) object. In other words, functions will be used and bound according to the same protocols as ordinary objects.

Abstracting terms

The next basic constructor is typed abstraction on any sub-object of an expression, using any type system, which allows the creation of new functions, i.e. lambda-expressions, from an arbitrarily (but strongly) typed lambda calculus, which gives something like:
lambda (x).sin(2*x+1)
method (x) ; sin(2*x+1) ; end method ; (using Dylan syntax)
fun x -> sin(2. *. x +. 1.) (using OCAML syntax)
[x:Real] sin(2.0 *. x +. 1.0) (using Coq syntax)

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.

  For example, if you have access to the type of terms for programs and data, then you can use standard "compilers" that construct objects from tools; among them are creations of inductive definitions and such 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 latter case, specifications may include how impure the function is.