0007151: Extended package type subtyping

Notes
(0015366) frisch (developer) 2016-02-17 09:29	> (module T with type t = <m:int;n:float>) is a subtype of (module T with type t = <m:int>) If the criterion is that this holds only if t appears in "positive context", then one should allow the opposite subtyping if t only appears in "negative context" (there is no reason to favor covariance over contravariance). This means that if t is not used at all (as in your first examples), one should have: (module T with type t = ...) <= (module T with type t = ...) for arbitrary type expressions. I have to say that I'm not convinced this is going into the right direction. In a would-be dynamic semantics where types would be kept explicitly, it would not make sense to allow subtyping on manfest type components in packaged module types. Can you describe some specific cases that would benefit from the proposal?

(0015367) yallop (developer) 2016-02-17 09:50	> If the criterion is that this holds only if t appears in "positive context", then one should allow the opposite subtyping if t only appears in "negative context" (there is no reason to favor covariance over contravariance). Right. I left the negative case implicit for brevity, not because I want to favour covariant contexts. > This means that if t is not used at all (as in your first examples), one should have: > > (module T with type t = ...) <= (module T with type t = ...) > > for arbitrary type expressions. Yes. We currently have that behaviour for other type constructors; for example, given this definition type 'a t = T then the following holds a t <= b t for any 'a' and 'b'. It seems reasonable for that existing behaviour to be extended to package types.

(0015368) frisch (developer) 2016-02-17 09:54	> It seems reasonable for that existing behaviour to be extended to package types. My intuition is that the situation is (and should be) rather different. A definition "type 'a t = T" is like a constant function from types to types; it returns a constant value so it is normal that "a t <= b t". But "(module T with type t = ...)" is more like a constraint on module types, and "sig type t = <m:int;n:float> end" cannot be seen as a subtype of "sig type t = <m:int>" for obvious reasons. It feels weird to allow some subtyping on package type than on the corresponding module types.

(0015369) yallop (developer) 2016-02-17 09:55	> Can you describe some specific cases that would benefit from the proposal? Here's one example. The following definition witnesses the fact that 'a' is a subtype of 'b': module type SUB = sig type a and b module Coerce(S: sig type +_ t end) : sig val coerce : a S.t -> b S.t end end type ('a, 'b) sub = (module SUB with type a = 'a and type b = 'b) It would be nice if the parameters of 'sub' were properly contra- and covariant, so that (a, b) sub <= (c, d) sub whenever b <= d c <= a

(0015370) yallop (developer) 2016-02-17 10:00	> A definition "type 'a t = T" is like a constant function from types to types; it returns a constant value so it is normal that "a t <= b t". I don't think that's quite the right model. If it were, then we'd have a t == b t but that's not the case: t is injective, and both co- and contra-variant.

(0015371) frisch (developer) 2016-02-17 10:04	Well, it depends on what you mean by "==". The types are equivalent for the equality induced by the subtyping relation. They are different for the stricter notion of equality used by the type system, but I'm not sure this is relevant here.

(0015372) yallop (developer) 2016-02-17 10:16	> sig type t = <m:int;n:float> end" cannot be seen as a subtype of "sig type t = <m:int>" for obvious reasons Do you mean that it's not a subtype in the current design, or that there's a fundamental reason (e.g. soundness) why the design couldn't possibly be extended to make it a subtype? I'd quite like to have the subtyping relation lifted to the module level, so I'm curious to know whether there's some reason that wouldn't be possible.

(0015373) frisch (developer) 2016-02-17 10:49	Ah, ok, so your proposal is really to extend the subtyping of module types, to allow e.g: module X : sig type t = <m:int> end = struct type t = <m:int;n:int> end This would significantly complexify the inclusion check on signatures; it would need to check all occurrences of the type t in the rest of the signature to know which subtyping direction is allowed on the manifest type. It would also make the notion more complex to explain. Do we even have a clear specification of what it means for a type to be used only in positive or negative positions? (in particular, if it is used in another type definition, it seems we would need to perform a rather complex fix point analysis, as for the current variance inference, but lifted to the full module language). A lot of work in perspective. I see the idea of your "witnessing subtyping" example; but can you give a practical application of this ablility to represent subtyping as the value level?

(0015374) yallop (developer) 2016-02-17 11:21	> Ah, ok, so your proposal is really to extend the subtyping of module types, to allow e.g: At the moment, I'm only interested in package subtyping. If value subtyping were extended to modules then I think it'd be better to have an explicit coercion rather than simply to extend the existing signature inclusion operation. But that's a discussion for another time! I agree that there might be subtleties involved, which is why this PR is phrased a question rather than an outright proposal. I'd like to have package type variance, but I'm wondering if there's some reason why it's trickier than I imagine. > I see the idea of your "witnessing subtyping" example; but can you give a practical application of this ablility to represent subtyping as the value level? Yes: there are several such applications. The use cases are similar to the things you can do with GADTs, but allow you to turn evidence for propositions (e.g. a vector has length n, or a file descriptor can be used for reading and writing) into evidence for weaker propositions (e.g. a vector has length at least m <= n, or a file descriptor can be used for reading) without performing any computation.

(0015389) yallop (developer) 2016-02-23 12:42 edited on: 2016-02-23 12:44	> In a would-be dynamic semantics where types would be kept explicitly, Is there a concerete proposal for such a dynamic semantics anywhere? The idea doesn't seem to fit very harmoniously with the existing OCaml design. For example, consider the behaviour of package subtyping in the current OCaml release. Since subtyping is defined structurally, and since type components have no representation, the following program is accepted module type RST = sig type r type s type t end module type TS = sig type t type s end module F(X: sig type +_ t end) = struct let f (x: (module RST) X.t) = (x :> (module TS) X.t) end If we wanted to give type components a representation then as far as I can see there are two options: 1. make programs like this invalid, breaking backwards compatibility 2. use a complicated representation for type components, along the lines of objects Neither of these seems appealing. [Update: I've fixed the example, which originally coerced a value of type "(module RST)" instead of "(module RST) X.t".]

Issue History
Date Modified	Username	Field	Change
2016-02-16 20:20	yallop	New Issue
2016-02-17 09:29	frisch	Note Added: 0015366
2016-02-17 09:50	yallop	Note Added: 0015367
2016-02-17 09:54	frisch	Note Added: 0015368
2016-02-17 09:55	yallop	Note Added: 0015369
2016-02-17 10:00	yallop	Note Added: 0015370
2016-02-17 10:04	frisch	Note Added: 0015371
2016-02-17 10:16	yallop	Note Added: 0015372
2016-02-17 10:49	frisch	Note Added: 0015373
2016-02-17 11:21	yallop	Note Added: 0015374
2016-02-23 12:42	yallop	Note Added: 0015389
2016-02-23 12:44	yallop	Note Edited: 0015389	View Revisions
2016-12-07 16:44	yallop	Relationship added	related to 0005337
2017-02-23 16:45	doligez	Category	OCaml typing => typing
2017-04-13 14:20	doligez	Status	new => acknowledged