Skip to content
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

Open
vicuna opened this Issue Feb 16, 2016 · 10 comments

Comments

Projects
None yet
1 participant
@vicuna
Copy link
Collaborator

vicuna commented Feb 16, 2016

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?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

Comment author: @alainfrisch

(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?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

Comment author: @yallop

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

Comment author: @alainfrisch

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

Comment author: @yallop

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

Comment author: @yallop

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

Comment author: @yallop

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

Comment author: @alainfrisch

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?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 17, 2016

Comment author: @yallop

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 23, 2016

Comment author: @yallop

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.