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

[vicuna]

Original bug ID: 5078
Reporter: kaustuv
Assigned to: @alainfrisch
Status: resolved (set by @alainfrisch on 2012-01-18T09:42:42Z)
Resolution: suspended
Priority: normal
Severity: feature
Version: 3.12.0+beta1 or 3.12.0+rc1
Category: ~DO NOT USE (was: OCaml general)
Has duplicate: #5140
Monitored by: nlinger

Bug description

The 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 =

instead of

type [] =

for ?

[vicuna]

Comment author: @alainfrisch

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.

[vicuna]

Comment author: nlinger

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.

[vicuna]

Comment author: @alainfrisch

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.

[vicuna]

Comment author: @alainfrisch

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!

[vicuna]

Comment author: kaustuv

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.

[vicuna]

Comment author: @alainfrisch

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!

[vicuna]

Comment author: nlinger

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.

[vicuna]

Comment author: @alainfrisch

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.

[vicuna]

Comment author: @gasche

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?

[vicuna]

Comment author: @alainfrisch

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!