HLL Primitives

[Francois-Rene Rideau]

Dearest Brian,

re: your discussion about
	http://tunes.org/HLL/hlm/
	http://tunes.org/HLL/primitives.html

> [...] 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. [...] start with the primitives [...]

> 1) Applying Functions

> First, are multi-argument functions considered to be attributes?

As for Ulrich's remark that you harshly rebuked, I think the
miscommunication is due to the fact that Ulrich was thinking about
(un)curryfication, that are operations that apply to functional objects,
not functional syntax. And indeed, though the general topic of your
enquiry is about term constructors, the equivalence between functions
and attributes it something the meaning of which appears much downstream
in the semantic transformation from input syntax into computational effects:
it applies to functional objects, not to functional terms.
[Reminder: if unary functions can be isomorphed into attributes,
then multi-argument functions can be seen as attributes by morphing them
into unary functions in the usual ways: curryfication and uncurryfication
(i.e. higher-order function of decreasing order as you apply more arguments,
or function of a tuple).]

So if I understand your question correctly, it is about whether
it is possible to unify syntaxes for functions and attributes,
rather than just unify their semantics up to some rather elaborate
semantic transformations. -- i.e. can said semantic transformations
be made trivial, and if we can, what does that mean?
[If you are to distinguish the meaning of functional terms
at various moments of the semantic transformation process,
we should be useing different well-identified names for the various stages.]

Yet, I think that though Ulrich mightn't have understood the question,
his reply was still somehow correct: multiple-argument attributes
can be unified with multiple-argument functions, by considering
the straightforward mapping of multiple-argument into single-argument
through static tupling (with the syntax-specified number of arguments).

As for a conceptual model for attributes, etc. - in Tunes,
I think that what I had in my mind when I wrote this page
was that the "state" of the system at any moment could be seen as a set
of (attribute, object(s), value(s)) tuples that are known to hold.
This view of the world is that of various knowledge-based systems,
and it might also satisfy our relational database loving Mad70.
As opposed to an simple relational databases, however,
our semantics integrates dynamism deep inside the knowledge base,
whereas relational databases are static stuff that are modified
by external dynamic agents. (This statement begs for formalization.)

> 2) Abstracting terms
>
> I suppose that this is the constructor for
> the annotations on syntactic types mentioned above. Does this make sense?
Abstrating terms was about lambda-abstraction, defun, and similar things.
They are term constructors indeed (special forms, would say a lisper).
Otherwise, I don't see what you mean.

> how information gets added to specify what
> constraints are needed to trigger the abstraction/annotation.
Well, the usual ways of doing things are that either the formal parameters
are specified as part of the lambda/whatever syntax, as in the pattern
`(lambda ,formals ,@body) -- or the parameters are specified as a special
syntax, as in $1 $2 $@ in shells, de Bruijn indices, etc. -- or any
unqualified variable of a certain syntax is considered as being a formal
variable for the nearest abstraction point, as in Prolog.
In the resulting expression graph, references to formal parameters in
the body are somehow linked back to the formal parameters at the
abstraction point, independently from the abstraction syntax.

I know you know all that (though not all our readers might).
I felt I had to restate it, because the only sense I can make
of your question is that of choosing among the above
a standard input syntax for the HLL- abstractions.
They might as well be lambda like, for what I care.

> 3) "Defining typed constructors"

> wherever this term came from.
Well, typed lambda-calculi, as in ML, Coq, etc.
Though you have something like that in Boyer&Moore's ACL2, too.
And you have records, cases, structs, unions, and objects in most languages,
that amount to something similar.

As for "trust", I guess the term ought to have been elaborated.
-- When I wrote that, I was thinking in terms of the Curry-Howard Isomorphism,
where types are propositions and objects are proofs, so that declaring
"x is an object of type T" amounts to assuming an axiom.

In strongly typed programming languages, constructors obtained from
type definitions are usually typesafe by construction.
But as the type system gets more elaborate, and as types are understood
by the system as having elaborate meaning, users may both want to both
(a) be able to declare objects/axioms that are not safe relatively to what
the system can automatically check, and (b) be safe from objects/axioms
that are declared by other users in other parts of the system.

So this is an issue of scoping/capabilities.
I admit my way of putting things wasn't very orthogonal.
I admit as far as syntactic primitives go, this means that
(a) we have several ways of defining new objects
 (including new constructors). These ways may include more or less checks.
(b) access to these ways is subjected to capabilities at the meta-level
(c) we need a way to express containment zones inside which
 the user has greater relative power to define new axioms.

> I'm reminded of the Epsilon Calculus reference you make
Indeed, an epsilon is a way to assert to you assume
(in the continuation of the epsilon, that is)
that you will have been able to fulfill the (type or other) constraints
asserted in the epsilon construct.
(now, if the epsilon is a future, it may fulfill
the partial constraints that are checked without ever managing
to synchronize into a globally coherent value).

> There's also the question of different kinds of types.
And different kinds of typesystems, indeed.
Selecting a particular typesystem for an object is easy enough.
The hard challenge has always been in making typesystems interact,
without either falling back to a trivial typesystem,
or ending up making horribly expensive computations
just for the useless sake of computing types that are not really used.
I admit I have no great answer to make here, except that we will
indeed have to fallback to dynamic typechecking in the general case,
and experiment a lot, if/when we want to do better.
As for a syntactic primitives, I guess there must be
(a) a way of selecting a typesystem for a program fragment
(b) a way of specifying type constraints relative to the ambient typesystem
 within a program fragment (type checks, type assumptions)

> a single object has infinitely many types.
Yes, though it may have principal types in various typesystems
(and at the meta-level these typesystems will provide a primitive
to extract, check, etc. said principal types).

> we need some primitive that
> expresses universal quantification *independently* from the abstraction
> primitive.
Note that universal quantification can either be a syntactic abstraction
as in (forall (x) (foo x)), or it can be a higher-order syntactic combinator
to be used with other means of abstractions, as in (holds-universally #'foo).

> Note that the dispatch argument effectively separates universal
> quantification from the abstraction primitive, at least to some extent.
I'm not sure what you mean.

> Anyway, this is universal quantification of "output" vs. "input", so the
> argument is even farther removed. What primitive do you think arises here?
It's late and I can't think straight about that,
and figure out what you mean and what I might have meant.

> 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.
Future and actual, or call-by-{need,name,future}
vs call-by-{value,object,reference} are semantically very different things,
both desirable at the same time, that thus require a syntactic constructor
to distinguish between them. As for how to what to choose at first, if we
are to bootstrap from CL, we might as well copy the way Screamer did it.

For side-effecting vs. non-side-effecting, I was thinking not only
of constructors for types that specify the difference, but also
of functors that transform side-effecting objects into pure objects,
and vice versa -- a bit like monads in Haskell, except that monads are
never absorbed in Haskell, so that if ever you want to use locally,
you either clutter up the whole program globally, or you do unsafe things.
I admit I can't provide full formal semantics for such
absorption and reification of monads.

> 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.
Yup - that's the kind of things that the primitive I'm looking for
would resolve into, when implemented.

And you're right that if we have a general syntax for this kind of things,
considering techniques for modular construction of language semantics
through the incremental application of monads, this could be the focal
point of "reflection" in the HLL.

> So [...] we have two of four "basic constructors" which don't have
> an obvious specification yet.
Indeed.

I hope my answer clarified my original thoughts
as expressed on the project page.
I readily admit these thoughts were more of a seed than an achievement.
I hope this answer made sense despite my mind getting so tired.

Best regards,

[ François-René ÐVB Rideau | Reflection&Cybernethics | http://fare.tunes.org ]
[  TUNES project for a Free Reflective Computing System  | http://tunes.org  ]
Always design a thing by considering it in its next larger context -- a chair
in a room, a room in a house, a house in an environment, an environment in a
city plan. -- Eliel Saarinen