Re: The Paradox of Partial Parametricity

[+es-discuss]

I didn't realize that I composed this in reply to a message only on
public-script-coord. Further discussion should occur only on es-discuss.
Sorry for the confusion.


On Fri, May 10, 2013 at 5:52 AM, Mark S. Miller <erights@google.com> wrote:

> 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
>



-- 
    Cheers,
    --MarkM