All,

i'm mostly a neophyte with OCaml. Please find below a simple example of a
code i would like to be able to write, but that the compiler will not eat. i
build a term language over a set of variables that are themselves abstractly
characterized in terms of some identifier type. i would like to write a
recursive module in which the abstract type of identifier is essentially the
type of the joinedcompositionfunctor applied to itself. One can show that
this results in a (mathematically) well-founded definition. Is there a
version of OCaml or an OCaml compiler option that will enable this kind of
recursive definition?

Best wishes,

--greg

(* What we demand of identifiers used by variables *)

module type IDENTIFIER =
  sig
    type idType
    val comparator : idType -> idType -> bool
  end

(* Two monoids 'joined at the hip', i.e. sharing an identity and set of
'variables' *)

module type JOINEDCOMPOSITIONFUNCTOR =
  functor (VarId : IDENTIFIER) ->
    sig
      type idType = VarId.idType
      type composite =
          Empty
        | Var of idType
        | Mult of composite list
        | Sum of composite list
      exception IllFormedMultiplication
      exception IllFormedSummation
      val zero : composite
      val multiply : composite list -> composite
      val sum : composite list -> composite
    end

module JoinedCompositionFunctor =
  functor  ( VarId : IDENTIFIER ) ->
    struct
      type idType = VarId.idType
      type composite =
      Empty
    | Var of idType
    | Mult of composite list
    | Sum of composite list

      exception IllFormedMultiplication
      exception IllFormedSummation

      let zero = Empty
      let rec multiply cList =
    (match cList with
         [] -> Empty
       | cListHd :: cListRest ->
           (let mRest = multiply cListRest in
          (match cListHd with
               Empty -> mRest
             | _ ->
             (match mRest with
                  Empty -> Mult( [ cListHd ] )
                | Mult( mList ) -> Mult( cListHd :: mList )
                | _ -> raise IllFormedMultiplication))))
      let rec sum cList =
    (match cList with
         [] -> Empty
       | cListHd :: cListRest ->
           (let mRest = sum cListRest in
          (match cListHd with
               Empty -> mRest
             | _ ->
             (match mRest with
                  Empty -> Sum( [ cListHd ] )
                | Sum( mList ) -> Sum( cListHd :: mList )
                | _ -> raise IllFormedSummation))))
    end

(* A structural equivalence, with an abstract characterization of
bag-equivalence *)

module Equivalence ( TFun : JOINEDCOMPOSITIONFUNCTOR ) ( VarId : IDENTIFIER
) =
  struct
    module JoinedComposition = TFun( VarId )
    let rec structural c1 c2 =
      match ( c1, c2 ) with
      ( JoinedComposition.Empty, JoinedComposition.Empty ) -> true
    | ( JoinedComposition.Mult( [] ), JoinedComposition.Empty ) -> true
    | ( JoinedComposition.Empty, JoinedComposition.Mult( [] ) ) -> true
    | ( JoinedComposition.Sum( [] ), JoinedComposition.Empty ) -> true
    | ( JoinedComposition.Empty, JoinedComposition.Sum( [] ) ) -> true
    | ( JoinedComposition.Mult( [] ), JoinedComposition.Sum( [] ) ) -> true
    | ( JoinedComposition.Sum( [] ), JoinedComposition.Mult( [] ) ) -> true
    | ( JoinedComposition.Mult( multiplicands1 ), JoinedComposition.Mult(
multiplicands2 ) ) ->
        (structuralBags multiplicands1 multiplicands2
JoinedComposition.multiply structural)
    | ( JoinedComposition.Sum( sumands1 ), JoinedComposition.Sum( sumands2 )
) ->
        (structuralBags sumands1 sumands2 JoinedComposition.sum structural)
    | ( JoinedComposition.Var( id1 ), JoinedComposition.Var( id2 ) ) ->
        ( VarId.comparator id1 id2 )
    | ( d1, d2 ) -> ( d1 = d2 )
    and structuralBags opands1 opands2 compositeCtor equiv =
      (match opands1 with
       [] ->
         (match opands2 with
          [] -> true
        | _ -> false)
     | opands1Hd :: opands1Rest ->
         let compositeCtor1Rest = (compositeCtor opands1Rest) in
         let filterfn =
           (fun opands2Candidate ->
          (equiv opands1Hd opands2Candidate)) in
           (match opands2 with
            [] -> false
          | opands2Hd :: opands2Rest ->
              match (List.partition filterfn opands2) with
              ( [], _ ) -> false
            | ( candidatesHd :: candidatesRest, failures ) ->
                let lc = ref true in
                let found = ref false in
                let c = ref candidatesHd in
                let cRest = ref candidatesRest in
                let fails = ref failures in
                  ((while !lc do
                  if (equiv compositeCtor1Rest (compositeCtor (!cRest @
!fails)))
                  then
                    (found := true;
                     lc := false)
                  else
                    (fails := !c :: !fails;
                     (match !cRest with
                      [] -> lc := false
                    | cRestHd :: cRestRest ->
                        (c := cRestHd;
                         cRest := cRestRest;)))
                done);
                   !found)))
  end

module VariableOfString =
struct

  type idType = string
      let comparator = (=)
end

module JoinedCompositionOfString = JoinedCompositionFunctor (
VariableOfString )

module JoinedEquivalenceOfString = Equivalence ( JoinedCompositionFunctor )
( VariableOfString )

(*

  The following definition can be proven to be mathematically
  well-founded, but is there a compiler that will do the right thing?

  module VariableOfRJoinedComposition =
  struct

  module RJoinedCompositionEquivalence =
  Equivalence ( JoinedCompositionFunctor )( VariableOfJoinedRComposition )

  type idType = RJoinedCompositionEquivalence.JoinedComposition.idType
  let comparator =
RJoinedCompositionEquivalence.JoinedComposition.comparator

  end

*)

-- 
L.G. Meredith
Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103

+1 206.650.3740