Parametric locally abstract type

Question

I'm trying to figure out how to write a function depending on a module with a parametric type but I can't find anything similar anywhere. I tried to reduce the problem as much as possible and ended up with this dummy example.

module type Mappable = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

let plus (type m) (module M : Mappable with type 'a t = 'a m) (xs : int m) = 
  M.map (fun x -> x + 1) xs

which yields the error Error: Syntax error: module-expr expected.

If I drop the 'a, I end up with the following error.

Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained signature:
       Type declarations do not match: type t is not included in type 'a t
       They have different arities.

What's the correct syntax to do this?

Answer 1

I believe what you want to do here is impossible in OCaml 4.02.3. Let see a simplified version without the type variable:

module type Mappable = sig
  type t
  val map : ('a -> 'b) -> t -> t
end

let plus (type m) (module M : Mappable with type t = m) (xs : m) = 
  M.map (fun x -> x + 1) xs

The above is typable and plus has the following type:

val plus : (module Mappable with type t = 'm) -> 'm -> 'm

the type m in its definition is abstracted to a variable 'm.

Now, back to your original code and think what the type plus is supposed to have. Since you are trying to abstract m by (type m), it should be:

val plus : (module Mappable with type 'a t = 'a 'm) -> 'a 'm -> 'a 'm

Unfortunately, OCaml does not support the higher kinded polymorphism which allows this form of type 'a 'm. It seems the first class module typing is carefully implemented not to introduce it.

You can see the following short paper which explains the current (unfortunate) status of the higher kinded polymorphism in OCaml. This explains a workaround: how to encode it in the current OCaml framework with a cost of explicit coersions:

https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf

I have never tried by myself but the same workaround could be applied to your example.

Answer 2

It is not possible in OCaml, as the type constraint is not a regular module type constraint, but a special syntactic construct, that doesn't allow polymorphic types:

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.

A usual workaround would be to create a module that binds all type variables to concrete types:

module type Mapper = sig 
  type a
  type b
  type src
  type dst
  val map : (a -> b) -> src -> dst
end

let plus (type src) (type dst)
    (module M : Mapper with type dst = dst
                        and type src = src
                        and type a = int
                        and type b = int) (xs : src) : dst =
  M.map (fun x -> x + 1) xs

In your particular example, there is no need to bind 'a and 'b, since they're essentially not used, so it can be simplified to:

module type Mapper = sig 
  type src
  type dst
  val map : ('a -> 'b) -> src -> dst
end

let plus (type src) (type dst)
    (module M : Mapper with type dst = dst
                        and type src = src) (xs : src) : dst =
  M.map (fun x -> x + 1) xs

Of course, this is very limiting, but this is what is possible to the day.

Answer 3

If you want to pass modules to functions, you should use functors instead:

module F (M : Mappable) = struct
  let plus xs = M.map (fun x -> x + 1) xs
end