Nested modules: signature restriction possible?

Nested modules: signature restriction possible?

[Wesley W. Terpstra]

[-- Attachment #1: Type: text/plain, Size: 1731 bytes --]

Hi!

I've been writing code in ocaml that performs various forms of work over
abstract algebra structures. I have been very happy with modules and
functors which allow me to build these structures from algebraic rules.

However, after slowly growing the type system which I need, I've run
into several inefficiencies. I've attached ocaml file in question.

The part that annoys me is how I keep having to make two of every module
type. A normal version and a 'NotNested' version.

For example, you'll see there is a RingNotNested and
CommutativeRingNotNested in addition to a Ring and CommutativeRing
signature. Notice that this mess finds its way into the functors
which create these signatures as well (Make[Commutative]Ring).

I've had to do this because ocaml (and sml) lack both:
  the ability to refine the signature of an 'included' module
    eg: include Ring with module Multiplication : AbelianMonoid
  the ability to rebind a module (the way variables can be re-bound)
    eg: module A = Foo
        ... code ...
        module A = Bar

These features could lead to a more natural formulation, like:

module type Ring =
  sig
    type t
    module Addition : AbelianGroup with type t = t
    module Multiplication : Monoid with type t = t
    val distributive : unit
    val zero : t
    val one  : t
    val eq  : t -> t -> bool
    val add : t -> t -> t
    val sub : t -> t -> t
    val neg : t -> t
    val mul : t -> t -> t
  end

module type CommutativeRing =
  sig
    include Ring
    module Multiplication : AbelianMonoid with type t = t
  end

Is there another way to simplify this code that I am not familiar with?
Would one of the above changes be useful to people more than just me?

-- 
Wesley W. Terpstra

[-- Attachment #2: algebra.ml --]
[-- Type: text/plain, Size: 8452 bytes --]

(****************************************************************** Groups *)

module type SemiGroup =
  sig
    type t
    val associative : unit
    val eq  : t -> t -> bool
    val mul : t -> t -> t
  end

module type Monoid =
  sig
    include SemiGroup
    val one : t
  end

module type AbelianMonoid =
  sig
    include Monoid
    val commutative : unit
  end

module type Group =
  sig
    include Monoid
    val div : t -> t -> t
    val inv : t -> t
  end

module type AbelianGroup =
  sig
    include Group
    val commutative : unit
  end

module type CyclicGroup =
  sig
    include AbelianGroup
    val order : Big_int.big_int
    val generator : t
  end

(****************************************************************** Rings *)

module type RingNotNested =
  sig
    type t
    val distributive : unit
    val zero : t
    val one  : t
    val eq  : t -> t -> bool
    val add : t -> t -> t
    val sub : t -> t -> t
    val neg : t -> t
    val mul : t -> t -> t
  end
module type Ring =
  sig
    include RingNotNested
    module Addition : AbelianGroup with type t = t
    module Multiplication : Monoid with type t = t
  end

module type CommutativeRingNotNested = 
  sig
    include RingNotNested
  end
module type CommutativeRing =
  sig
    include CommutativeRingNotNested
    module Addition : AbelianGroup with type t = t
    module Multiplication : AbelianMonoid with type t = t
  end

module type IntegralDomainNotNested = 
  sig
    include CommutativeRingNotNested
    val no_zero_divisors : unit
  end
module type IntegralDomain =
  sig
    include IntegralDomainNotNested
    module Addition : AbelianGroup with type t = t
    module Multiplication : AbelianMonoid with type t = t
  end

module type EuclideanDomainNotNested =
  sig
    include IntegralDomainNotNested
    val quo : t -> t -> (t * t)
  end
module type EuclideanDomain =
  sig
    include EuclideanDomainNotNested
    module Addition : AbelianGroup with type t = t
    module Multiplication : AbelianMonoid with type t = t
  end

module type FieldNotNested =
  sig
    include IntegralDomainNotNested
    val div : t -> t -> t
    val inv : t -> t
  end
module type Field =
  sig
    include FieldNotNested
    module Addition : AbelianGroup with type t = t
    module Multiplication : AbelianGroup with type t = t
  end

(* note that a finite field does not have a cyclic additive group
 * the additive group can only generate terms up to the characteristic
 *)
module type FiniteFieldNotNested =
  sig
    include FieldNotNested
  end
module type FiniteField =
  sig
    include FiniteFieldNotNested
    module Addition : AbelianGroup with type t = t
    module Multiplication : CyclicGroup with type t = t
  end

(****************************************************************** Functors *)

module MakeRingNotNested(Addition : AbelianGroup)(Multiplication : Monoid with type t = Addition.t) =
  struct
    type t = Addition.t
    let distributive = ()
    let zero = Addition.one
    let one  = Multiplication.one
    let eq   = Multiplication.eq
    let add  = Addition.mul
    let sub  = Addition.div
    let neg  = Addition.inv
    let mul  = Multiplication.mul
  end
module MakeRing(Addition : AbelianGroup)(Multiplication : Monoid with type t = Addition.t) : Ring with type t = Addition.t =
  struct
    include MakeRingNotNested(Addition)(Multiplication)
    module Addition = Addition
    module Multiplication = Multiplication
  end

module MakeCommutativeRingNotNested(Addition : AbelianGroup)(Multiplication : AbelianMonoid with type t = Addition.t) =
  struct
    include MakeRingNotNested(Addition)(Multiplication)
  end
module MakeCommutativeRing(Addition : AbelianGroup)(Multiplication : AbelianMonoid with type t = Addition.t) : CommutativeRing with type t = Addition.t =
  struct
    include MakeCommutativeRingNotNested(Addition)(Multiplication)
    module Addition = Addition
    module Multiplication = Multiplication
  end
  
module MakeIntegralDomainNotNested(Addition : AbelianGroup)(Multiplication : AbelianMonoid with type t = Addition.t) =
  struct
    include MakeCommutativeRingNotNested(Addition)(Multiplication)
    let no_zero_divisors = ()
  end
module MakeIntegralDomain(Addition : AbelianGroup)(Multiplication : AbelianMonoid with type t = Addition.t) : IntegralDomain with type t = Addition.t =
  struct
    include MakeIntegralDomainNotNested(Addition)(Multiplication)
    module Addition = Addition
    module Multiplication = Multiplication
  end
  
module MakeFieldNotNested(Addition : AbelianGroup)(Multiplication : AbelianGroup with type t = Addition.t) =
  struct
    include MakeIntegralDomainNotNested(Addition)(Multiplication)
    let div = Multiplication.div
    let inv = Multiplication.inv
  end
module MakeField(Addition : AbelianGroup)(Multiplication : AbelianGroup with type t = Addition.t) : Field with type t = Addition.t =
  struct
    include MakeFieldNotNested(Addition)(Multiplication)
    module Addition = Addition
    module Multiplication = Multiplication
  end

module MakeFiniteFieldNotNested(Addition : AbelianGroup)(Multiplication : CyclicGroup with type t = Addition.t) =
  struct
    include MakeFieldNotNested(Addition)(Multiplication)
  end
module MakeFiniteField(Addition : AbelianGroup)(Multiplication : CyclicGroup with type t = Addition.t) : FiniteField with type t = Addition.t =
  struct
    include MakeFiniteFieldNotNested(Addition)(Multiplication)
    module Addition = Addition
    module Multiplication = Multiplication
  end

(****************************************************************** Bindings *)

module BindSemiGroupToPercent(S : SemiGroup) =
  struct
    let ( !=% ) x y = not (S.eq x y)
    let ( <>% ) x y = not (S.eq x y)
    let (  =% ) = S.eq
    let ( ==% ) = S.eq
    let (  *% ) = S.mul
  end
module BindSemiGroupToDollar(S : SemiGroup) =
  struct
    let ( !=$ ) x y = not (S.eq x y)
    let ( <>$ ) x y = not (S.eq x y)
    let (  =$ ) = S.eq
    let ( ==$ ) = S.eq
    let (  *$ ) = S.mul
  end
  
module BindMonoidToPercent(M : Monoid) = BindSemiGroupToPercent(M)
module BindMonoidToDollar(M : Monoid) = BindSemiGroupToDollar(M)
module BindAbelianMonoidToPercent(M : AbelianMonoid) = BindMonoidToPercent(M)
module BindAbelianMonoidToDollar(M : AbelianMonoid) = BindMonoidToDollar(M)

module BindGroupToPercent(G : Group) =
  struct
    include BindMonoidToPercent(G)
    let ( /% ) = G.div
    let ( !% ) = G.inv
  end
module BindGroupToDollar(G : Group) =
  struct
    include BindMonoidToDollar(G)
    let ( /$ ) = G.div
    let ( !$ ) = G.inv
  end

module BindAbelianGroupToPercent(G : AbelianGroup) = BindGroupToPercent(G)
module BindAbelianGroupToDollar(G : AbelianGroup) = BindGroupToDollar(G)
module BindCyclicGroupToPercent(G : CyclicGroup) = BindAbelianGroupToPercent(G)
module BindCyclicGroupToDollar(G : CyclicGroup) = BindAbelianGroupToDollar(G)

module BindRingToPercent(R : Ring) = 
  struct
    let ( !=% ) x y = not (R.eq x y)
    let ( <>% ) x y = not (R.eq x y)
    let (  =% ) = R.eq
    let ( ==% ) = R.eq
    let (  +% ) = R.add
    let (  -% ) = R.sub
    let (  ~% ) = R.neg
    let (  *% ) = R.mul
  end
module BindRingToDollar(R : Ring) = 
  struct
    let ( !=$ ) x y = not (R.eq x y)
    let ( <>$ ) x y = not (R.eq x y)
    let (  =$ ) = R.eq
    let ( ==$ ) = R.eq
    let (  +$ ) = R.add
    let (  -$ ) = R.sub
    let (  ~$ ) = R.neg
    let (  *$ ) = R.mul
  end

module BindCommutativeRingToPercent(R : CommutativeRing) = BindRingToPercent(R)
module BindCommutativeRingToDollar(R : CommutativeRing) = BindRingToDollar(R)
module BindIntegralDomainToPercent(I : IntegralDomain) = BindCommutativeRingToPercent(I)
module BindIntegralDomainToDollar(I : IntegralDomain) = BindCommutativeRingToDollar(I)

module BindEuclideanDomainToPercent(E : EuclideanDomain) =
  struct
    include BindIntegralDomainToPercent(E)
    let ( /% ) = E.quo
  end
module BindEuclideanDomainToDollar(E : EuclideanDomain) =
  struct
    include BindIntegralDomainToDollar(E)
    let ( /$ ) = E.quo
  end

module BindFieldToPercent(F : Field) =
  struct
    include BindIntegralDomainToPercent(F)
    let ( /% ) = F.div
    let ( !% ) = F.inv
  end
module BindFieldToDollar(F : Field) =
  struct
    include BindIntegralDomainToDollar(F)
    let ( /$ ) = F.div
    let ( !$ ) = F.inv
  end

module BindFiniteFieldToPercent(F : FiniteField) = BindFieldToPercent(F)
module BindFiniteFieldToDollar(F : FiniteField) = BindFieldToDollar(F)

Re: [Caml-list] Nested modules: signature restriction possible?

[Christian Szegedy]

I am writing a code with almost the same functionality and
I was also bugged by the same problem and posed the same
question in the functional mailing list.

Julien Signoles was kind enough to answer:

> I also encounter this annoying situation. In general, I solve it in the
> following way:
> 
> module type A = sig type t val f: t -> t end
> module type B = sig include A val g: t -> t end
> module type C' = sig type c val h: c -> c end
> module type C = sig include A include C' with type c = t end
> module type D = sig include B include C' with type c = t end
> 
> Sadly, this solution uses some additional types and with-type constraints
> but IMHO it is the best when your signatures are big.
> 
> Hope this helps,

I've got a similar algebra package as yours, but my design is quite
pragmatic: I have only programmed those parts I really needed.
I send my version in a separate mail.

It would be fun to cooperate, if you would like to.

(What I currently think about is the GCD computation over multivariate 
polynomial fields (it is needed for the functions field), and it
is hard to get it efficient. After I solved it, I will want to programm
Groebner base manipluation.)

Best regards, Christian