Why parametrized types are not supported in (module package-type)?

Learning
,
1

Let’s say we have a module type M with the following signature:

module type M = sig
    type 'a t
    val x : 'a t
end

and a module ListM:

module ListM : (M with type 'a t = 'a list) = struct
    type 'a t = 'a list
    let x : 'a t = []
end

We could use (module ListM : M) to create a first-class module; however, the type 'a t of M would be unspecified.

With the constraint (module ListM : M with type 'a t = 'a list), the code can’t be compiled according to First-class modules.

The package-type syntactic class appearing in the (module package-type) type expression and in the annotated forms represents a subset of module types. This subset consists of named module types with optional constraints of a limited form: only non-parametrized types can be specified.

I don’t understand why parametrized type constraints are not allowed here. Is this related to the decidability or soundness of typing?

Thanks!

2

I just tried compiling your posted code

module type M = sig
     type 'a t
     val x : 'a t
end
 
module ListM : (M with type 'a t = 'a list) = struct
     type 'a t = 'a list
     let x : 'a t = []
end

And it compiled fine… Why would aliasing a type(or exposing a type) cause problems? Maybe the experts could chime in…

3

You can do:

module type S = M with type 'a t = 'a list
type t = (module S)

The syntax (module S with type t = foo) is a special syntax reserved for exposing types in the module type as parameters of the package type. For example:

type 'a t = (module S with type t = 'a)

Since OCaml does not have higher-kinded type variables (i.e. variables 'a which can be instantiated with type constructors like list) there is no support for the special with syntax for type constructors.

In principle the syntax could be extended to work for constructors even though there are no higher-kinded variables to use with them, but there are a number of issues that would need to be overcome in both the implementation and the design. For example, the whole purpose of the special with type is to allow type variables (i.e. 'a) to be used on the right-hand side of the =, but in your list example there is also an 'a needed for the type parameter – so we’d need to allow some kind of shadowing of type variable names, which is not something OCaml currently has.

6 Likes