Re: [Caml-list] Eliminating array bounds check

[oleg@pobox.com]

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]
;;