Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005078OCamlOCaml generalpublic2010-06-17 00:422013-07-01 15:28
Reporterkaustuv 
Assigned Tofrisch 
PrioritynormalSeverityfeatureReproducibilityalways
StatusresolvedResolutionsuspended 
PlatformOSOS Version
Product Version3.12.0+beta1 or 3.12.0+rc1 
Target VersionFixed in Version 
Summary0005078: <package-type-constraint> does not allow constraints for non-nullary abstract types
DescriptionThe following is rejected because package type constraints as specified in the grammar (sec. 7.14 of the manual) cannot constrain a non-nullary type.

   % ocaml
           Objective Caml version 3.13.0+dev0 (2010-06-07)
   
   # 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 <typeconstr-name> = <typexpr>

instead of

   type [<type-parameters>] <typeconstr-name> = <typexpr>

for <package-type-constraint>?
TagsNo tags attached.
Attached Files

- Relationships
has duplicate 0005140closedfrisch restricted use of constraints in module package 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.
(0009662)
gasche (developer)
2013-07-01 13:41

I occasionally run into this limitation as well (one fairly common example would be parametrizing functions over a first-class 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)
2013-07-01 15:28

> What is the "upstreamability status" of the branch fstclassmod_parametrized?

The type-checking of first-class 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 type-inference 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
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
2013-07-01 13:41 gasche Note Added: 0009662
2013-07-01 15:28 frisch Note Added: 0009663


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker