Polymorphic Functors in OCaml (related to Include command)

Question

EDIT: I replaced abstract example with module type A and B by a more concrete example using groups and rings.

I present my problems with functors on an example using well-known algebraic structure. Define a signature for groups:

module type Group = 
sig
    type t
    val neutral: t
    val add: t -> t -> t
    val opp: t -> t
end

And define a signature for groups that contains many useful operations, e.g. here conjugation:

module type Extended_Group =
sig
    include Group
    val conjugate: t -> t -> t
end

Implementation for conjugation depends only on addition and opposite, so I don't want to write it explicitly for all groups I define, so I write the following functor:

module F (G: Group) =
struct
    include G
    let conjugate x y = add (add x y) (opp x)
end

Now, suppose you are working with other structures that "extend" the notion of group, for instance the ring of integers:

module Z = 
struct
    (* Group *)
    type t = int
    let neutral = 0
    let add x y = x+y
    let opp x = -x
    (* Ring *)
    let m_neutral = 1
    let mult x y = x*y
end

Since a ring is a particle case of group, we can apply functor F to it:

module Extended_Z = F(Z)

Unfortunately, to apply F to Z, Ocaml first restrict the type of Z to Group, and then apply F. Everything behaves exactly as if I did this:

module (Group_Z: Group) = Z
module Extended_Z = F(Group_Z)

And thus, eventhough Z.mult makes sense, Extended_Z.mult is unknown to the compiler. I don't want to lose the fact that Extended_Z is still a ring ! Of course, the solution that consist in writing a functor F_Ring that does just like F but taking a Ring as input is not a satisfying one: I don't want to write F_Fields, F_VectorSpace, and so on.

Here is what I would want:

1. Either a way to extend the signature of a module, to expose more values. It is possible to do it the other way, restricting the signature of a module (with the syntax I used for Group_Z), but I can't find a way to enlarge a signature. Here it would be something like:

   module (Ring_Extended_Z: Ring) = Extended_Z
   

2. Or, a way to define polymorphic functors, that is defining a functor F that takes a module of signature "at least Group" and output a module of signature "at least Extended_Group". Of course, this makes sense only in presence of include, which is why I strongly believe such a feature does not exist in OCaml.

After searching for several days for answers on the Internet, I think the correct way to achieve this is actually the following one: (Inspired from chapter 9 of Real World OCaml)

module F (G: Group) =
struct
    let conjugate x y = ...
end

(same as previously but without the include) and then perform all the includes at the same point:

module Extended_Z =
struct
    include Z
    include F(Z)
end

Can someone confirm that this is the good way to achieve what I want, and that my first approach does not fit the spirit of OCaml ? More specifically, can someone confirm that options 1. and 2. are indeed impossible in OCaml ?

EDIT: Concerning dynamic typing

It seems to me that this is still static typing, since if I write

module Extended_Z = F(Z: Ring)

OCaml could still type this statically as a module that has signature Ring with the extra value "conjugate". It requires polymorphism at the module level, which I understand does not exist, but I think it could exist without making the type system dynamic.

Answer 1

I share in this answer the two partially-satisfying solution I have found to implement what I wanted.

The first one is the one suggested at the end of my question, and in the case of algebraic structure is probably the "good" one.

module type Group = 
sig
    type t
    val neutral: t
    val add: t -> t -> t
    val opp: t -> t
end

module type Extended_Group =
sig
    include Group
    val conjugate: t -> t -> t
end

module F (G: Group) =
struct
    let conjugate x y = G.add (G.add x y) (G.opp x)
end

module type Ring = 
sig
    include Group
    val m_neutral: t
    val mult: t -> t -> t
end

module Z = 
struct
    type t = int
    let neutral = 0
    let add x y = x+y
    let opp x = -x
    (* Ring *)
    let m_neutral = 1
    let mult x y = x*y
end

module Extended_Z = 
struct
    include Z
    include F(Z)
end

In this case, the signature of Extended_Z inferred by OCaml "extends" the signature Ring, and indeed Extended_Z.mult is visible outside the module.

The second solution uses pieces of what Andreas Rossberg and Ivg suggested to simulate polymorphism at the module level. It is less satisfying in the case of algebraic structure, but for my actual problem it is just perfect.

module type Group_or_More =
sig
    include Group
    module type T
    module Aux: T
end

module F (G: Group_or_More) =
struct
    include G
    let conjugate x y = add (add x y) (opp x)
end


module Z = 
struct
    type t = int
    let neutral = 0
    let add x y = x + y
    let opp x = -x
    module type T = 
        sig
            val m_neutral: t
            val mult: t -> t -> t
        end
    module Aux = 
        struct
            let m_neutral = 1
            let mult x y = x*y
        end
end


module Extended_Z = F(Z) ;;

Here, the signature Group_or_More captures exactly this idea that I had of a signature extending another. You put everything extra into the auxiliary module Aux. But, in order to be able to provide as many auxiliary functions as one wants, you specify the signature of this Aux module as part of your group.

For algebraic structure, it is less satisfying since Z and Extended_Z are rings in a weaker sense: multiplication is accessed by Z.Aux.mult and Extended_Z.Aux.mult.