Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007151OCamltypingpublic2016-02-16 20:202018-04-08 09:36
Reporteryallop 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0007151: Extended package type subtyping
DescriptionGiven

   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?
TagsNo tags attached.
Attached Files

- Relationships
related to 0005337assignedgarrigue variance not inferred for package type 

-  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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker