0005078: <package-type-constraint> does not allow constraints for non-nullary abstract types

Notes
(0005562) frisch (developer) 2010-06-17 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) 2010-07-29 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) 2010-07-29 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 type-based operations.

(0005655) frisch (developer) 2010-09-09 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) 2010-09-13 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 non-nullary 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) 2010-09-13 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 (implicit-unpack) which improves a lot the support for first-class 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 with-constraints in package types. These extensions might not play so well with with-constraints extended on parametrized types. So if you have a good case for this extension, this is the time to describe it!

(0005659) nlinger (reporter) 2010-09-13 17:43	The primary reason I have for wanting with-constraints 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 With-constraints over the t component of these signatures allows one to express 1. higher-rank 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 locally-free type variable 'a in the with-constraint) 2. Lighter-weight existentials: For example, the pseudo-type "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 non-trivial barrier to entry for using fancy types like these.

(0006719) frisch (developer) 2012-01-18 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 well-tested patch, we will happily consider it for inclusion, though.

Issue History
Date Modified	Username	Field	Change
2010-06-17 00:42	kaustuv	New Issue
2010-06-17 09:33	frisch	Status	new => assigned
2010-06-17 09:33	frisch	Assigned To	=> frisch
2010-06-17 09:38	frisch	Note Added: 0005562
2010-06-17 09:39	frisch	Status	assigned => acknowledged
2010-07-29 20:17	nlinger	Note Added: 0005630
2010-07-29 20:34	frisch	Note Added: 0005631
2010-09-07 18:01	frisch	Relationship added	has duplicate 0005140
2010-09-09 20:31	frisch	Note Added: 0005655
2010-09-13 17:14	kaustuv	Note Added: 0005657
2010-09-13 17:20	frisch	Note Added: 0005658
2010-09-13 17:43	nlinger	Note Added: 0005659
2012-01-18 10:42	frisch	Note Added: 0006719
2012-01-18 10:42	frisch	Status	acknowledged => resolved
2012-01-18 10:42	frisch	Resolution	open => suspended