The Paradox of Partial Parametricity

I think the key exchange in these threads was

On Fri, May 3, 2013 at 4:17 PM, Jonas Sicking <jonas@sicking.cc> wrote:
[...]

> I.e. permitting nested promises creates a more complex model and with
> that you always get more confusion and more questions.
>

 On Sat, May 4, 2013 at 1:48 AM, Claus Reinke <claus.reinke@talk21.com>
 wrote:
[...]

> From the perspective of a-promise-is-just-like-other-**wrapper-classes,
> auto-flattening promises creates a more complex model



Together with each of their explanations about what they meant. They are
both right. Lifting and auto-lifting do not mix. Q Promises give us
autolifting with no lifting. Monadic promises would give us lifting but no
autolifting. Having both in one system creates a mess which will lead
programmers into the particular pattern of bugs Jonas warns about in his
message.

For clarity I define the following APIs so I can define the three
architectural choices in terms of the subset of these APIs they contain.
Obviously, I do not intend to start a bikeshed yet on the particular names
chosen for these operations. Let's stay focused on semantics, not
terminology.

An upper case type variable, e.g. T, is fully parametric. It may be a
promise or non-promise.
A lower case type variable, e.g. t, is constrained to be a non-promise. If
you wish to think in conventional type terms, consider Any the top type
immediately split into Promise and non-promise. Thus type parameter t is
implicitly constrained to be a subtype of non-promise.




Ref<T> is the union type of T and Promise<T>.

Q.fulfill(T) -> Promise<T> // the unconditional lift operator

Q(Ref<t>) -> Promise<t> // the autolift operator

p.map: Promise<T> -> (T -> U) -> Promise<U>

p.flatMap: Promise<T> -> (T -> Promise<U>) -> Promise<U>
// If the onSuccess function returns a non-promise, this would throw an
Error,
// so this type description remains accurate for the cases which succeed.

p.then: Promise<T> -> (T -> Ref<u>) -> Promise<u>
// Ignoring the onFailure callback



* A Monadic promise system would have Q.fulfill, p.map, and p.flatMap.

* A Q-like promise system would have Q, and p.then

* The dominant non-Q-like proposal being debated in these threads has
Q.fulfill, Q, and p.then.




This note explains why I believe the last is much worse than either of the
other two choices. As Jonas points out, generic code, to be useful in this
mixed system, has to be careful and reliable about how much it wraps or
unwraps the payloads it handles generically. Had programmers been armed
with .map and .flatMap, they could succeed reliably. Arming them only with
.then will lead to the astray. As an example, let's start with a variant of
Sam's async table abstraction. The parts in angle brackets or appearing as
type declarations only documents what we imagine the programmer may be
thinking, to be erased to get the real code they wrote. In this
abstraction, only promises for keys are provided. The get operation
immediately returns a promise for the value that will have been set. (An
interesting variant is a table that works even when the get arrives first.
But we can ignore this wrinkle here.)


    class AsyncTable<T,U> {
        constructor() {
            this.m = Map<T,U>(); // encapsulation doesn't matter for this
example
        }
        set(keyP :Promise<T>, val :U) {
            keyP.then(key => { this.m.set(key, val) });
        }
        get(keyP :Promise<T>) :Promise<U> {
            return keyP.then(key => this.m.get(key));
        }
    }

When U is a non-promise, the code above works as intended. The .then in the
.get method was written to act as .map. When tested with U's that are not
promises, it works fine. But when U is actually Promise<V>, the .get method
above returns Promise<V> rather than Promise<U>. As far as the author is
concerned, the .then is functioning as a broken .map in this case, with the
signature

p.then: Promise<T> -> (T -> U) -> Promise<V>  // WTF?


This same abstraction in a monadic promise system would be written

    class AsyncTable<T,U> {
        constructor() {
            this.m = Map<T,U>(); // encapsulation doesn't matter for this
example
        }
        set(keyP :Promise<T>, val :U) {
            keyP.map(key => { this.m.set(key, val) });
        }
        get(keyP :Promise<T>) :Promise<U> {
            return keyP.map(key => this.m.get(key));
        }
    }

This works reliably.


This same abstraction in a Q-like promise system would be written

    class AsyncTable<t,u> {
        constructor() {
            this.m = Map<t,u>(); // encapsulation doesn't matter for this
example
        }
        set(keyP :Promise<t>, val :u) {
            keyP.then(key => { this.m.set(key, val) });
        }
        get(keyP :Promise<t>) :Promise<u> {
            return keyP.then(key => this.m.get(key));
        }
    }

This works reliably. After erasure, note that this is exactly the same as
the first example. The difference is that the code now correctly implements
the annotated types representing the programmer's intention.

In a system with autolifting, you can't get full parametricity of promises
simply by adding an unconditional lift. You have to remove, or at least
strongly discourage, autolifting. Or you have to take pains to carefully
work around it.

The main failure mode of standards bodies is to resolve a conflict by
adding the union of the advocated features. Here, this works even worse
than it usually does. The coherence of lifting depends on the absence of
autolifting, *and vice versa*. We need to make a choice.


-- 
    Cheers,
    --MarkM