From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q3DAqVUj006015 for ; Fri, 13 Apr 2012 12:52:31 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aq4BAIEEiE/RVdK2mGdsb2JhbABFDgiFULFUCCIBAQEBAQgJDQcUJ4IJAQEBAwESAgYJBBkBGwsEAQQGAwEDAQsGAwILDQICERUCAiIBEQEFARwGExoBB4ddAQMGBQubGwqLUk6CcoUJChknDVeIdgEFC4EkigMFgnCCGIEYBI83hjWBEY1FPYNTOYFSCA X-IronPort-AV: E=Sophos;i="4.75,415,1330902000"; d="scan'208";a="153913266" Received: from mail-iy0-f182.google.com ([209.85.210.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 13 Apr 2012 12:52:25 +0200 Received: by iahk25 with SMTP id k25so6633285iah.27 for ; Fri, 13 Apr 2012 03:52:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=Y9uuPBp16H0ERm0eFNmmM5R7MrvnY14vR0hlvWotqhs=; b=HGlR3vv0VsjOt/9UNHj39xiNcN3f7bE0dX2y+q9HEl7GKZtWkYg1AIRfMwIWIB1NXW 2MP0yoDBDlpfot9DnClqt1KoceNB7N/qcc1VJRqPY+WZXRSP9feVdfrf3JfhUvKIMzCk u+hfzc6fJO80W7ZT/o4ZzSoE97h/LjyURntsdOlavtmrx1h68ix4Vz5f6WNvy6XamVPa 1x68k9LzwsQWToIA/ARW0RsFLGKltxHDruefLMOO+yRfdLknO7tZizRK4AcjmNDhdWVa g90vAtjHX4NZq+J9mqJtu372+fRUcj7k+w7n43Tz5UoBXUv8CicT68NMybzSsNLTkacF pE6w== Received: by 10.50.179.34 with SMTP id dd2mr918054igc.60.1334314344188; Fri, 13 Apr 2012 03:52:24 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.140.100 with HTTP; Fri, 13 Apr 2012 03:51:44 -0700 (PDT) In-Reply-To: <1C4497DB-1650-4172-9F01-3434125C79DA@math.nagoya-u.ac.jp> References: <6A006A62-F9C0-4A90-90E5-B2EFD0177E88@math.nagoya-u.ac.jp> <1C4497DB-1650-4172-9F01-3434125C79DA@math.nagoya-u.ac.jp> From: Gabriel Scherer Date: Fri, 13 Apr 2012 12:51:44 +0200 Message-ID: To: Jacques Garrigue Cc: caml users Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q3DAqVUj006015 Subject: [Caml-list] Re: Variance of GADT parameters Dear list, I'm afraid my last e-mail was rejected because it was too long. This is probably a good indication that it would be too long for you as well, but for the record I have uploaded the email content and the attached technical development: http://gallium.inria.fr/~scherer/variance_gadts/second_email.text http://gallium.inria.fr/~scherer/variance_gadts/interference_proof.text > A stronger approach would be to check interfaces to ensure that abstraction > cannot be broken. > I was already thinking about that for making abstract types covariant when > the module interface only allows covariant uses. > But this can be very tricky. If I understand correctly, you are suggesting allowing to annotate abstract types at a module boundary with a variance that contradicts the internal type implementation, as long as the operations proposed in the interface respect this stronger variance. For example, we could have covariant immutable arrays by just restricting the existing invariant implementation and interface. This is something interesting, but indeed it seems difficult and is, I think, relatively orthogonal to the present discussion. It would be a new way to enrich variance information (and possibly upward/downward closure) at abstraction boundaries but, if I understand correctly, it does not subsume the expressivity of variance (or possibly upward/downward closure) information: type +α t val weird_id : α t → α → α >> From a design point of view, the "right thing" would be to let people >> publish this information in the signature for an opaque type. Just as >> we can annotate the type with variance information, we should be able >> to publish its upward/downward closure properties. > > This is rather heavy-weight... Variance annotations on abstract types are already in the domain of experts library writers, not simple users – most people have never heard of them. I don't think the upward/downward closure criterion is much harder to understand or would have much cognitive burden. (There would be the same problem with current variant annotations, that you may have to rely on third-party code defining abstract types that haven't been richly annotated enough by ignorance. I don't think this would make the problem worse.) >> Another natural question is: what if we added the symmetric of the >> "private" concept, a type (blind σ) strictly above σ for all types? >> Would we lose all reasonable variance properties on OCaml types? > > Is there any use for these "blind" types ? I don't know what those "blind" types could be useful for, and I'm certainly not asking for them. Intuitively I'd say that there are situations where one works in a negated world, where what was naturally covariance becomes contravariant, and what should usually be made private would now require such "blind" types. But as said with my previous mail, favoring covariance does not seem to be problematic in practice. This is more of a design argument: we have added a construct but not the symmetric one; what if we had done this, just for the sake of regularity? If something changes from usable to unusable because of this fairly gratuitous move, maybe there is a problem of design fragility. > What do you mean by "all reasonable variance properties" ? > This should only have an impact on GADTs, isn'it ? I mean that upward-closure is currently a fairly natural notion for ordinary types (yes, if a tuple (x,y) can be given a type, then it must be a cartesian product type), which would be broken by adding those types. I informally and nearly unconsciously assumed it held when reasoning about my (Prod : α expr * β expr → (α * β) expr) constructor. Yes, among the type-system features I know of, this would only impact GADTs. More precisely, that would only impact GADTs whose constraint are equality constraints. Still that is something to take into account. I suppose you were not aware, at the time of introducing private types, that this added feature could negatively impact other areas of the type system; we now have the opportunity to ponder this tension more carefully. (I don't know which of GADTs or private types people would find more useful; that surely depends on one's domain and programming style. What would we do if we were given the opportunity to go back in time and remove private types to strengthen equality GADTs?) I believe saying "this new type will never be made private in the future" is the good way to control this tension. I didn't like the idea at first, but that's a way to have our two cakes (private types and equality GADTs) and eat them both, without either one putrefying the other. Indeed this must be transmitted through abstraction boundaries, but I don't think this "go against abstraction", or at least encapsulation. Marking a new type as "non-privatizable" is not revealing some of its internal aspects, but making a design choice for its future use, just as OOP programmers often decide to mark their classes "final" to get stronger reasoning principles on them. Again, I don't say we should add this to the OCaml interface language in a few days/months. I'm only trying to establish that making the design choice of using the upward/downward closure criterion would not close us doors in the future, that it is possible to control it finely without giving away the designer's freedom to evolve the subtyping lattice. On a pragmatic level, I would be fine with keeping the current situations where no type is "non-privatizable" but (indeed) all types are "non-blindable" and not adding the ability to change this locally. This means we can't have equality-constrained contravariant GADT parameters, but the situation on covariant types, which is my main point of interest, is quite reasonable. > Contravariant parameters are not generalized because this would > be unsound: Oh, I was not aware of this. Thanks for the correction. If I understand correctly, the reason is that values do not have an uniform runtime representation. > This does not seem particularly difficult: we already extend the type environment > for GADTs, so it would only mean using private or "blind" types in place of > aliases. That is good news. I had not realized that, just as a local abstract types serves as existential variables, a local private type is in some way a "canonical" smaller type. >> For example, the idiomatic use of the (+α expr) datatype is the >> (eval : ∀α. α expr → α) function, and it can be written on this >> monotonous version. > > There are certainly examples in both directions. > For instance the "print" example in the manual uses the opposite direction. There is a strong difference between the types "expr" and "ty" type α expr | Val : α → α expr | Prod : α expr * β expr -> (α * β) expr type α ty | Ty : α expr | Prod : α ty * β ty → (α * β) ty `expr` carries data so is intuitively covariant. `ty` carries no data so could be used in either directions. Note that the printing function for `expr` does not require contravariance, as its type is `α expr → string`. So I believe that the `print : α ty → α → string` is an example of GADT that should be invariant – rather than an example of GADT that we want to make covariant but couldn't this an open-world presentation, whatever that may mean. > On the other hand, if you really want variance, this looks like a cleaner solution. That's the idea. Having the option to use subtyping constraints rather than equality constraints would allow a library designer to make compromises. Invariance is easier to handle for everyone, but in case covariance is really important it can be done – which is not currently the case. Note that the two ideas, one of using upward/downward closure to strengthen variance properties in the equality case, the other of using subtyping constraints to gain covariance at the cost of weaker elimination, are not mutually exclusive. You can even factor upward/downward considerations through the subtyping constraint approach: instead of checking that equality is sound at constructor definition site, you can check at each elimination site that you can regain a full equality constraint from the subtyping hypothesis through an upward/downward closure argument. I think a reasonable design process for a library writer would be to first go for the easy equality case and, if one discovers a need for {co,contra}variance, wonder about upward/downward closure properties and, if they don't hold, weaken the type to subtyping constraints in the good direction. Each step is potentially more expressive, but also more costly (in term of required annotations, etc.). > Well, your simplest criterion (just check that the instantiated parameter > is upward-closed, failing on "unknown" abstract types) seems easy enough to check. > The question is whether is it really sufficient in practice. > For all the other annotations, there would need to be a very strong justification. I agree with your evaluation of the situation. Thanks for answering so carefully. On Fri, Apr 13, 2012 at 5:45 AM, Jacques Garrigue wrote: > Dear Gabriel, > > Thank you for this detailed analysis. > It is comforting to know that the current criterion is sound! > > I have a few remarks/questions. > >> # A criterion in the general case >> >> I believe (and have a draft of proof in the attached technical annex) >> that the requirement of Simonet&Pottier is equivalent, in the equality >> case, to the following criterion that *could* be implemented in >> a type-checker – more easily than by adding a general constraint >> solver. >> >>  Given variance annotations (≤i) for the type ᾱ t, the type >>  constructor >>    K : ∀ᾱ∀β̄[α₁ = T₁(β̄), α₂ = T₂(β̄)...] τ̄ → ᾱ t >>  or equivalently (in OCaml syntax) >>    K : τ̄ → (T₁(β̄),T₂(β̄)...) t >>  respects the variance if all the conditions below are met: >> >>  1. Non-interference: if an existential variable β appears in several >>     Ti(β̄), then all its occurences in the whole type expression >>     (T₁(β̄),T₂(β̄)...) t must be in invariant position. >> >>  2. Upward/downward closure, or eliminability: for each i, β̄, α', if >>     (Ti(β̄) ≤i α') holds then α' is of the form Ti(β̄'). >> >>  3. Constructor parameters variance: the variance of the β̄ in the >>     type expression (T₁(β̄),T₂(β̄)...) t must respect their variance in >>     the constructor parameters τ̄ – just like if we had a non-GADT >>     declaration in term of the β̄, (type β̄ t = K of τ̄ | ...). >> >> I believe this is sound, not unreasonably difficult to check, and >> would help in a lot of concrete cases that are currently rejected. > > Have you considered my comment on the interaction with abstraction: > >>> Again I wonder whether you are not going to get problems with abstraction. >>> At first sight, no: if when you define a GADT t, the type u is abstract, then >>> it will have no supertype in any environment where we use t. >>> But if you think more carefully, you realize that if in the future we allow >>> (gadt-)unification between abstract types, everything breaks, since abstract >>> types may end up having supertypes in a local environment. >>> So it looks like the only types you can allow for instantiation are concrete >>> datatypes and well-known types (abstract types defined in the initial environment >>> or in the current module). > > In the future, we really want to be able to instantiate normal abstract types with > GADT pattern matching, not just local ones. > Wouldn't it mean that you can never now whether an abstract type is upward closed? > > module M : sig type t type u = private int val eq : (t,u) eq end = >  struct type u = int  type t = u  let eq : (t,u) eq = Eq end > > Note that this doesn't means that I could build a proof of unsoundness. > You criterion may actually be too restrictive. > Actually, my counter-example with a private type used a contravariant gadt. > >> # Discussion of private types and contravariance >> >> There is something quite disturbing in the idea that the mere >> existence of private types creates a strong asymmetry between >> covariant and contravariant parameters for GADTs: while upward-closed >> types are relatively common (so that we can expect "the usual >> examples" of GADTs to have "the expected variance"), there are no more >> downward-closed types, which means no contravariant constrained >> parameter. >> >> Upward or downward closure can be easily decided on fully transparent >> types (types whose definition is known). But there is a problem with >> opaque types: as we don't know how they were defined, we can't check >> if they are upward/downward closed. > > Sorry about the above comment. > This seems to be what you are referring to here. > I would just remind you that we have lots of opaque types around, > so that this may be a strong limitation in practice. > Of course we can still apply the criterion that opaque types in > the initial environment (builtin + pervasives) cannot be circumvented, > but this a kind of hack. > > A stronger approach would be to check interfaces to ensure that abstraction > cannot be broken. > I was already thinking about that for making abstract types covariant when > the module interface only allows covariant uses. > But this can be very tricky. > >> From a design point of view, the "right thing" would be to let people >> publish this information in the signature for an opaque type. Just as >> we can annotate the type with variance information, we should be able >> to publish its upward/downward closure properties. > > This is rather heavy-weight... > >> Another natural question is: what if we added the symmetric of the >> "private" concept, a type (blind σ) strictly above σ for all types? >> Would we lose all reasonable variance properties on OCaml types? > > Is there any use for these "blind" types ? > What do you mean by "all reasonable variance properties" ? > This should only have an impact on GADTs, isn'it ? > >> One idea from Didier Rémy is to allow, when defining a new type 't' >> (not a type synonym), to define it as "non-privatizable" >> (and correspondingly non-blindable). We or another programmer would >> then not be allowed to define a type 'private t'. In exchange for this >> lost flexibility, 't' would be downward-closed. The idea is that >> introducing private types increased our freedom, and reciprocally >> lessened our ability to reason about "what cannot be done"; >> non-privatizable annotations allow to locally make the inverse choice >> of losing 'private' for better subtyping properties. > > This one would really go against abstraction... > >> From a pragmatic standpoint, I suspect the current restrictions >> 'private' entails on the GADT variance checks are not going to be >> really problematic in practice. We tend to use covariant types >> (data) more often than contravariant types (computations). The OCaml >> type system is already skewed towards covariance in one place: while >> the relaxed value restriction (which, I recall, is the reason why >> I needed GADT variance in the first place) would work equally well >> to generalize variables that appear only in covariant or only in >> contravariant positions, the relaxation is implemented in the >> type-checker only for covariant parameters. And I have not yet heard >> of someone requesting generalization of only-contravariant >> parameters, so apparently treating contravariant parameters as >> second-class citizens is ok among OCaml users. > > Contravariant parameters are not generalized because this would > be unsound: > > let f : 'a -> unit = let r = ref [| |] in >  fun x -> if !r = [| |] then r := [|x|] else (!r).(0) <- x > > let crash = f 1.0; f 1 > > It is unsound to add a top type to the ocaml type hierarchy. > But the "blind" types would of course be sound. > >> # A theoretical open-world approach >> >> Some people may consider the upward-downward criterion as >> fundamentally unsatisfying because of the closed-world assumption it >> makes: it is not preserved by enrichment of the OCaml subtyping >> lattice. >> >> There is another possibility to get some variance properties out of >> GADTs that still works in an open-world system: allow GADTs >> constraints to have subtyping constraints, instead of only equality >> constraint. >> >> For example we could define the type of well-typed expressions in >> this way (note the ≥ in constraints): >>  type +α expr = >>    | Val : ∀α. α → α expr >>    | Prod : ∀α∀βγ[α ≥ β*γ] β*γ → α expr >>    | Priv : ∀α[α ≥ priv_int] priv_int → α expr >> >> It is trivial that this definition is covariant in its type parameter, >> because covariance was baked in the definition. Indeed, if α≤α' >> and α≥β*γ, then α'≥β*γ by transitivity: the constraint is preserved by >> going to a larger type. In the soundness requirement of >> Simonet&Pottier, one can use the exact same existential variables on >> both sides (β̄':=β̄), and the constraints will be satisfied. >> >> The downside of this easier covariance property is that we get weaker >> types on deconstruction (pattern matching of GADT values): when >> matching on a (α t), in the Prod clause, we only know that (α ≥ β*γ) >> rather than (α = β*γ) – note that we could regain the stronger >> hypothesis by locally using the closed-world assumption. >> >> This simple idea has two potential problems: >> >> 1. This may not be implementable as part of the current OCaml >>   type-checker, which uses type equalities internally and has more >>   limited subtyping support (in particular we can't abstract over >>   arbitrary subtyping assumptions). That said, this particular way of >>   adding subtyping hypothesis in the context might be simple enough >>   for it to handle. >> >> 2. Getting a weaker hypothesis may be unusable: maybe the usual GADT >>   programs really make use of the equality assumptions, and going for >>   subtyping assumptions would make untypable programs that would be >>   perfectly fine under the closed-world assumption. >> >> >> Jacques can tell us about point 1. > > This does not seem particularly difficult: we already extend the type environment > for GADTs, so it would only mean using private or "blind" types in place of > aliases. > >> Regarding point 2., I'm not sure >> and have not thoroughly checked examples, but my intuition is that it >> is actually not a problem. I think that the types we naturally want to be >> covariant are also the types we want to manipulate as data (so it's ok >> if the type is larger than what we expect), rather than consumers, and >> conversely. >> >> For example, the idiomatic use of the (+α expr) datatype is the >> (eval : ∀α. α expr → α) function, and it can be written on this >> monotonous version. >> >> let rec eval : ∀α. α expr → α = function >>  | Val (v : α)                        → (v : α) >>  | Prod ∃βγ[α≥β*γ] (b:β, c:γ)        → ((b, c) : β*γ :> α) >>  | Priv [α ≥ priv_int] (n : priv_int) → (n : priv_int :> α) >> >> One would need to study more examples to get a better understanding of >> this question. > > There are certainly examples in both directions. > For instance the "print" example in the manual uses the opposite direction. > And in some cases you are going to want both simultaneously. > Moreover this is very heavy: all subtyping requires type annotations, > while type equalities are directly handled by unification. > This may look like you don't need that many here, but in general > we only currently require type annotations on ambiguous types > when they escape the current case. In some cases this is a tiny > fraction of the uses of equality. > > On the other hand, if you really want variance, this looks like a cleaner solution. > >> # Conclusion and questions >> >> We have a relaxed criterion that we're confident is sound and can >> plausibly be implemented in OCaml (including possibly before the >> next release). But it relies on a closed-world assumption that is >> currently skewed towards covariance because of private types -- not >> a problem for our use case, the relaxed value restriction. Finally, it >> would suggest some language extensions to benefit fully from it, by >> enabling upward/downward closure specification for abstract types, and >> allowing to forbid making a new type `private` in the future >> (or blind) to gain stronger variance properties. >> >> On the other hand, we know that this criterion would not hold as is in >> an open world scenario. Is this consideration relevant to the OCaml >> type system? If one wants to keep the door open to the open world >> case, would the suggested approach (reasoning under subtyping >> constraints in pattern clauses) be implementable? > > For OCaml the problem is abstraction. > I think it has consequences very close to open world, except if you're > willing to add lots of information to interfaces. > >> I don't believe the two choices are exclusive: if we have an >> annotation to say "this type will never be marked private", it becomes >> downward-closed even in an open-world scenario, and we can recover the >> current behavior by saying that all types, by default, "will never be >> marked blind" but "may be marked private". Those defaults are design >> areas to explore. >> >> I would welcome feedback on the current state of affairs. Given what >> we know, is there a hope of relaxing the variance check for GADT at >> some short-to-medium-term point? > > Well, your simplest criterion (just check that the instantiated parameter > is upward-closed, failing on "unknown" abstract types) seems easy enough to check. > The question is whether is it really sufficient in practice. > For all the other annotations, there would need to be a very strong justification. > Honestly, my feeling is just that GADTs do not play well with subtyping, and > there is no really satisfactory solution (except maybe subtyping constraints, but > they are going to be very heavy). > >        Jacques Garrigue