[Caml-list] Polymorphic module type constraints

[Caml-list] Polymorphic module type constraints

[Raphael 'kena' Poss]

Hi all,

I am trying to take advantage of OCaml locally abstract types to constrain a functor. I want to use this to support the creation of modules from user-provided functions and some defaults. I encounter two issues with polymorphic types, which I am unable to solve. Maybe you will have some suggestions?

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?



Now, the other issue is when the signature explicitly declares a polymorphic type:

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

So far so good; but how to define makeMappable function, that takes a map function and Poly module and defines a Mappable instance from them?

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?

Thanks in advance,


-- 
Raphael 'kena' Poss · r.poss@uva.nl
http://staff.science.uva.nl/~poss/

Re: [Caml-list] Polymorphic module type constraints

[Leo White]

> 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