Anonymous  Login  Signup for a new account  20140918 05:37 CEST 
Main  My View  View Issues  Change Log  Roadmap 
View Issue Details [ Jump to Notes ]  [ Issue History ] [ Print ]  
ID  Project  Category  View Status  Date Submitted  Last Update  
0005078  OCaml  OCaml general  public  20100617 00:42  20130701 15:28  
Reporter  kaustuv  
Assigned To  frisch  
Priority  normal  Severity  feature  Reproducibility  always  
Status  resolved  Resolution  suspended  
Platform  OS  OS Version  
Product Version  3.12.0+beta1 or 3.12.0+rc1  
Target Version  Fixed in Version  
Summary  0005078: <packagetypeconstraint> does not allow constraints for nonnullary abstract types  
Description  The following is rejected because package type constraints as specified in the grammar (sec. 7.14 of the manual) cannot constrain a nonnullary type. % ocaml Objective Caml version 3.13.0+dev0 (20100607) # module type S = sig type 'a t end ;; module type S = sig type 'a t end # let f (m : (module S with type 'a t = 'a * int)) = m ;; ^ Syntax error: ')' expected, the highlighted '(' might be unmatched Is there a technical reason to limit oneself to type <typeconstrname> = <typexpr> instead of type [<typeparameters>] <typeconstrname> = <typexpr> for <packagetypeconstraint>?  
Tags  No tags attached.  
Attached Files  
Relationships  

Notes  
(0005562) frisch (developer) 20100617 09:38 
Yes, there is a technical reason, related to type inference and unification. Currently, two package types (S with t1=T1 and ... and tn=Tn) and (S' with t1'=T1' and ... tm=T'm) are equal if and only if S and S' are the same path, n = m, ti=ti' (modulo permutation) and Ti=T'i for all i. This gives a simple unification procedure for package types. Allowing parametrized types in constraints within package types should be possible by using a more complex definition of equality and unification, but this is not completely straightforward. 
(0005630) nlinger (reporter) 20100729 20:17 
Here is a proposed generalization to packaged module type unification. unify (module A with (as1)t1 = T1 ... (asn)tn = Tn) and (module B with (bs1)s1 = S1 ... (bsn)sn = Tm) = begin ensure A = B (as paths) ensure n = m (as numbers) find a permutation p of {1..n} such that for each i in {1..n} t(i) = s(p(i)) (as names) for each i in {1..n} ensure that as(i) and bs(p(i)) have the same length m (as sequences of type variables) T := T(i) S := S(p(i)) for j in {1..m} create a fresh abstract type variable cj T := T with cj substituted for a(j) S := S with cj substituted for b(p(j)) unify T and S ensure that no c in {c1..cm} has escaped into the type environment. end This seems sound. The only tricky part is the check that c has not escaped into the type environment. Hopefully one could reuse for this purpose some the the machinery used to determine which type variables can be generalized at a let binding. 
(0005631) frisch (developer) 20100729 20:34 
For the implementation, I believe one should be able to reuse some machinery introduced for polymorphic methods. An equality like: (module S with type ('a, 'b) t = T) == (module S with type ('a, 'b) t = S) should behave as the equality: < m : 'a 'b. T > = < m : 'a 'b. S > This might give some guidance on how to extend all the typebased operations. 
(0005655) frisch (developer) 20100909 20:31 
The branch fstclassmod_parametrized in the OCaml SVN repository allows more kinds of constraints (in particular, constraints on parametrized types). Feel free to try it! 
(0005657) kaustuv (reporter) 20100913 17:14 
Awesome! Thanks. I have been playing with it for a few hours and it appears to be expressive enough for at least the use case this bug report was originally triggered by (phantom type parameters). The next obstacle I face is for something like this: module type T = sig type 'a t end let f (m : (module T)) = m let g (m : (module T with type 'a t = 'a * int)) = f m I understand why the expression "f m" above is rejected. I would have preferred if constrained module types induced a subtyping relationship so that I might have written, for example, "f (m :> (module T))". It forces me to duplicate some code  precisely, the code for f. However, unlike the ability to constrain nonnullary types, which was a show stopper, this duplication is only half a dozen lines in my actual code. It is probably not worth complicating the implementation of first class modules to handle this kind of subtyping. I'm not filing a separate feature request. 
(0005658) frisch (developer) 20100913 17:20 
You can simulate subtyping by unpacking and repacking: let g m = let module M = (val m : module T with type 'a t = 'a * int) in f (module M : module T) Jacques Garrigue is working on another branch (implicitunpack) which improves a lot the support for firstclass modules. Explicit package types become optional in (val expr) and (module M) forms, whenever the package type can be inferred. Also, explicit subtyping allows to forget withconstraints in package types. These extensions might not play so well with withconstraints extended on parametrized types. So if you have a good case for this extension, this is the time to describe it! 
(0005659) nlinger (reporter) 20100913 17:43 
The primary reason I have for wanting withconstraints on parameterized types is a straightforward encoding of universal and existential quantifiers like so module type Exists = sig type 'a t type a val witness : a t end module type Forall = sig type 'a t val poly : 'a t end Withconstraints over the t component of these signatures allows one to express 1. higherrank polymorphism: For example, the haskell type "(forall s. ST s a) > a" is straightforwardly encoded as "(module Forall with type 's t = ('s, 'a) st_monad) > 'a" (note the locallyfree type variable 'a in the withconstraint) 2. Lighterweight existentials: For example, the pseudotype "unit > exists a. (a * (a > int))" is straightforwardly encoded as "unit > (module Exists with type 'a t = 'a * ('a > int))" In both cases, one avoids the need to introduce an auxiliary module type with the appropriate instantiation of [t], which seems like a nontrivial barrier to entry for using fancy types like these. 
(0006719) frisch (developer) 20120118 10:42 
I mark this issue as suspended for now. This means that while we consider this as an interesting feature request, no core developer is currently interested in working on it. If someone can submit a short and welltested patch, we will happily consider it for inclusion, though. 
(0009662) gasche (developer) 20130701 13:41 
I occasionally run into this limitation as well (one fairly common example would be parametrizing functions over a firstclass module describing a monad). Has there been any change to the status of this discussion since january 2012? What is the "upstreamability status" of the branch fstclassmod_parametrized? 
(0009663) frisch (developer) 20130701 15:28 
> What is the "upstreamability status" of the branch fstclassmod_parametrized? The typechecking of firstclass module has changed a lot since then (to support type inference), so it won't be possible to integrate the branch in its current state. I've no idea if typeinference interacts well with this feature or not. Hopefully, Jacques will be able to give a more useful answer! 
Issue History  
Date Modified  Username  Field  Change 
20100617 00:42  kaustuv  New Issue  
20100617 09:33  frisch  Status  new => assigned 
20100617 09:33  frisch  Assigned To  => frisch 
20100617 09:38  frisch  Note Added: 0005562  
20100617 09:39  frisch  Status  assigned => acknowledged 
20100729 20:17  nlinger  Note Added: 0005630  
20100729 20:34  frisch  Note Added: 0005631  
20100907 18:01  frisch  Relationship added  has duplicate 0005140 
20100909 20:31  frisch  Note Added: 0005655  
20100913 17:14  kaustuv  Note Added: 0005657  
20100913 17:20  frisch  Note Added: 0005658  
20100913 17:43  nlinger  Note Added: 0005659  
20120118 10:42  frisch  Note Added: 0006719  
20120118 10:42  frisch  Status  acknowledged => resolved 
20120118 10:42  frisch  Resolution  open => suspended 
20130701 13:41  gasche  Note Added: 0009662  
20130701 15:28  frisch  Note Added: 0009663 
Copyright © 2000  2011 MantisBT Group 