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

Closed
vicuna opened this issue Feb 16, 2016 · 14 comments
Closed

Extended package type subtyping #7151

vicuna opened this issue Feb 16, 2016 · 14 comments

Comments

@vicuna
Copy link

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

@github-actions
Copy link

github-actions bot commented May 9, 2020

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.

@github-actions github-actions bot added the Stale label May 9, 2020
@Drup
Copy link
Contributor

Drup commented May 9, 2020

@garrigue @lpw25 Do you have an opinion about that feature ? I feel like this could be integrated in the current work on modules, but I'm not sure I'm sold on the feature.

@lpw25
Copy link
Contributor

lpw25 commented May 10, 2020

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:

module type Pos = sig
  type t
  val x : t
  val f : t -> unit
end

type 'a pos' = (module Pos with type t = 'a)

type +'a pos = Pos : (module Pos with type t = 'a) -> 'a pos

where pos' is still invariant but pos is covariant. The definition of Pos can be read as roughly: (∃('b < 'a). (module Pos with type t = 'b)) -> 'a pos.

All operations in Pos that use t in a positive context would be useable like:

let x (type a) (Pos (module M) : a pos) = (M.x :> a)

but those which used t in a negative context wouldn't.

@github-actions github-actions bot removed the Stale label Jun 15, 2020
@github-actions
Copy link

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.

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

No branches or pull requests

3 participants