Q: module dependent class bindings?

Messing around with module dependent functions, I discovered that class bindings in OCaml 5.5 cannot be module dependent. To illustrate (does not compile):

module type S = sig type t val show: t -> string end
module N = struct type t let show = string_of_int end
class c (module M : S) (v : M.t) = object method show = M.show v end

I’m not sure I understand why this shouldn’t be possible. Could someone with better PL type-theory chops explain why this doesn’t work? I’m really curious.

First, your example is not a valid class definition even without the module argument.

class c show v = object
  method show = show v
end

Error: Some type variables are unbound in this type:
class c : ('a → 'b) → 'a → object method show : 'b end
The method show has type 'b where 'b is unbound

Indeed, polymorphic classes require explicit type parameters:

class ['a] c (show:'a -> string) v = object
  method show = show v
end

Adding support for module-dependent functions would require to add module-dependent type parameters for classes at the very least, and possibly a separate notion for the types of classes.

Then, there is also the question of the interactions between local modules and all the type inference machinery for classes and inheritance which is still left open nowadays. From my memory, this is why local module definitions are not allowed in class bindings:

class c =
   let module M = struct type t = A end in
   object end

Error: Syntax error

Overall, my impression is that adding support for module-dependent classes is a risky endeavor in term of complexity, in an area which has not really attracted many contributors or interests.

Okay, but could you say more about the risk? It’s not clear to me what “module-dependent type parameters for classes” means or why it would be necessary to add them if class functions were permitted to have module-dependent parameters.

It seems like it shouldn’t be much different than a class definition like this:

class oof v = object val v_ = v method f = () end

The class specification for this:

class oof : 'a -> object val v_ : 'a method f : unit end

I’m not sure I see why a module-dependent class function should require its class binding to contain any type parameters. Can you elaborate, please?

A class is not a function (the way class types are printed is misleading).
Classes are second-class citizens in OCaml. Only objects can be manipulated like normal values.
If you write functions that return objects, you can use module dependent arrows without any issue:

module type S = sig type t val show: t -> string end
module N = struct type t = int let show = string_of_int end
let c (module M : S) (v : M.t) = object method show = M.show v end

It’s probably not solving your problem though: if you use classes, you’re probably using inheritance, which doesn’t work with objects.
As a workaround, you can parametrize a class on a module by wrapping it in a functor:

module type S = sig type t val show: t -> string end
module N = struct type t = int let show = string_of_int end
module Class_maker (M : S) = struct
  class c (v : M.t) = object method show = M.show v end
end

Using it is inconvenient though. There are restrictions on where you can put functor applications, so in practice you have to first bind the functor application to a module before you can use the class.

The intuition I have is that a class binding is definitely not a function in the context of an inherit field in a class body, but I struggle to see how it differs from any other ordinary function in the context of a new operator.

What am I missing?

new creates a regular value from a class. The type of this value is computed from the signature of the class. If the class language had support for dependent parameters, then it would be possible to translate a class with dependent parameters into a dependent function. But the class language doesn’t have support for dependent parameters, and it is sufficiently distinct from the normal expression language that adding support would require significant effort (if it is possible at all).

I am still confused. I’m not asking about why classes cannot have module-dependent parameters. I’m asking about why the class function does not allow module-dependent parameters.

I keep getting answers that explain that adding module-dependent parameters to the class would be necessary, and I don’t understand why that should be necessary if class function parameters are to have them.

I feel like I must be missing something important, and I don’t know what it is. When I read the language manual, it seems pretty clear to me that class parameters and class function parameters are two different parameters lists, i.e. the first is a list of possibly constrained universally quantified type variable bindings, and the second comprises the parts of an ordinary arrow type that ends in an object type derived from the class body.

It’s that arrow type that seems to me like it could be module-dependent, and I keep getting answered with an assertion that it would mean the first list of parameters would need to support module-dependence, and that just confuses me. Before I can even think about how that would work, I get stuck on why it’s even necessary.

What am I missing?

I might have used the wrong terminology. Consider the following class:

class c ['a] (x : 'a) = object method x = x end

To me, 'a is a type parameter of the class, and x is a class parameter.
The signature for the class would look like this:

class c : class ['a] c : 'a -> object method x : 'a end

The arrow in the signature above is not a regular arrow (in fact the right-hand side is not a valid type).
Here is what happens with new:

# let mk_c = new c;;
val mk_c : 'a -> 'a c = <fun>

So new converts class types into regular types, where class arrows translate to regular arrows and concrete classes translate to object types.

Hopefully that makes what I wrote earlier a bit more coherent ?

@jhw Sorry, I was slightly confused in my initial comment, and missed that your initial example with the type annotation do not have a free type variable in the object type but only a type variable in the class type through the type of the instance value x . This may have fueled your confusion.

However, the point remains that class type parameters must bind the free types that appears in the object type still hold. You cannot completely separate the two.

Going back to your example, it would have a signature type that looks like

class c: (module M:Showable) -> M.t ->
  object
    val x: M.t
    method show: string
  end

In this case, the dependency on M does not appear in the object type

#c: < show:string; .. >

and thus adding a module parameter to the type parameters class would probably not be required.
However, the resulting class type is still dependent on the module (through val x:M.t). I expect that this dependent type might require careful handling in inheritance and class constraints. Nevertheless, my overall feeling is that this special case of module-dependent class with no dependency in the object type may possibly work (with a non-trivial amount of work).

At the same time this is really a special case, and supporting this case and not

class [?] c (module M:Showable) -> object
  method compare: M.t -> M.t -> string
end

would feel strange and limiting to me, and this case would really require a notion of module parameter of a class type.

Thanks. That is the answer to my question that I needed and that I was hoping to elicit. My intuition is that it’s not a major theoretical problem, provided that a syntax could be found that makes it ergonomically pleasing. I’m happy to set that question aside for now.