HLL Primitives

[Brian T Rice]

Hi Fare and Tunes members,

For reference, the documentation discussed here is quite small, and
published at http://tunes.org/HLL/hlm/ . I am combining this with the "HLL
Primitives" page at http://tunes.org/HLL/primitives.html .

I have a series of questions about theses points, mostly for clarification
of the intent of them, which should result in some better specifications
that we could work from.

Basically, my general intent here is to detail the different kinds of
meta-objects and semantics that need to be implemented to realize HLL
(read: "Tunes High-Level") semantics. So I first will start with the
primitives:

1) Applying Functions

The idea is obvious, but with the caveat that in Tunes, we treat functions
as we would lambda's in Scheme, roughly-speaking. That is, a
single-argument function is equivalent to an attribute on an object for
that function. Now, the unclear part is for multi-argument functions and
for dispatch.

First, are multi-argument functions considered to be attributes? If so,
are they the attributes of the type of a quoted term? This quoted term
would be an Abstract Syntax Tree node: we would have a group of types for
this, I guess.

Dispatch also seems to be a factor, since an "ordinary" attribute is a
function that dispatches on an object's identity (or value if
referentially-transparent), so to speak, but some kinds of dispatch depend
on structural properties of the arguments. Pattern-matching seems like an
obvious example, but it occurs to me that so are "lookup" policies, or
anything that uses type information. So these are attributes whose values
must be checked.

2) Abstracting terms

Here's another obvious idea, except now that we have dispatch factored
out, I can look at the examples on the HLL page and realize why they're so
varied. But more to the point, I suppose that this is the constructor for
the annotations on syntactic types mentioned above. Does this make sense?

Unfortunately it's not clear to me how the information gets added (in
terms of our annotation idea and types and such) to specify what
constraints are needed to trigger the abstraction/annotation.

3) "Defining typed constructors"

I'll say up front that this phrase is not obvious nominally to the English
audience here, or maybe those who have not used Coq or wherever this term
came from. There is also the notion of trust explained here which seems to
belong elsewhere, but it's explaining something. If I can tease that
apart, I will.

Anyway, it seems analogous to defining "nullary" functions which provide
new terms annotated to have a given type, but having somehow incomplete
information, for the purpose of providing an object which axioms may speak
of. I'm reminded of the Epsilon Calculus reference you make to "providing
witnesses". This function produces, not quite a witness, but a universal
representative for the type, and raises lots of questions about typing in
Tunes.

For example, we would need at least somewhat-special support for axioms as
term types, since we create a sort of "exemplar" which has minimal
information for the specific purpose of providing enough information to
define the type that it "belongs to" or "is a witness for". So whatever
these axioms specify about the object(s) has to hold for anything else
using that constructor.

There's also the question of different kinds of types. Obviously there are
predicate types and then enumerated and then axiomatized classes of
objects. With these kinds combined, a single object has infinitely many
types. I'm not going to ask any questions now, because you'll just wave
your hands around and pretend that all the issues are addressed already
and "it's just a simple matter of coding". :P

There has to be a primitive to draw from this paragraph, or it simply
doesn't belong on that Primitives page. So, we need some primitive that
expresses universal quantification *independently* from the abstraction
primitive. Note that the dispatch argument effectively separates universal
quantification from the abstraction primitive, at least to some extent.
Anyway, this is universal quantification of "output" vs. "input", so the
argument is even farther removed. What primitive do you think arises here?

4) Evaluation strategy

We only see two issues mentioned here: future vs. actual, and
side-effecting vs. non-side-effecting. These are useful issues to address,
but they seem like just artifacts of current terminology rather than a
real definition.

About forcing vs. delaying objects, this seems like the Search phase of
the meta-level architecture. See:
http://tunes.org/HLL/architecture.html#search

so I don't see a point in making this a primitive, since you can provide
varying strategies over it. Would you want this to be the basis for
strategies? Would it be a default to be lazy and provide a "force"
primitive? The opposite concerning "delay" in Scheme seems to be
ineffective. A "force" primitive might overcome that by working
recursively on its arguments.

As far as Side Effects, I don't see any obvious semantic primitive to be
drawn from this. The text even states that this is not a clear issue. So
there must be some "containment" kind of primitive you're after, or maybe
higher-order rewrite (rewrite of rewrite rules in order to satisfy
constraints that aren't part of the declarative specification). But even
higher-order rewrite isn't really a separate primitive; maybe some
separate form of quotation if that's needed.

Laziness interacting with 'effects' is obviously a concern for the timing
of things, so these issues are related. Perhaps laziness or forcing is an
attribute somehow of attributions themselves, so that it would apply
equally to results and side-effects. Even so, this does not have simple
consequences.

...

So, finally (well, not so finally. I haven't reached the HLL- questions
yet), we have two of four "basic constructors" which don't have an obvious
specification yet. Let me know what your original thoughts were, or maybe
if things were thrown together and what the current state of knowledge
tells us to do with this.

-- 
Brian T. Rice
LOGOS Research and Development
mailto:water@tunes.org
http://tunes.org/~water/