Re: [Caml-list] Polymorphic module type constraints

[Leo White <lpw25@cam.ac.uk>]

> To show what I want, here is an example that "works fine" but uses regular types:
>
>   module type Eq = sig
>       type t
>       val (=) : t -> t -> bool
>       val (<>) : t -> t -> bool
>     end
>
>   let makeEq (type a) eq =
>     let module S  = struct
>       type t = a
>       let (=) = eq
>       let (<>) x y = not (x = y)
>     end
>     in (module S : Eq with type t = a)
>
>   (* val eq1: int -> int -> bool *)
>   let eq1 a b = (a mod 3) = (b mod 3)
>   module Eq1 = (val makeEq eq1)
>
> Here, I encounter the first issue:
>
>   (* val eq2: 'a option -> 'a option -> bool *)
>   let eq2 a b = match (a, b) with
>       | (None, None) -> true
>       | (Some x, Some y) -> x = y
>       | _ -> false
>
>   module Eq2 = (val makeEq ~eq2)
>
>   =>
>   Error: The type of this packed module contains variables:
>   (module Eq with type t = 'a option)
>
> Is there any way to generalize?

It is not clear what module type you expect `Eq2` to have. The following
type does not make any sense:

    sig
      type t = 'a option
      val (=) : t -> t -> bool
      val (<>) : t -> t -> bool
    end

because the type variable `'a` is not bound. On the other hand:

    sig
      type 'a t = 'a option
      val (=) : 'a t -> 'a t -> bool
      val (<>) : 'a t -> 'a t -> bool
    end

is not an instance of `Eq` which is the module type of `makeEq eq1`.

In addition `makeEq eq2` has type `(module Eq with type t =
'_a option)`. Note that the type variable '_a is weakly
polymorphic. This is due to the value restriction: `makeEq` may create
some state which is used in its returned module, meaning it cannot
safely be polymorphic.

> My first try:
>
>   let makeMappable1 (type s) (module O : Poly with type t = s) map =
>     let module S : Mappable with type 'a t = 'a O.t = struct
>        include O
>        let map : ('a -> 'b) -> 'a t -> 'b t = map
>     end
>     in (module S)
>
>   => 
>   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
>
> Ok, fair enough:
>
>   let makeMappable2 (type s) (module O : Poly with type 'a t = s) map =
>     let module S : Mappable with type 'a t = 'a O.t = ...
>
>   =>
>   Error: Syntax error: module-expr expected. (location: with type ... on first line)
>
> So, I try to fix this with:
>
>   let makeMappable3 (module O : Poly) map =
>     let module S : Mappable with type 'a t = 'a O.t = struct
>        include O
>        let map : ('a -> 'b) -> 'a t -> 'b t = map
>     end
>     in (module S)                                                                                                                                          
>
>   =>
>   Error: This expression has type ('a -> 'b) -> 'a O.t -> 'b t
>        but an expression was expected of type ('a -> 'b) -> 'a O.t -> 'b t
>        The type constructor O.t would escape its scope
>
> Any suggestion as to how to define makeMappable?

The function `makeMappable` that you are trying to write is polymorphic
in a type constructor (`O.t`), in other words it is higher-kinded. The
core OCaml type system does not support higher-kinded polymorphism, and
the traditional solution is to use functors:

    module MakeMappable (O : Poly) (M : Mappable with type 'a t := 'a O.t) = struct
      type 'a t = 'a O.t
      let map = M.map
    end

Of course, this particular functor is pretty redundent.

(A possible alternative is to use the higher library with the approach
described in: https://github.com/ocamllabs/higher/raw/paper/higher.pdf)

Regards,

Leo