From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 42011BB84 for ; Wed, 31 May 2006 21:36:56 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.6/8.13.6) with ESMTP id k4VJatqQ004212 for ; Wed, 31 May 2006 21:36:55 +0200 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA24515 for ; Wed, 31 May 2006 21:36:55 +0200 (MET DST) Received: from nf-out-0910.google.com (nf-out-0910.google.com [64.233.182.190]) by nez-perce.inria.fr (8.13.6/8.13.6) with ESMTP id k4VJaslO004204 for ; Wed, 31 May 2006 21:36:54 +0200 Received: by nf-out-0910.google.com with SMTP id p46so187896nfa for ; Wed, 31 May 2006 12:35:54 -0700 (PDT) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type; b=EiJ7JLAZasCGL9lyE1kuelRO6b9bpVSXH6K3qfpqTLqSg0fDCjJNgNv5lOT6gBeoN9kttIKJ58qnBqXZQ2tltOhbpXjvxF9+vk4aFEqgTsJDu7cWN7zuG0/5Qa7VTT93zm1Vfulta4B/0kvSBHMLpTCLJj4y49gcJwIVI0CZAtQ= Received: by 10.49.93.9 with SMTP id v9mr795810nfl; Wed, 31 May 2006 12:35:54 -0700 (PDT) Received: by 10.48.206.17 with HTTP; Wed, 31 May 2006 12:35:54 -0700 (PDT) Message-ID: <5de3f5ca0605311235h1f1db228t8e10f4ef65233e05@mail.gmail.com> Date: Wed, 31 May 2006 12:35:54 -0700 From: "L.G. Meredith" To: caml-list Subject: recursive modules? MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_30202_1624956.1149104154062" X-j-chkmail-Score: MSGID : 447DF056.000 on nez-perce : j-chkmail score : X : 0/20 1 X-Miltered: at nez-perce with ID 447DF057.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 447DF056.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; recursive:01 ocaml:01 compiler:01 abstractly:01 recursive:01 ocaml:01 compiler:01 sig:01 val:01 bool:01 functor:01 sig:01 mult:01 val:01 functor:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=2.0 required=5.0 tests=HTML_50_60,HTML_MESSAGE, RCVD_BY_IP,RCVD_IN_BL_SPAMCOP_NET autolearn=disabled version=3.0.3 ------=_Part_30202_1624956.1149104154062 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline 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 ------=_Part_30202_1624956.1149104154062 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline 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 ------=_Part_30202_1624956.1149104154062--