Lambda the Ultimate

How about you read the paper and then explain to me where the similarities and differences between abstract interpretation and your "condition propagation" lie? The paper I provided the link for just provides a few simple examples, but the document should give you a more precise understanding of what abstract interpretation IS.

I installed a new PDF reader and was able to see the paper (was garbled with my old reader). I can see that abstract interpretation gives an apparently unified way of reasoning about programs of a given language. One abstract interpretation application in the vain of CP is the verification of boundaries. The paper even specifically gives the example of verifying array boundaries in a Pascal-like language. If the task were to produce or at least approximate the boundary conditions of a given program, I could see abstract interpretation as being invaluable. If, on the other hand, they were hard-wired into the primitive operators and propagated from there, complex analysis can be avoided. I do see one possible sticky place for the compiler however: determining what condition(s) are satisfied by a particular resolution expression. This may be a place where abstract interpretation could help, because it involves proving that a particular condition is satisfied by a given assertion. Anyway, thanks for the link, maybe I'll understand it better with another read. ;-)

I found the 1977 paper a tough read, too. What helped me was to work through Dan Friedman and Anurag Mendhekar's Using an Abstracted Interpreter to Understand Abstract Interpretation to get a hands-on hacker's intuition before trying Cousot and Cousot again.

The aim is similar (avoid evaluating), but lazy evaluation puts off obtaining values in general in hopes that the value will not actually be required. CP avoids evaluating in order to contain boundary conditions. CP operators expose the conditions under which a value may be obtained and lets the evaluator decide whether to: a) satisfy the conditions and evaluate, b) return some other value or perform some other action, or c) propagate the condition and decide "earlier" in the expression what to do.

Consider this:

insert RowX into TableY
  when not RowUnique then
    update TableX set RowX

And this:

if (insert RowX into TableY) satisfies true then...

The former example inserts a row if it isn't in the table, or updates the row if it is. Note that unlike exception handling, no attempt was made to actually insert the row in order to revert to an update. Instead, the same condition that the system must already perform to avoid a key violation is performed and the developer decides what to do if that condition fails. Note that the condition only needs to be evaluated once.

I suspect that CP and lazy evaluation are orthogonal, and can imagine a language that does both CP and lazy evaluation. ...Interesting.

Note that unlike exception handling, no attempt was made to actually insert the row in order to revert to an update. Instead, the same condition that the system must already perform to avoid a key violation is performed and the developer decides what to do if that condition fails. Note that the condition only needs to be evaluated once.

I don't see the difference. With exceptions, 'insert RowX into TableY' for a duplicate row would fail as soon the key violation test is performed, and control would transfer to the exception handler. The test for row uniqueness is performed the same number of times (once for the insert, once for the update).

Similarly, in examples like the array boundary and parsing examples, I don't see how the described system is observably different from a system with resumable exceptions. E.g. when an array access exception occurs, an exception handler would be called essentially as an ordinary function, and one of the choices available to the handler is to return a value like Point(0, 0) to the point at which the exception occurred.

Sparse rows look like a different sort of feature to me. Without working out the implementation details myself, I can only take it on faith that their implementation mechanism via CP would be similar to that of the other examples. It'd be useful to see even a sketch of a toy implementation. That'd also help answer the various questions about how CP relates to abstract interpretation, lazy evaluation, and dependent types. ;)

I assume your perception is that an exception version of the same logic would look like this:

try
  insert RowX into TableY;
catch
  on KeyViolation do
    update TableX set RowX;
end;

In such case, you are correct that the check is only performed once, but the prescribed methodology for exception handling is to avoid exceptions and keep them "exceptional". Thus, a "proper" implementation based on exceptions might be:

if not exists (TableY where KeyCol = RowX.KeyCol) then
  insert RowX into TableY
else
  update TableY set RowX;

This is, unless there is an operator like:

TryInsert(Table : Table, Row : Row) : Boolean;

As I state in my main posting on the subject, exception languages have evolved towards such operators to allow exceptions to be avoided. To re-state another point, when is something an exception and when is it an expected outcome? The current mantra in the .NET space, for example, is to avoid exceptions altogether. Under this, exceptions become almost synonymous with defects; places where the developer did not adequately avoid them.

Beyond the philosophical reasons, there are also practical reasons to avoid them. There is an often costly performance hit; not just due to particular implementations but by nature. Exceptions aren't as "cheap" as a simple branch, which is another reason the "TryParse" pattern has evolved.

As the latter example in my prior post shows, it is also important to be able to query a condition without attempting execution. Again, with exception handling it is incumbent on the developer to know and anticipate the conditions of any given operation in order to avoid an exception. This becomes increasingly difficult or even impossible for complex operations like database manipulation. It is impossible when the ability to test the condition without attempting the operation is not exposed, which it often isn't.

CP is largely about splitting the condition from the operation. This allows the operation's conditions to be evaluated independent of the operation, and it allows for the conditions to be resolved earlier than necessary. Not unlike null propagation in usage, conditions can be addressed at different places in the expression.

select Rotate(Translate(Point((5 / X) * 100, Y)), 45) resolve DivideByZero as Point(0, 0);

Unlike null, however, the compiler is ensuring that the DIV operator never receives a 0 denominator. This avoids the run-time null propagation logic as well as the boundary checks within the actual operators.
Again, the conditions can also be inquired of independently:

select Rotate(Translate(Point((5 / X) * 100, Y)), 45) satisfies DivideByZero; // true if X isn't 0

One more point regarding exceptions: The exception embracing languages that I know of don't allow exceptions to be resolved within an expressive context. I don't necessarily see a reason why such languages couldn't be extended to support this, though most such languages are not richly expressive and so I assume this simply hasn't been perceived as a major obstacle. Languages that are more expressive, however, would clearly need to have some sort of try...catch expression. I can only imagine the nightmare this would create for an optimizer that can't "see" the conditions leading to these exceptions.

Regarding sparse rows: I agree that this concept is largely distinct from CP. It is clear that CP could exist without sparse rows, but the converse is not true. Frankly, of the two ideas, I am much more comfortable with CP. I think I could build an implementation of CP right now, while I'm not sure I could say the same about sparse rows. I agree that a prototype would be a good way to exhibit the concept. Perhaps I'll get a chance to modify our D4 language to support CP.