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