Lambda the Ultimate

The way I've liked to think about this ever since Filinksi's DCaCD (which I have since discovered was already, like many things, well anticipated by Landin) is the following:

    With state, the "last" assignment is effective.
    With exceptions, the "first" throw is effective.

(which immediately should suggest more commutative generalizations; eg, the dual of monotonic lattice variables for state —substituting max for last— are synchronous reactive systems where the exception which throws the highest — substituting max for first— determines the overall effect)

Since "throw" is the dual to "get" and "catch" the dual to "set", isn't this expressed rather as (quoting the Dumas paper):

For instance, it can be proved that for looking up the value of a location i only the previous updating of this location i is necessary, and dually, when throwing an exception constructed with ti only the next recovery operation ci [catch], is necessary.

Or in other words, an assignment eliminates the effect of previous assignments, whereas handling an exception eliminates the effect of subsequent handlers.

an assignment eliminates the effect of previous assignments, whereas handling an exception eliminates the effect of subsequent handlers.

But an assignment doesn't eliminate the effect of previous assignments, in general, unless it's an assignment of the entire state of the universe, which seems a pretty absurd and meaningless sort of "assignment". An assignment changes one element of state, and meanwhile the previous assignment may have had effects on other elements of state, so that after the current assignment, the overall state of the universe is different that it would have been if the previous assignment had never happened. Whereas an exception can eliminate possible branches of the future completely, so that they will not happen and the universe will be entirely unaffected by them.

I believe they're talking about the effect on a particular location and on a particular thrown exception. And there are further parallels, e.g that propagating an exception is dual to setting a location to the same value it currently has.

It seems there's also a connection to division and subtraction of types. In Scala notation:

trait Lens[A, B] {
   def get(x: A): B
   def set(x: A, y: B): A
}

trait Prism[E, A] {
   def raise(x: A): E
   def handle(e: E): Either[A, E]
}

A Lens says that A is isomorphic to (B, R) where R is some unknown type. So R = A / B.

A Prism says that E is isomorphic to Either[A, R] where R is some unknown type. So R = E - A.

Duality means that two things are the the same - but with all their implications reversed. AND and OR are dual in this sense:

(A and B) implies A, (A and B) implies B
A implies (A or B), B implies (A or B)

The above cited paper shows that state handling (not control flow) and exception handling exhibit this same duality.