New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Contravariance of Lwt resolvers is unsound #458

Closed
aantron opened this Issue Jul 23, 2017 · 11 comments

Comments

Projects
None yet
3 participants
@aantron
Copy link
Collaborator

aantron commented Jul 23, 2017

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 aantron added the question label Jul 23, 2017

@aantron aantron closed this in 49c96ff Oct 13, 2017

@aantron

This comment has been minimized.

Copy link
Collaborator

aantron commented Nov 7, 2017

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?

@aantron aantron reopened this Nov 7, 2017

@aantron aantron added this to the 3.2.0 milestone Nov 7, 2017

@Drup

This comment has been minimized.

Copy link
Member

Drup commented Nov 7, 2017

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 added a commit that referenced this issue Nov 10, 2017

@aantron aantron added breaking and removed question labels Nov 10, 2017

@aantron aantron modified the milestones: 3.2.0, 4.0.0 Nov 10, 2017

@aantron

This comment has been minimized.

Copy link
Collaborator

aantron commented Nov 10, 2017

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.

@aantron aantron added the in progress label Dec 18, 2017

aantron added a commit that referenced this issue Dec 23, 2017

@aantron aantron closed this in #518 Mar 24, 2018

aantron added a commit that referenced this issue Mar 24, 2018

@ivg

This comment has been minimized.

Copy link

ivg commented Jun 29, 2018

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

This comment has been minimized.

Copy link
Collaborator

aantron commented Jun 29, 2018

@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

This comment has been minimized.

Copy link
Collaborator

aantron commented Jun 29, 2018

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

This comment has been minimized.

Copy link

ivg commented Jun 29, 2018

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

This comment has been minimized.

Copy link

ivg commented Jun 29, 2018

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

This comment has been minimized.

Copy link
Collaborator

aantron commented Jun 29, 2018

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

This comment has been minimized.

Copy link
Collaborator

aantron commented Jun 29, 2018

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

This comment has been minimized.

Copy link

ivg commented Jul 2, 2018

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment