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
Extended package type subtyping #7151
Comments
Comment author: @alainfrisch
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? |
Comment author: @yallop
Right. I left the negative case implicit for brevity, not because I want to favour covariant contexts.
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. |
Comment author: @alainfrisch
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. |
Comment author: @yallop
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
whenever
|
Comment author: @yallop
I don't think that's quite the right model. If it were, then we'd have
but that's not the case: t is injective, and both co- and contra-variant. |
Comment author: @alainfrisch 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. |
Comment author: @yallop
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. |
Comment author: @alainfrisch Ah, ok, so your proposal is really to extend the subtyping of module types, to allow e.g:
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? |
Comment author: @yallop
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.
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. |
Comment author: @yallop
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 F(X: sig type +_ t end) = If we wanted to give type components a representation then as far as I can see there are two options:
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".] |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
These days my preferred approach to handling difficult variance cases is to first implement first-class subtypes and then use those. With first-class subtypes one could write something like:
where All operations in
but those which used |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 7151
Reporter: @yallop
Status: acknowledged (set by @damiendoligez on 2017-04-13T12:20:57Z)
Resolution: open
Priority: normal
Severity: feature
Category: typing
Related to: #5337
Monitored by: runhang @Drup @hcarty
Bug description
Given
module type T = sig type t end
then we have
(module T with type int)
is a subtype of
(module T)
Could we also have
(module T with type t = <m:int;n:float>)
is a subtype of
(module T with type t = <m:int>)
and more generally
(module T with type t = a)
is a subtype of
(module T with type t = b)
whenever a is a subtype of b and t only appears in positive contexts in T?
The text was updated successfully, but these errors were encountered: