From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <pierre.weis@inria.fr>
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39])
	by yquem.inria.fr (Postfix) with ESMTP id 355D9BC29
	for <caml-list@yquem.inria.fr>; Sun,  7 Nov 2004 00:40:04 +0100 (CET)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iA6Ne3im017042
	for <caml-list@yquem.inria.fr>; Sun, 7 Nov 2004 00:40:03 +0100
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id AAA30938 for <caml-list@pauillac.inria.fr>; Sun, 7 Nov 2004 00:40:03 +0100 (MET)
Received: from paris.dvs1.informatik.tu-darmstadt.de (paris.dvs1.informatik.tu-darmstadt.de [130.83.166.129])
	by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iA6Ne2U4017038
	(version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO)
	for <caml-list@inria.fr>; Sun, 7 Nov 2004 00:40:02 +0100
Received: by paris.dvs1.informatik.tu-darmstadt.de (Postfix, from userid 11060)
	id 4FEE64EBE9; Sun,  7 Nov 2004 00:40:02 +0100 (CET)
Date: Sun, 7 Nov 2004 00:39:58 +0100
From: "Wesley W. Terpstra" <terpstra@gkec.tu-darmstadt.de>
To: caml-list@inria.fr
Subject: Nested modules: signature restriction possible?
Message-ID: <20041106233957.GA7443@muffin>
Mime-Version: 1.0
Content-Type: multipart/mixed; boundary="PEIAKu/WMn1b1Hv9"
Content-Disposition: inline
User-Agent: Mutt/1.5.6+20040722i
X-Miltered: at concorde with ID 418D60D3.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Miltered: at concorde with ID 418D60D2.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; tu-darmstadt:01 ocaml:01 algebra:01 functors:01 ocaml:01 functors:01 sml:01 refine:01 foo:01 sig:01 val:01 val:01 bool:01 sig:01 associative:01 
X-Attachments: name="algebra.ml" 
X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr
X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled 
	version=3.0.0
X-Spam-Level: 


--PEIAKu/WMn1b1Hv9
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline

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

--PEIAKu/WMn1b1Hv9
Content-Type: text/plain; charset=us-ascii
Content-Disposition: attachment; filename="algebra.ml"

(****************************************************************** 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)

--PEIAKu/WMn1b1Hv9--