Surprised by Joy

[btanksley@hifn.com]

BTW, Tunsers, there was an article on comp.lang.forth which discussed some
of the Tunes documents.  I suspect that some of us would find something in
it to discuss.  The title is "more rationalizing", and the author is
"cLIeNUX user".

We now return you to our regularly scheduled quibble :).

I'm going to split this message into two parts: in the first part goes
anything about the applicative CLIP system, and in the second part goes
stuff about Joy.

>From: iepos@tunes.org [mailto:iepos@tunes.org]

>It would be possible to make types first-class... a type could
>be thought of as a pure procedure which takes a thing off the
>stack, and pushes a proposition (True or False) indicating
>whether the popped thing was a member or not. But, maybe this would
>not be a good idea... I'm not sure...

RTTI, in other words.

>Type systems are usually
>kept separate from the rest of the system.

Ah, but the type information is useful and shouldn't be kept hidden.  In
addition, TUNES has this "thing" about wanting everything to be first class.

>And, mentioning "-" reminded me of something else... One interesting
>primitive one could add to the system is an "undo" primitive...
>Such a primitive would take a quoted program off the stack, and
>would "undo" the quoted program. This probably seems like a
>wild idea; "undo" is usually thought of as a fancy feature often added
>to text editors and things... to treat it as a fundamental primitive
>of a system is getting weird... it would probably make the system
>impossible to fully implement.

Probably.  However, at the same time, it _is_ possible; existance proof is
in the language 'J', which implements an adverb 'power'.  n-th power repeats
the given verb n times, but if n is negative is repeats the inverse of the
verb n times.

>But, there are interesting things about "undo"... It seems to be
>the analogue of the "inverter" primitive that I wanted in my
>applicative system. Using it in conjunction with the Church Numbers
>(those "doonce", "dotwice", "dothrice", and such, that I mentioned
>earlier), it would be possible to form all kinds of interesting
>Church numbers (including negative, fractional, irrational, imaginary,
>etc.). Actually, "undo" might itself be considered the Church Number
>for negative one.

Hmm.  Possibly...  Yes, that makes sense.

>Then, as an example, one could form a "dohalf" primitive, that
>takes a quoted program and executes it a "half" a time:

>  [[dotwice] cons] undo

I don't see that one.  It looks to me like -2, not 1/2, since it undoes a
function twice.  A simpler way to express -2 would be:

  [dotwice] undo.

Our functions aren't identical in their effects, though; perhaps I'm wrong.
Your function actually looks more like it'll undo a cons with dotwice, which
is very different from undoing something twice.

>I think that is right... and, the "dotwice", "dothrice", and such
>I used earlier took a quotation and resulted in a quotation;
>as I use them now, they do not result in a quotation, but rather
>just execute the quotation they are given so many times...

Right.  Fortunately, it's trivial to use quotation to allow them to result
in a quotation.

>would be a function that subtracts 5... I guess then that

>  [add] cons undo

>would be a subtraction program...

It would be a program which undid adding something.  I don't see why you
can't do

  [add] undo.

, though.

>And, of course, some programs do not make sense to be run a negative
>number of times, or a fractional or imaginary number of times
>(although some do), or some might make sense in multiple ways...
>Not sure how a system would deal with this... 

Nor am I.  J deals with it by only implementing power partially: only
specific primitives, and specific ways of combining those primitives, have
inverses.

>Now seems like a good time to share the idea I had about altering
>the quotation construct of Joy to make it better correspond to
>application of "T"... (I don't claim that this enhancement
>would make Joy better; in fact, looking back, I think it would make
>it worse, although it does inspire a few other thoughts)

Thought is good.  :)

>The basic idea is to make "[foo]" denote the program of pushing
>the program "foo" onto the stack; then, for instance, "[add]" and
>"[swap add]" are equivalent programs, since each pushes the "adding"
>program onto the stack. And... if you told the mythical system to
>do "[add] [swap add] =", it would push "True" onto the stack
>(although it might not realize it, if it is acting in a lazy style).

Okay.  As far as this goes, that's great -- but it's not possible in general
to test the equality of programs.  I would recommend that '=' treat programs
as incomparable unless they're actually the same program.  Now, it's
possible for ==> and => to test the equality of programs under a finite set
of transforms, and in such a treatment, given the commutative axiom, your
two programs would result in True.

>To emphasize, in my mythical modified Joy system, "[add]" and 
>"[swap add]"
>mean the same thing to the system and can be replaced by each other.
>A consequence of doing it this way is that programs cannot directly
>be introspected; however, this could be fixed by adding a "reify"
>primitive. 

This would indeed be a consequence (although adding a reification primitive
would not solve it, but rather push off the real solution to another level).

I think a better solution is to provide two new types and two new operators.

The first type is 'symbol'; an object of this type may or may not represent
a function in this or some other context.

The second type is 'function'; an example of the function type is
demonstrated by running

  [+ +] uncons

The result of this is a function followed by a list (which contains a
function).

The first new operator is "=>"; it acts like Joy's notation, but returns
true if and only if one of its first argument can be rewritten as its second
argument using a single rule.

The second new operator is "==>"; like the first, it checks whether its
first argument can be rewritten to look like its second with any number of
steps.

(Note that these two operators may not always be commutative, depending on
what rules the system knows.  Other operators could be provided which were
commutative, such as "<==>".)

These four additions allow reasoning about quotations even though functions
cannot be compared for true equality.  In addition, the new datatypes make
it possible to write functions which expect 'quotations' in a specific
format.

For example, you recall my [0 add] example, where my program expected to be
able to uncons the input, but the optimizer had optimised the "0 add" away.
Under my new system, the input would be better expressed as something like
[0 #add], where #name returns a symbol.

>Now, there is the issue of lists... how will lists be represented,
>now that quoted programs no longer have introspection?

I recommend that quoted programs keep their full introspective capabilities.

>My answer
>is that you do not need lists; just push all the elements directly
>onto the stack (perhaps with an additional integer, indicating
>how many there are). Then, make all the "list" operators
>(such as "reverse", "concat", and "cons") operate on the bare
>stack.

You know what?  I really dislike this idea.  It seems so messy!  If you
_really_ felt it to be important that lists not be the same as quotations (I
don't think that's important, but to each his own I suppose), simply create
a new datatype named 'list'.

>By the way, if for some reason you really needed to manipulate
>all the elements as a single beast, then you could use a quoted program
>that pushes the elements onto the stack.

Yes, but without the ability to do quote introspection there's no way to
build such a list at runtime.

I don't think this is a good idea.  However, it does point out a good idea
-- right now Joy has an "unquote" combinator.  I think we also need an
"unlist" function, which dumps everything in a list (or quotation) on the
stack without executing any of it.

>By the way, this talk of pushing lots of stuff onto the stack reminded
>me of Henry Baker's "The Forth Shall be First", which I was reading
>again a bit ago... he really seems to advocate "linear" 
>implementations,

You know, great minds think alike ;-).  The moment I read about Joy, linear
logic popped to mind.

However, the really interesting thing about Joy-type systems is that I
suspect that it's possible to _mix_ linear logic with real GC.  The trick is
that some functions, such as deepcopy, are "linear", and others, such as
"dup", are not.  We could use a generational garbage collector, where the
first 'generation' is managed by linear logic, and objects are tagged to be
managed otherwise simply by having a non-linear operator used on them.

So in a naive system, the definition "myoperator == dup drop" is nonlinear.
(Of course, in a more sophisticated system this causes no problem; it's
clearly linear.)

>Also, there would need to be some way of threads coordinating with
>each other... in my system, I had thought of using Fields...
>new fields could be constructed with a "new" primitive, and then
>they coulded be fetched or stored using "get" and "set" primitives
>(like the "@" and "!" of FORTH)... multiple threads could use
>the same fields... however, I'm not convinced that this is the
>best way; it actually seems to be not a very good way at all,
>considering the synchronization issues. In a linear system, it may
>also tend to cause wasteful moving around of data structures 
>(from a thread's stack, to a field, and then to another 
>thread's stack).

A facinating question.  I've put no time into considering it before.

Multithreading (without the capability of message-passing) is possible
simply by saving the data stack pointer, return stack pointer, and
instruction pointer (and not sharing stacks).  The easiest way for me to
imagine message-passing is via a send/recieve pair of primitives; I suspect
that both block until the transaction is complete (this also implements
synchonization).  If you need asynchronous messaging, you really need an
extra thrad anyhow, and our library will provide a stock way to set one up
(but it likely won't be a primitive).

>Another option is to have some direct primitives by which one
>can transfer items from one thread's stack to another... one
>would need to have been explicitly set to read and the other 
>explicitly set to write (so that items would never get pushed
>onto a thread's stack by another while it was in the middle of doing
>something else)...

Whoops, I see you were thinking of that.  I prefer this solution; it's more
directly implementable (more primitive).

You mentioned an overhead due to linear logic; however, may I point out that
in this case there _is_ no overhead to linear logic, because each item is
referred to by exactly one pointer, and when we transfer the item to another
thread we're actually transferring only the pointer (and the right to use
it, of course).  If any copying actually happens, it would have happened
anyhow.

>Anyway, this is just another tentative idea...
>By the way, in a nice system, I would probably still like to
>have fields... they just don't seem to be good low-level primitives
>for an implementation... fields could probably be constructed
>using this stack-transfering primitive, by making a thread for
>each field, a thread that has the field's value on its stack,
>and which waits for some signal (to fetch or store), at which
>point it would either read in a replacement value for the
>stack or else write a copy to some other thread...

Hmm.  You make a good argument for making 'fields' be a datatype in their
own right.  In most architectures a primitive implementation of 'field'
would be _far_ more efficient (and simpler to implement) than this.
However, this is an _excellent_ model of how fields operate mathematically:
they essentially _are_ a seperate process.

>> Okay.  I'm dizzy. ;-)

>> A procedure is a function which takes a continuation 
>> parameter, and returns
>> a function (if it can take more parameters) or a command (if 
>> that's all the parameters it can take).

>Exactly. Ahh... we're talking again about my applicative system...
>I'm still interested in it, although I'm now more interested
>in implementing a refinement of the Joy system than in implementing
>that purely applicative system... In a bit I'll mention some
>refinements I have in mind...

Wow.  Cool.  :-)

Yes, refinements are _certainly_ needed.

-Billy