HLL Primitives

[Ulrich Hobelmann]

Brian T Rice wrote:
> 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.

They might be attributes of a tuple.  In fact I don't see why they need 
to be attributes at all.  Aren't normal functions ok?

Another problem here is actions (I/O, side effects).  How should they be
treated?  At some level or other there have to be side effects, though 
one can go the Haskell way, but thats kind of awkward.
Certainly a drawScreen operation wouldn't be an attribute...
But then maybe we could treat mmapped I/O as attributes :)

> 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

Hmmm... yes.  Can't the compiler just statically check (or compile 
dynamic checks) for those properties that are interesting for a certain 
program part?

> 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.

In a declarative language IMHO evaluation is an implementation issue, so 
it should be lazy in general, but strict where the compiler likes that 
(which might be lots of program parts).  The distinction lazy thunk or 
value is just another type/attribute anyway.

> 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.

See above.  I don't think this can be any primitive.  Maybe one could 
declare a function to have a certain side effect, but this is too much 
like ML, i.e. unpure (unless thats fine with you).  The usual problem is 
      state and when / how many times a function gets evaluated, unless 
we go for strict evaluation.
Maybe monads aren't too bad after all(?) (and are just a form of 
quotation in a sense).

Ulrich