From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.6 required=5.0 tests=AWL,NO_REAL_NAME,SPF_FAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 6AD9FBC4E for ; Wed, 6 Sep 2006 07:07:05 +0200 (CEST) Received: from selenite.metnet.navy.mil (selenite.metnet.navy.mil [192.16.167.32]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k865713Y006907 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Wed, 6 Sep 2006 07:07:04 +0200 Received: (qmail 11150 invoked by uid 107); 6 Sep 2006 05:06:58 -0000 Received: from vwmetnet.metnet.navy.mil (192.16.167.21) by selenite.metnet.navy.mil with SMTP; 6 Sep 2006 05:06:58 -0000 Received: from Adric.metnet.fnmoc.navy.mil ([10.100.105.102]) by vwmetnet.metnet.navy.mil (NAVGW 2.5.2.9) with SMTP id M2006090605195324948 ; Wed, 06 Sep 2006 05:19:53 GMT Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id 7D87BABF9; Tue, 5 Sep 2006 22:03:40 -0700 (PDT) To: Alain.Frisch@inria.fr Cc: caml-list@inria.fr Cc: ccshan@cs.rutgers.edu In-reply-to: <44FBD432.8030602@inria.fr> Subject: Re: [Caml-list] Eliminating array bounds check Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org From: oleg@pobox.com Message-Id: <20060906050340.7D87BABF9@Adric.metnet.fnmoc.navy.mil> Date: Tue, 5 Sep 2006 22:03:40 -0700 (PDT) X-j-chkmail-Score: MSGID : 44FE5775.001 on concorde : j-chkmail score : X : 0/20 1 X-Miltered: at concorde with ID 44FE5775.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; oleg:01 sig:01 sig:01 val:01 struct:01 struct:01 generative:01 sml:01 notation:01 val:01 sml:01 functor:01 formalize:01 work-around:01 modular:01 Hello! > module GenT(X:sig end) : sig type t val v : t end = > struct type t = int let v = 1 end > ;; > let module M1 = GenT(struct end) in > let module M2 = GenT(struct end) in > M1.v = M2.v > ;; That is very nice! Thank you. > (Ok, you must then trust the client not to apply GenT with > named structures.) I can hide this code in a trusted kernel: I merely need to be able to generate unique types. Frankly, what bsearch code really needed is local generative modules -- something like (in SML notation) val test = let local structure A = Kernel(val a = ...) open A in ... end in ... According to my reading of the Definition of the Standard ML, this is allowed. Alas, neither SML/NJ nor Poly/ML support this pattern. > Unfortunaly, you cannot make a polymorphic functor such as: > module GenT(A : sig val a : 'a array end) ... But the following close approximation works: module GenT(A : sig type e val a : e array end) : sig type barray type bindex type bindexL type bindexH val init_indexL : bindexL val init_indexH : bindexH val the_arr : barray val cmp : bindexL -> bindexH -> (bindex * bindex) option val get : barray -> bindex -> A.e end = struct type barray = A.e array type bindex = int type bindexL = int type bindexH = int let the_arr = A.a let init_indexL = 0 let init_indexH = Array.length A.a - 1 let cmp i j = if i <= j then Some (i,j) else None let get = Array.get end;; let test1 = let module X = GenT(struct type e = int let a = [|1;2|] end) in match X.cmp X.init_indexL X.init_indexH with Some (i,j) -> X.get X.the_arr j ;; let test2 = let a = [|1;2|] in let module X = GenT(struct type e = int let a = a end) in let module Y = GenT(struct type e = int let a = a end) in match X.cmp X.init_indexL X.init_indexH with Some (i,j) -> X.get Y.the_arr j ;; (* expected error: This expression has type Y.barray but is here used with type X.barray *) (* But this is OK *) let test3 = let module N = struct type e = int let a = [|1;2|] end in let module X = GenT(N) in let module Y = GenT(N) in match X.cmp X.init_indexL X.init_indexH with Some (i,j) -> X.get Y.the_arr j;; For formalization, the higher-rank types seem better (System F is easier to formalize than lambda-calculus plus the module system). For real work, the module system is obviously nicer. Thank you for the suggestions! > As a work-around, you can take only the length of the array as an argument: > module TrustedKernel(L: sig val len: int end) : sig Hmm, that means that modular arithmetics and implicit configurations described in http://www.eecs.harvard.edu/~ccshan/prepose/prepose.pdf http://www.eecs.harvard.edu/~ccshan/prepose/talk.ps.gz are immediately implementable in OCaml. That is very neat. module ModularNum (M : sig val modulus : int end) : sig type t val of_int : int -> t val to_int : t -> int val ( +$ ) : t -> t -> t val ( -$ ) : t -> t -> t val ( *$ ) : t -> t -> t val normalize : int -> t end = struct type t = int let normalize a = a mod M.modulus let of_int x = normalize x let to_int x = x let ( +$ ) x y = normalize (x + y) let ( -$ ) x y = normalize (x - y) let ( *$ ) x y = normalize (x * y) end;; (* (3*3 + 5*5) modulo 4 *) let test3 = let module XXX = struct module M = ModularNum(struct let modulus = 4 end) open M let a = of_int 3 and b = of_int 5 let v = a *$ a +$ b *$ b let result = to_int v end in XXX.result ;; (* The modulus is implicit, just as desired. *) (* It is clear that with a bit of camlp4 sugar, the boilerplate can be removed and we can write something like let test3 = with_modulus 4 (let a = of_int 3 and b = of_int 5 in a *$ a +$ b *$ b) *) (* testing non-interference: can't mix computations with different moduli The error message, This expression has type M.t but is here used with type M.t could be more helpful, though... *) (* A computation polymorphic over the modulus *) module Foo(M : sig val modulus : int end) = struct module M = ModularNum(M) open M let a = of_int 1000 let v = a *$ a *$ of_int 5 +$ of_int 2000 let result = to_int v end ;; (* Run the Foo computation over the series of moduli *) let test4 = List.map (fun m -> let module M = Foo(struct let modulus = m end) in M.result) [1;2;3;4;5;6;7;8;9] ;;