Contravariance of Lwt resolvers is unsound

[aantron]

Fortunately, they don't have a variance annotation in lwt.mli. However, they do in lwt.ml, and there appears to have been the intent to make resolvers contravariant in the past (363f67a).

I think they actually were contravariant at that point (I haven't looked at what the whole interface was back then). However, about 1.5 years later, Lwt.waiter_of_wakener was added (d996472), making possible the following interaction if resolvers are declared as type -'a u:

let () =
  let
    (p1 : [ `Foo | `Bar ] Lwt.t),
    (r1 : [ `Foo | `Bar ] Lwt.u) =
      Lwt.wait ()
  in

  (* [ `Foo ] is a subtype of [ `Foo | `Bar ], so [ `Foo | `Bar ] Lwt.u
     is a subtype of [ `Foo ] Lwt.u, if Lwt.u is contravariant. We can
     therefore pass r1 to an instance of Lwt.waiter_of_wakener at type
     [ `Foo ]: *)

  let
    (p2 : [ `Foo ] Lwt.t) =
      Lwt.waiter_of_wakener (r1 :> [ `Foo ] Lwt.u)
  in

  (* We now have a reference p2, to the same promise as p1, which
     supposedly can only be resolved with `Foo. However, we have a
     resolver, for both p1 and p2, that allows resolving with either
     `Foo or `Bar. So let's mess things up: *)

  ignore p1;
  Lwt.on_success p2 (function
    | `Foo -> prerr_endline "got `Foo");
  Lwt.wakeup_later r1 `Bar

This prints got `Foo. Presumably, the compiler optimizes away the pattern-matching.

Going by only the commit messages, it looks like not marking resolvers contravariant in the interface was an oversight, but it turned into a happy accident when Lwt.waiter_of_wakener was added – but of course, I don't know if this was intentional from the beginning, etc. @vouillon, @diml, any relevant background on any of this?

[aantron]

I think we should mark this function deprecated, and either remove it in 4.0.0, or tell users that if they use waiter_of_wakener, they need to be almost as careful as if using Obj.magic. Indeed, internally, waiter_of_wakener is exactly Obj.magic. We should then mark resolvers contravariant (i.e, declare them as type -'a Lwt.u).

I don't actually have any example where contravariance of resolvers is necessary. However, not having them contravariant suggests some kind of big misconception in Lwt, and doesn't match the expectations of people with some type theory background.

Another thing that suggests deleting or discouraging use of waiter_of_wakener is that it doesn't make immediate sense in a JS implementation. There, the resolver is just a pair of the fulfill and reject functions. It makes no sense to extend it with a reference to the promise, only to support waiter_of_wakener, a single flawed API that messes up the typing of Lwt.

@Drup, @hcarty, @raphael-proust, anyone else, any thoughts on this?

[Drup]

Note that once the removal of float array optim has landed properly, the typechecker will be able to generalize contravariant variables just like covariant ones. Not sure if it's actually useful for Lwt.u, but that's worth noting. :)

[aantron]

Ok, I marked the function deprecated. I decided to save marking resolvers contravariant for 4.0.0. It's some kind of "co-breaking" change. While it shouldn't break any existing code that already compiles, it might break the assumptions of some programmers in a nasty way when writing new code or refactoring.

[ivg]

It is not that -'a u is unsound, it the waiter_of_wakener which is unsound. Basically, a variance of a datatype is not affected by the way how it is used, only how it is constructed. Thus adding a new function may not change/invalidate the variance. But of course, waiter_of_wakener breaks the type system, as you've shown (you can even get a segfault, by passing int and waiting float).

[aantron]

@ivg, perhaps I come from a slightly different background, where variance is determined by elimination forms, of which waiter_of_wakener is one.

With that perspective, the full statement is "-'a u is unsound in the presence of waiter_of_wakener," i.e. "removing waiter_of_wakener is enough to make -'a u sound," which is of course what was done (by deprecating it).

[aantron]

And just to clarify, when either one of us says "-'a u is unsound," we are not talking about the 'a u, but about the - :)

[ivg]

What is unsound in waiter_of_wakener is that it coerces 'a t to 'a u. Once they were separated for the purpose of ascribing them different variances, they shouldn't be unified back again, as it defeats the whole purpose of splitting a bivariant type into two parts, one contravariant and another covariant.

So waiter_of_wakener is unsound if we will treat 'a t and 'a u as types with different variances. Since this was never in the public interface, the introduction of this function was fine.

Besides, waiter_of_wakener breaks the covariance of 'a t also. This is rather symmetric.

Perhaps, instead of deprecating waiter_of_wakener it is better not to expose variance of -'a u at all (and even remove an annotation in the implementation). The question is what is more useful.

[ivg]

To clarify, the type is defined by its definitions, thus the set of eliminators is fixed:

  type ('a, 'u, 'c) promise = {
    mutable state : ('a, 'u, 'c) state;
  }

  and (_, _, _) state =
    | Fulfilled : 'a                  -> ('a, underlying, resolved) state
    | Rejected  : exn                 -> ( _, underlying, resolved) state
    | Pending   : 'a callbacks        -> ('a, underlying, pending)  state
    | Proxy     : ('a, _, 'c) promise -> ('a, proxy,      'c)       state

The idea was, that only the 'a u (the wakener) should be used to modify the state field. Since a mutable cell has two eliminators: getter of type 'a cell -> 'a which is covariant, and setter 'a cell -> 'a -> _ which is covariant, together they form a bivariant type. However, we can split them into two types, one is for getting and another is for setting, and safely ascribe them corresponding variances. This works only because now these two types are different. But then waiter_of_wakener comes... which, by virtue of a pure magic, converts one type to another.

[aantron]

To clarify, the type is defined by its definitions, thus the set of eliminators is fixed:

Normally, yes, but:

1. The .ml file is (and always was) rife with Obj.magic for multiple reasons, and the type actually declared in the .ml is actually invariant.
2. The type is abstract in the .mli file, so the set of eliminators from a user's point of view is the set of functions that can take a resolver. Since the .ml file is using Obj.magic anyway, and the type, as declared, is invariant, it is the .mli that must be used for reasoning about variance.

Or, in other terms, the abuse going on in lwt.ml means that OCaml's type system does not check that the variance declared in the .mli is what is actually implemented in lwt.ml, so we must reason about the .mli ourselves.

[aantron]

...a.k.a. the typing connection between the constructors and basic operations in lwt.ml, and the surface functions exposed in lwt.mli, is broken. lwt.mli is the "lowest" surface to the declaration that we can actually use for reasoning.

[ivg]

Yep. magic breaks everything, I agree. What I'm trying to say, is that it is not a variance of the type variable in 'a u that is broken, but the function waiter_of_wakener. If we will remove the latter, we can actually keep the variance annotations, and benefit from it in the future, once the value restriction is relaxed to the point where contravariant types could be also generalized. At that time it would be possible to publish it as -'a u in the mli file, and let p,w = Lwt.wait () will be generalized to 'a t * 'a u.