Failure-handling as fundamental

[Brent L Kerby]

Hello, TUNES folks ... 

Last night I thought of some exciting ideas (at least they seemed exciting) for
a TUNES-like language. These ideas really are not new, but this way of thinking
of them has striking consequences that I'd never seen before.

(I apologize if the following is long or confusing. If clarification is needed,
please ask)

The central idea I realized was that failures (or exceptions), and constructs
for handling failures, naturally form a part in the very foundation of
mathematics and computation. I'll try to explain how this is so ...

In most systems, truth and falsehood are treated as two special values that can
be inputed and outputed from functions. However, try applying this metaphor:

  A "true" program is one which terminates without failure.
  A "false" program is one which fails.

Fare has hinted at this idea before, long ago, in his paper on Reflection, I
believe. This may not seem earth-shattering. However, consider now how the
logical primitives ("or", "not", "if", etc) can now play dual roles as boolean
operators and control structures, since they operate on programs. Thus, (using a
Joy-like concatenative notation)

  [P] [Q] or

would execute P, and iff it fails execute Q. And,

  [P] [Q] if

would execute P, and iff it succeeds execute Q. This is similar to UNIX piping,
really.

Now, for some theoretical joys this system has ... for one, it reconciles the
paradoxes; because, we can see that there is a third class of programs, beside
the ones that succeed or fail: namely, programs which never terminate. We'll
find that when paradoxical statements are translated into this formalism, they
simply become non-terminating programs; thus they are neither true nor false,
and we can see why and be satisfied.

Second, recall long ago the mention was made of a mythical "undo" primitive,
which given a program, would perform the opposite action as the program, acting
to satisfy the rule:

  A [A] undo   ==  

In other words, "undo" should literally undo the effect of a program as if it
had just been executed. Now, granted "undo" may be a nice pseudo-primitive in
word-processing applications (or many other applications), one may argue that it
has no place in the core of a system. But, then consider, "undo" is literally
the Church number for "-1", and Church numbers are a fantastically beautiful way
of defining numbers in terms of combinators. Church numbers are normally
resticted to positive integers, but with a "-1" primitive, we have the
possibility of  Church real numbers and even Church complex numbers. I can't see
what the effects of this would be, exactly, but I suspect that they may make
many or all of the axioms of numbers derivable from the more basic axioms of
combinators, in perhaps a beautiful and dramatic way. (Note I'm seeing extended
Church numbers as being a valuable tool in proof-systems and other theoretical
type things, but they are probably not really useful in ordinary computer
programming)

So what does this have to do with failures? Well, the fact is that sometimes
"undo" cannot satisfy its magical rule. Consider

   2 [0 *] undo

This is trying to divide by zero, essentially. Naturally, we would just say that
this program fails. Now, here is something interesting ... the very operator of
equality can be constructed neatly from "undo" as

   [dup] undo

If the two objects are unequal, then "dup" could not have just been executed,
and failure (falsehood) will occur; otherwise, a single copy of the identical
objects will be left, and the program will be true.

Here's another strange result from "undo". Try

   [drop] undo

You might say this program is indeterminate, in that anything can be pushed onto
the stack as a satisfactory execution of "undo", and it might well be different
things each time it is run. An indeterminate program here just means one that
may give different results (perhaps even sometimes fail and sometimes succeed)
each time it is run, even given an identical system state. This is not
exceptionally unusual in the context of normal programming, of course; it is
quite common for programs to have different possible outcomes, due to user
influence for example.

Now, here's a fascinating question and challenge: Is it possible to create
quantifiers using "undo" in conjunction with a logical operator (say "or",
"not", or "if")? That is, can you construct an "all" such that

  [P] all

will succeed only if "[Q] P" would have always succeeded for any "Q", and fail
otherwise. Or, can you construct a "some" such that

  [P] some

will succeed only if "[Q] P" would have been guaranteed to succeed for at least
one "Q", and fail otherwise? If so, that would be very fascinating. It would
mean that from a combinatory base (say, "s", "k") and "undo" and one logical
primitive (i.e., to catch "undo"'s failures), it is possible to express even
theorems of calculus and such things, using extended Church numbers.

Here's a final note on logical primitives, as far as which of them can be used
as a foundational base. Actually, "not" will do as a base by itself, as

  or ==  A\ B\  [[B] not [A] not] not    ( == [[not] cons] dip [not] cons cat
not)
  if ==  A\ B\  [B [A] not] not          ( == [not] cons cat not)

And, "if" will do as a base, as
  
  not ==  A\    [A] [2 [0] undo] if      ( == [2 [0] undo] if)
  or  ==  A\ B\ [B] [[A] not] if         ( == [not] cons if )

For "2 [0] undo" could be substituted actually any program that is guaranteed to
fail (actually, preferrably a program that would not leave an extra junk "2" on
the stack, if this is possible).

I don't think "or" will work as a base ... 

Well, I hope that whole thing made some sense. If anyone can figure more out
about the theoretical side of this, I would be excited. Or any comments could be
interesting, really.

Meanwhile, I think I'll try to make a little prototype implementation of this
kind of system (a Joy-like one, but with failures and failure-handling, and also
with a style of variables, but of course not with "undo").

- Brent Kerby