617S07 Homeworks for Cherif Andraos

Braun Trees (Continued)

Functions (Continued)

Now that we have a new release of Concoqtion, we can easily write the remove function which required a nested match statement. Also the unjustified warning described in the fold function for dependently-typed Braun trees is now removed.

Remove

Unsized

exception TreeException;;

let rec remove_last_bt bt =
   match bt with
   |Leaf -> raise TreeException
   |Parent(r,Leaf,Leaf) -> Leaf
   |Parent(r,bt1,bt2) -> Parent (r, bt2, (remove_last_bt bt1));;

Sized

let rec remove_last_dbt .|n:'(nat)| (dbt: ('(S n),'a) dbtree) : ('(n),'a) dbtree  = 
   match dbt in ('(n),'a) dbtree with 
   | DParent1 .|m:'(nat)| (r, dbt1, dbt2) -> 
        (match dbt2 in ('(n),'a) dbtree with 
         | DLeaf -> DLeaf
         | DParent1 .|l:'(nat)| (r2, dbt3, dbt4) -> DParent2 .|'(l*2)| (r,dbt1, remove_last_dbt .|'(l*2)| dbt2) 
         | DParent2 .|l:'(nat)| (r2, dbt3, dbt4) -> DParent2 .|'(S (l*2))| (r,dbt1, remove_last_dbt .|'(S (l*2))| dbt2) ) 
   | DParent2 .|m:'(nat)| (r, dbt1, dbt2) ->  DParent1 .|'(m)| (r, remove_last_dbt .|'(m)| dbt1, dbt2) 

Note that in the unsized version we have to raise an exception if the tree is already empty, this case can't happen in the sized version because the type of input tree is a tree of size successor of n which implies that it can't be empty. Even if we try to add a branch in the match that matches the input tree against an empty tree as shown below, here is what happens:

Definition:

let rec remove_last_dbt .|n:'(nat)| (dbt: ('(S n),'a) dbtree) : ('(n),'a) dbtree  = 
   match dbt in ('(n),'a) dbtree with 
   | DLeaf -> raise TreeException
   | DParent1 .|m:'(nat)| (r, dbt1, dbt2) -> 
        (match dbt2 in ('(n),'a) dbtree with 
         | DLeaf -> DLeaf
         | DParent1 .|l:'(nat)| (r2, dbt3, dbt4) -> DParent2 .|'(l*2)| (r,dbt1, remove_last_dbt .|'(l*2)| dbt2) 
         | DParent2 .|l:'(nat)| (r2, dbt3, dbt4) -> DParent2 .|'(S (l*2))| (r,dbt1, remove_last_dbt .|'(S (l*2))| dbt2) ) 
   | DParent2 .|m:'(nat)| (r, dbt1, dbt2) ->  DParent1 .|'(m)| (r, remove_last_dbt .|'(m)| dbt1, dbt2) 

Output:

File "bt.ml", line 112, characters 4-9:
Error while unifying the type of the argument of match  
  ('(S n), 'b) dbtree and pattern type ('(0), 'c) dbtree:
  This pattern matches values of type '(
  S _UNBOUND_REL_1) but is here used to match values of type '(0)

The type checker catches the fact that this is not possible and saves us from doing this unnecessary check.

Small Test

Code:

let t1 = insert_dbt1 .|'(0)| 0 DLeaf ;;
let t2 = insert_dbt1 .|'(1)| 10 t1;;
let t3 = insert_dbt1 .|'(2)| 20 t2;;
let t4 = insert_dbt1 .|'(3)| 30 t3;;
let t5 = insert_dbt1 .|'(4)| 40 t4;;
let t6 = insert_dbt1 .|'(5)| 50 t5;;
let t7 = insert_dbt1 .|'(6)| 60 t6;;
let t8 = insert_dbt1 .|'(7)| 70 t7;;
let t9 = insert_dbt1 .|'(8)| 80 t8;;

let add a b = a+b;;
let n = fold_dbt .|'(9)| 0 add t9;;

let t8_1 = remove_last_dbt .|'(8)| t9;;
let n_1 = fold_dbt .|'(8)| 0 add t8_1;;

Output:

val t1 : ('(1), int) dbtree = DParent1 (0, DLeaf, DLeaf)
val t2 : ('(2), int) dbtree =
  DParent2 (0, DParent1 (10, DLeaf, DLeaf), DLeaf)
val t3 : ('(3), int) dbtree =
  DParent1 (0, DParent1 (10, DLeaf, DLeaf), DParent1 (20, DLeaf, DLeaf))
 .
 .
 .
 .
val t9 : ('(9), int) dbtree =
  DParent1 (0,
   DParent2 (10, DParent2 (30, DParent1 (70, DLeaf, DLeaf), DLeaf),
    DParent1 (50, DLeaf, DLeaf)),
   DParent2 (20, DParent2 (40, DParent1 (80, DLeaf, DLeaf), DLeaf),
    DParent1 (60, DLeaf, DLeaf)))
val add : int -> int -> int = <fun>
val n : int = 360
val t8_1 : ('(8), int) dbtree =
  DParent2 (0,
   DParent2 (10, DParent2 (30, DParent1 (70, DLeaf, DLeaf), DLeaf),
    DParent1 (50, DLeaf, DLeaf)),
   DParent1 (20, DParent1 (40, DLeaf, DLeaf), DParent1 (60, DLeaf, DLeaf)))
val n_1 : int = 280

Project report (2007-04-09(M))

Title	FFT using indexed types	Group Member:	Cherif Salama & Angela Zhu	Date:	2007-04-09

Overview

Discrete Fourier Transformation (DFT) is widely used in digital signal processing applications, such as linear filtering, correlation analysis, and spectrum analysis. Its efficient computation is a topic that has been greatly studied in both academia and industry. The algorithm to perform DFT is called Fast Fourier Transform (FFT). Basically, computing the DFT can be seen as computing a sequence {X(k)} of N complex-valued numbers given another sequence of data {x(n)} of the same length N.

We are aiming at implement FFT algorithm, specifically the Cooley-Turkey's recursive algorithm (CT_FFT), using index types. The implementation in "A Methodology for Generating Verified Combinatorial Circuits" requires that the input to the algorithm must be a list whose length is power of 2. But this must be checked at run time.Our idea is that by encoding the length of FFT input and output, we can statically guarantee that the CT_FFT algorithm behaves well on its input.

---

++ Basic functions CT_FFT algorithm computes the DFT of a list of size N by first split the input list into two sub-lists, one has all odd index elements and another has all even index elements. It then computes the DFT of two sub-lists and uses the result to compute DFT the original list. If N = 2^n, this can be applied recursively and thus the basic functions in the implementation includes:

• Split function: take a list of size 2*n, output two list of size n

let rec  split l =
  match l with 
    [] -> ([], [])
  | x::y::xs -> let (a,b) = split xs in (x::a, y::b)

• Merge function: take two lists of size n, outputs a list of size 2*n.

let rec merge .|n:'(nat)| (dir: float) (l1: ('(n), 'a) slist) (l2: ('(n), 'a) slist): ('(n*2), 'a) slist =
   let len = fftlength .|'(n)| l1 in
    let rec mg .|m:'(nat)| (ll1: ('(m), 'a) slist) (ll2: ('(m), 'a) slist) j =
      match (ll1, ll2) in ('(n*2), 'a) slist with
      | Cons .|m1:'(nat)| (x, xs), Cons .|m2:'(nat)| (y, ys) ->
         let z1 = mult (w dir len j, y) in
         let zx = add (x, z1) in
         let zy = sub (x, z1) in
         let (a,b) = (mg .|'(m1)| xs ys (j+1)) in (Cons .|'(m1)| (zx, a), Cons .|'(m1)| (zy, b))
      | Nil, Nil -> Nil, Nil in 
   let (c, d) = mg .|'(n)| l1 l2 0 in 
      appends .|'(n), '(n)| c d

• FFT function: take a list of size 2^n, recursively call "split" and "merge", output a list of size 2^n.

let rec fft dir l =
  if (List.length l = 1) then 
    l
  else
    let (e,o) = split l in
    let y0 = fft dir e  in
    let y1 = fft dir o  in
    merge dir y0 y1

Lessons in implementation

Types of functions "split", "merge" and "FFT" (First Step):

We first tried to get the length of list recorded in the list and the three element functions:

type ('n  :'(nat), 'a) slist =
  | Nil : ('(0), 'a) slist
  | Cons of   l  et   'm:'(nat) in 'a * ('(m), 'a) slist: ('(S m), 'a) sl  ist

val split :
  (forall n:'(nat) .
      ('(n), 'a) slist -> ('(div2 n), 'a) slist * ('(div2 n), 'a) slist) =
  <forall>

val merge :
  (forall m:'(nat) .
      float ->
      ('(m), float * float) slist ->
      ('(m), float * float) slist -> ('(m + m), float * float) slist) =
  <forall>

val fft :
  (forall n:'(nat) .
      float -> ('(n), float * float) slist -> ('(n), float * float) slist) =
  <forall>

This is exactly what we want w.r.t. to the length of lists we manipulated. If the input to the "fft" function is exactly of length 2^n, we have no problem. However, if the input list has a length like "3, 6, 10,..." which are not a power of 2, the program will complain and report a mis-matching.

Types of functions "split", "merge" and "FFT" (Second Step):

Now the problem is clear: how to guarantee the index type .|n| is a power of 2? So that further in the split we know it will always get a list of even length.

To achieve this, in the index type of the input list, beside the length "n", we need a property or predicate to say that "n" is a power of 2. So we first define the property in Coq like follows:

Inductive isPower2: nat -> Prop :=
      | Power_0 : isPower2 1
      | Power_S : forall n, isPower2 n -> isPower2 (double n).

And now the fft function looks like this:

let rec fft .|n:'(nat), p:'(isPower2 n)| (dir: float) (l: ('(n), 'a) slist) : (('(n), 'a) slist) =
    if (fftlength .|'(n)| l = 1) then l
   else
      let (e,o) = split .|'(n)| l in
          let y0 = fft .|'(div2 n),'(isPower2 (div2 n))| dir e  in
          let y1 = fft .|'(div2 n),'(isPower2 (div2 n))| dir o  in
      aux .|'a, '(n)| (merge .|'(div2 n)| dir y0 y1);;

However, this will not work since we should not pass .|'(isPower2 (div2 n))|directly, as expected, we get the error:

Kind error while checking type application: 
    Type '(isPower2 (div2 n)) is expected to be  of kind '(isPower2 (div2 _UNBOUND_REL_2))     but got '(Prop)

To pass a correct property to say n/2 is also of power 2, we need the following Lemma:

   Lemma div_power2: forall n, gt n 1 -> isPower2 n -> isPower2 (div2 n).

In the next, we show the difficulties to proof and use this Lemma.

"gt n 1" and "gt n/2 1" ---- function "destr_gt"

One pre-condition of lemma "div_power2" is to guarantee that n>1, because n=1 is a power of 2, but 1/2=0 is not. Although in the fft function, if n=1 we return "l" directly, and the recursive call to fft only happens when n>1, but it is not easy to pass this information around.

Thanks to Emir for his help on this problem

*We define another natural number type where:

If n<=1, it is encoded as 'No0' and 'No1'; If n>1, it is encoded as 'Yes' and a proof of n>1:

type 'n:'(nat) gt_one =
  | No0: '(0) gt_one
  | No1: '(S 0) gt_one
  | Yes of let 'm:'(nat) 'p:'(gt m 1) in unit : '(m) gt_one

• We then define a "safelength" which instead of getting the length of the list, returns the lengh

of type '(n) gt_one.

let rec safelength .|n:'(nat)| (l: ('(n), 'a) slist) : '(n) gt_one =
  match l in '(n) gt_one with
  | Nil -> No0
  | Cons .|m1:'(nat)| (x, xs) ->
   (match xs in '(n) gt_one with
      | Nil -> No1
      | Cons .|m2:'(nat)| (y, ys) -> Yes .|'(n), '(ss_gt_1 m2)| ())

• Now we can pass the '(n) gt_one to fft function and it will get the proof of n>1 to prove n is a power of 2. But this is not trivial, we need an auxiliary function to behave like this:

Emir:" give me a return type r and a '(n) gt_one, and two functions (one for each case). If it is greater than the one, I'll invoke the first function and pass the prof to it. Otherwise, I'll invoke the other function and pass the proof to it. Both functions must return the result type 'r which you instantiate for every particular use. Note that this is just a function-based way of writing the case. BUT, it allows us to avoid nested matches etc.

......destr_gt which is an "elimination scheme" for the gt type which acts very much like the match statement, but can be used in place of the match statement. Its type is as follows: "

val destr_gt :
  (forall n:'(nat) , r:'(OCamlType) .
      '(n) gt_one ->
      (forall p:'(n > 1) . unit -> '(r)) ->
      (forall p:'(n <= 1) . unit -> '(r)) -> '(r))

and the "safefft" function now is implemented using the above auxiliary function:

let rec safefft .|n:'(nat),p:'(isPower2 n)| (dir:float) (l:('(n),'a) slist)  : ('(n),'a) slist =
   let case_less    .|p:'(n<=1)| () : ('(n),'a) slist = l in
   let case_greater .|q:'(n>1)| ()  : ('(n),'a) slist   = 
      let (e,o) = split .|'(n)| l in
      let y0 = safefft .|'(div2 n),'(div_power2 n q p)| dir e in
      let y1 = safefft .|'(div2 n),'(div_power2 n q p)| dir o in
      let rr = aux .|'a, '(n)| (merge .|'(div2 n)| dir y0 y1) in rr in
   let condition = destr_gt .|'(n), ('(n),float * float) slist| (safelength .|'(n)| l) in
      condition case_greater case_less

Proofs of Lemma in Coq

We use several Lemma in coq environment to guarantee the desired properties on the lenth of fft lists. Basically, we need the following definitions and lemmas:

Inductive isPower2: nat -> Prop :=
      | Power_0 : isPower2 1
      | Power_S : forall n, isPower2 n -> isPower2 (double n).

Lemma ss_gt_1: forall n, gt (S (S n)) 1.
Lemma div2_double : forall n:nat, div2 (2*n) = n.
Lemma div_power2: forall n, gt n 1 -> isPower2 n -> isPower2 (div2 n).
Lemma div2_plus_div2 : forall n:nat, gt n 1 -> isPower2 n -> div2 n + div2 n = n.
Lemma list_cast : forall e, forall m n:nat, (m=n) -> (OCaml_slist m e) = (OCaml_slist n e).

During this project, we learned how to write proofs for these lemma. Detailed proof please refer to the appendix.

A view on "safe cast"

Cast function is used in our implementation to convert the type of "merge" output, which is '(n/2 + n/2) slist, to the type '(n) slist, for "fft" function. Notice that this is only true when n is even. This is guaranteed if the input to "fft" function is a list of length 2^n. We achieve this by passing the proof around in the index type.

However cast function withOUT "Obj.magic" is a little different from what we've seen in the type checker. In "type_checker.ml" we do the cast by first construction a type called "eq_typ" which can help us to get an indexed type to another indexed type (computational cast). However, this is not applicable here since we only have original coq type.

Thanks to Emir for his help on this problem

Following is what worded for our implementation w.r.t. "cast" issue:

external castFun:'a -> 'b = "%identity";;

let cast .|a,b,p:'(a=b)| (x:'(a)) : '(b) = castFun x;;

let aux .|a, m:'(nat), p:'(gt m 1), q:'(isPower2 m)| (x: ('((div2 (m))+(div2 (m))), 'a) slist) =
    cast .|'(OCaml_slist ((div2 (m))+(div2 (m))) a),
           '(OCaml_slist (m) a),
           '(list_cast a ((div2 (m))+(div2 (m))) (m) (div2_plus_div2 m p q))| x

Concoqtion bug reporting

Before trying to proof the fft function will always get a list of length 2^n, we tried something on "split" function first to guarantee it will always get a input list of even length.

We failed because concoqtion's problem on nested matching, and reported in our email. Emir affirmed that this is a bug and the problem is specified as follows:

let rec split .|n:'(nat), p:'(even n)| (l: ('(n), 'a) slist): (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) =
   match l in (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) with
   | Nil -> Nil, Nil
   | Cons .|m1:'(nat)| (x, xt) ->   
      match xt in (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) with
      | Cons .|m2: '(nat)| (y, xs) ->       
         let (xxs,yys) = (split .|'(m2),'(even_minus_two m2 p)| xs) in Cons .|'(div2 m2)| (x, xxs), Cons .|'(div2 m2)| (y, yys) ;;
*************************************************************************
File "fft1.ml", line 113, characters 35-57:
Coq error in escaped type:
At location 19-20:
Error:
In environment
m2 : nat
m1 := S m2 : nat
n := S _UNBOUND_REL_0 : nat
p : even n
The term "p" has type "even n" while it is expected to have type
"even (S (S m2))"
*************************************************************************

Clearly, n = S m1 and m1 = S m2, but the pattern matching lost this information in the nested match statement.

Test and evaluation

The test cases we used is at the end of the attached source code in the "Appendix".

Appendix: Full implementation in concoqtion

(***********************************************
*     Angela Yun Zhu                           *
*     Cherif Salama                            *
*     RAP, CS Dept, Rice Univ.                 *
*     2007, April 8th                          *
*     Seminar 617 Homework                     *
*     Concoqtion implementation of FFT         *
************************************************)

(* Pi value *)
let pi = 4.0 *. atan(1.0)

(* W = exp(-2PI dir/N)^j. Note that dir=1.0 for the forward transform *)
let w dir n j = 
  let theta = dir *. ((float_of_int (-2 * j)) *. pi) /. (float_of_int n) in
  ((cos theta), (sin theta)) 

(* Complex number addition. Complex numbers are represented as float tuples *)
let add ((r1,i1), (r2, i2)) = ((r1 +. r2), (i1 +. i2))

(* Complex number addition. Complex numbers are represented as float tuples *)
let sub ((r1,i1), (r2, i2)) = ((r1 -. r2), (i1 -. i2))

(* Complex number addition. Complex numbers are represented as float tuples *)
let mult ((r1, i1), (r2, i2)) =
  let rp = (r1 *. r2) -. (i1 *. i2) in
  let ip = (r1 *. i2) +. (r2 *. i1) in
  (rp, ip)
  
(* Sized lists data type as defined before. Use to guarantee
   that the list returned from the fft function is of
   the correct size which is equal to the returned size *)
type ('n:'(nat), 'a) slist =
  | Nil : ('(0), 'a) slist
  | Cons of let 'm:'(nat) in 'a * ('(m), 'a) slist: ('(S m), 'a) slist
;;

(* Some coq definitions and lemmas *)
coq
   (* Required Libraries *)
   Require Import Div2.
   Require Import Arith.Gt.
   
   (* Inductive definition of isPower2, if n=1 than it is a
      power of 2 and if n=double n0 where n0 is a power of2 
      than n also is a power of 2 *)
   Inductive isPower2: nat -> Prop :=
      | Power_0 : isPower2 1
      | Power_S : forall n, isPower2 n -> isPower2 (double n).
   
   (* A successor of a successor is always greater than 1.
      Used for the safe length function *)
   Lemma ss_gt_1: forall n, gt (S (S n)) 1.
      auto with arith.
      Qed.
   
   (* Half double n equals n. Used in the proof of the following
      2 lemmas *)
   Lemma div2_double : forall n:nat, div2 (2*n) = n.
      induction n.
      simpl; auto.
      simpl.
      replace (n + S (n + 0)) with (S (2 * n)).
      rewrite IHn.
      auto.
      simpl.
      auto with arith.
      Qed.
   
   (* If n > 1 and n is a power of 2 than dividing n by 2 gives 
      a power of 2 also. Used in safefft to prove that after spliting 
      a sized list whose length is a power of 2 we get 2 sized lists
      whose lengths are also powers of 2 *)
   Lemma div_power2: forall n, gt n 1 -> isPower2 n -> isPower2 (div2 n).
      intros.
      inversion H0.
      subst.
      absurd (1 > 1).
      apply gt_irrefl.
      auto.
      replace (div2 (double n0)) with n0.
      auto.
      replace (double n0) with (2 * n0).
      rewrite div2_double.
      auto.
      replace (double n0) with (n0 + n0).
      simpl.
      auto.
      auto.
      Qed.

  (* If n > 1 and n is a power of 2 than dividing n by 2 and adding the
    result to itself gives n again. Used in safefft to prove that after 
    and merging we get a list of the same size as of the original list *)
  Lemma div2_plus_div2 : forall n:nat, gt n 1 -> isPower2 n -> div2 n + div2 n = n.
      intros.
      inversion H0.
      subst.
      absurd (1 > 1).
      apply gt_irrefl.
      auto.
      replace (div2 (double n0)) with n0.
      auto.
      replace (double n0) with (2 * n0).
      rewrite div2_double.
      auto.
      replace (double n0) with (n0 + n0).
      simpl.
      auto.
      auto.
      Qed.

 (* if m=n than a sized list of size m has a size equal to a sized list
    of size n. Used in aux function to help achieving a safe cast *)
 Lemma list_cast : forall e, forall m n:nat, (m=n) ->
           (OCaml_slist m e) = (OCaml_slist n e).
      intro; intro; intro.
      intro H.
      rewrite -> H.
      trivial.
        Qed.
end;;

(* external castFun : 'a -> 'b = "%identity" *)
external castFun:'a -> 'b = "%identity";;

(* val cast : (forall a , b , p:'(a = b) . '(a) -> '(b)) = <forall> *)
let cast .|a,b,p:'(a=b)| (x:'(a)) : '(b) = castFun x;;

let aux .|a, m:'(nat), p:'(gt m 1), q:'(isPower2 m)| (x: ('((div2 (m))+(div2 (m))), 'a) slist) =
    cast .|'(OCaml_slist ((div2 (m))+(div2 (m))) a),
           '(OCaml_slist (m) a),
           '(list_cast a ((div2 (m))+(div2 (m))) (m) (div2_plus_div2 m p q))| x

(* splits a lists into 2 lists of equal size, one containing the elements
   originally in odd positions and one containing the elements originally 
   in even positions *)
let rec split .|n:'(nat)| (l: ('(n), 'a) slist): (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist)=
   match l in (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) with
   | Nil -> Nil, Nil
   | Cons .|m1:'(nat)| (x, xs) -> 
      (match xs in (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) with 
       | Cons .|m2:'(nat)| (y, ys) -> 
         let (xxs, yys) = split .|'(m2)| ys in    
         Cons .|'(div2 m2)| (x, xxs), Cons .|'(div2 m2)| (y, yys))

(* The following 4 function are needed to implement the original merge function 
   as appeared in the paper *)

(* Function that takes a sized list and returns its length as an OCaml integer.
   Used in merge function *)
let rec fftlength .|n:'(nat)| (l: ('(n), 'a) slist) : int =
  match l in int with
  | Nil -> 0
  | Cons .|m1:'(nat)| (x, xs) -> 1 + fftlength .|'(m1)| xs;;

(* Function that takes 2 sized lists and append them. Used in merge function *)
let rec appends .|m:'(nat), n:'(nat)| (l1 : ('(m), 'a) slist) (l2 : ('(n), 'a) slist): ('(m+n), 'a) slist =
   (match l1 as ('i:'(nat),'t) slist in ('(i+n),'t) slist with
   | Nil -> l2
   | Cons .| m1:'(nat)| (x,xs) -> Cons .| '(m1+n) | (x, appends .|'(m1),'(n)| xs l2));;

(* Helper function for merge *)
let rec mg .|n:'(nat)| (l1: ('(n), 'a) slist) (l2: ('(n), 'a) slist) (dir: float) (n: int) (j: int): (('(n), 'a) slist) * (('(n), 'a) slist) =
    match (l1, l2) in (('(n), 'a) slist) * (('(n), 'a) slist) with
    | (Cons .|m1:'(nat)| (x, xs), Cons .|m2:'(nat)| (y, ys)) ->
   let z1 = mult (w dir n j, y) in
   let zx = add (x, z1) in
   let zy = sub (x, z1) in
   let (a,b) = (mg .|'(m1)| xs ys dir n (j+1)) in (Cons .|'(m1)| (zx,a), Cons .|'(m1)| (zy,b))
    | (Nil, Nil) -> (Nil, Nil);;

(* Merge function. Used in safefft *)
let merge .|m:'(nat)| (dir: float) (l1: ('(m), 'a) slist) (l2: ('(m), 'a) slist): (('(m+m), 'a) slist) =
  match l1 in (('(m+m), 'a) slist) with
  | Cons .|m1:'(nat)| (x, xs) -> 
      let n = 2 * fftlength .|'(S m1)| l1 in
      let (a,b) = mg .|'(S m1)| l1 l2 dir n 0 in appends .|'(S m1),'(S m1)| a b;;

(* The following type and 3 functions are needed to implement the original fft function
   as appeared in the paper *)
   
(* This type is required to be able to easily differentiate between numbers that are 
   greater than 1 and those that are not while storing their values. This can be 
   thought of a way of encoding natural numbers while keeping the fact of either
   they are greater than 1 or not explicit in the encoding itself *)   
type 'n:'(nat) gt_one =
  | No0: '(0) gt_one
  | No1: '(S 0) gt_one
  | Yes of let 'm:'(nat) 'p:'(gt m 1) in unit : '(m) gt_one
;;

(* This function is passed a sized list and returns a gt_one encoded number representing
   its length *)
let rec safelength .|n:'(nat)| (l: ('(n), 'a) slist) : '(n) gt_one =
  match l in '(n) gt_one with
  | Nil -> No0
  | Cons .|m1:'(nat)| (x, xs) ->
   (match xs in '(n) gt_one with
      | Nil -> No1
      | Cons .|m2:'(nat)| (y, ys) -> Yes .|'(n), '(ss_gt_1 m2)| ())

(* This function is passed a gt_one encoded number and returns a function that work as follows:
   If given a function that returns something of type r if this number is greater than 1
   and another function that returns something of type r if this number is not greater than r
   it returns something of type r *)
let rec destr_gt .|n:'(nat),r:'(OCamlType)| (cond:'(n) gt_one) : (forall p:'(n>1). unit -> '(r)) -> (forall p:'(n<=1). unit -> '(r)) ->  '(r) = 
   match cond as ('q:'(nat)) gt_one in (forall p:'(q>1). unit -> '(r)) -> (forall p:'(q<=1). unit -> '(r)) -> '(r) with 
   | Yes .|m:'(nat),p:'(m>1)| () -> fun  f g -> f .|'(p)| ()
   | No0 -> fun f g -> g .|'(le_S 0 0 (le_n 0))| ()
   | No1 -> fun f g -> g .| '(le_n 1)| ()  


(* Safe FFT function that takes a sized list of size n which is guaranteed to be a power of 2 
   and returns the FFT as a list of the same size *)
let rec safefft .|n:'(nat),p:'(isPower2 n)| (dir:float) (l:('(n),'a) slist)  : ('(n),'a) slist =
   let case_less    .|q1:'(n<=1)| () : ('(n),'a) slist = l in
   let case_greater .|q2:'(n>1)| ()  : ('(n),'a) slist   = 
      let (e,o) = split .|'(n)| l in
      let y0 = safefft .|'(div2 n),'(div_power2 n q2 p)| dir e in
      let y1 = safefft .|'(div2 n),'(div_power2 n q2 p)| dir o in
      let rr = aux .|'a, '(n), '(q2), '(p)| (merge .|'(div2 n)| dir y0 y1) in rr in
   let condition = destr_gt .|'(n), ('(n),float * float) slist| (safelength .|'(n)| l) in
      condition case_greater case_less
;;

(* The following function is the standard fft implementation from the paper *)
let pi0 = 4.0 *. atan(1.0);;

let w0 dir n j = 
  let theta = dir *. ((float_of_int (-2 * j)) *. pi0) /. (float_of_int n) in
  ((cos theta), (sin theta)) ;;

let add0 ((r1,i1), (r2, i2)) = ((r1 +. r2), (i1 +. i2));;

let sub0 ((r1,i1), (r2, i2)) = ((r1 -. r2), (i1 -. i2));;

let mult0 ((r1, i1), (r2, i2)) =
  let rp = (r1 *. r2) -. (i1 *. i2) in
  let ip = (r1 *. i2) +. (r2 *. i1) in
  (rp, ip);;

let rec split0 l =
  match l with 
  [] -> ([], [])
  | x::y::xs ->
  let (a,b) = split0 xs in (x::a, y::b);;

let merge0 dir l1 l2 =
  let n = 2 * List.length l1 in
  let rec mg0 l1 l2 j =
    match (l1, l2) with
      (x::xs, y::ys) ->
        let z1 = mult0 (w0 dir n j, y) in
        let zx = add0 (x, z1) in
        let zy = sub0 (x, z1) in
        let (a,b) = (mg0 xs ys (j+1)) in (zx::a, zy::b)
    | _ -> ([], []) in
  let (a,b) = mg0 l1 l2 0 in (a @ b);;

let rec fft0 dir l =
  if (List.length l = 1) then 
    l
  else
    let (e,o) = split0 l in
    let y0 = fft0 dir e  in
    let y1 = fft0 dir o  in
    merge0 dir y0 y1;;


(* Tests *)

(* Regular fft *)
let l10 = [(1.1,2.2);(3.3,4.4);(5.5,6.6);(7.7,8.8)];;
fft0 1.0 l10;;

(* Safe fft *)
let l1 = (Cons .|'(3)|((1.1,2.2),Cons .|'(2)|((3.3,4.4),Cons .|'(1)|((5.5,6.6),Cons .|'(0)|((7.7,8.8),Nil)))));;
safefft .|'(4),'(Power_S 2 (Power_S 1 Power_0))| 1.0 l1;;

(* Performance comparison *)
Trxtime.init_times ();;
Trxtime.timenew "Regular fft"  (fun _ -> fft0 1.0 l10);;
Trxtime.timenew "Safe fft"   (fun _ -> (safefft .|'(4),'(Power_S 2 (Power_S 1 Power_0))| 1.0 l1));;
Trxtime.print_times ();;

(* Results running the above code using concoqtion interpreter *)
(*
__ Regular fft _____________ 65536x avg= 1.793996E-02 msec
__ Safe fft ________________ 65536x avg= 1.936152E-02 msec
*)

(* Results running the above code using concoqtion compiler *)
(*
__ Regular fft _____________ 65536x avg= 2.199154E-02 msec
__ Safe fft ________________ 65536x avg= 2.548305E-02 msec
*)
(* In both cases Regular fft is about 10% faster than Safe fft *)

Project proposal: FFT using indexed types

Project Overview

• This is a two weeks project we will work on during Prof. Taha's absence. (3/23-4/9)
• Group member: Angela & Cherif
• Presentation dates: 3/30 (Cherif) & 4/2 (Angela)

Motivation

Discrete Fourier Transformation (DFT) is widely used in digital signal processing applications, such as linear filtering, correlation analysis, and spectrum analysis. Its efficient computation is a topic that has been greatly studied in both academia and industry. The algorithm to perform DFT is called Fast Fourier Transform (FFT). Basically, computing the DFT can be seen as computing a sequence {X(k)} of N complex-valued numbers given another sequence of data {x(n)} of the same length N.

We propose an index-typed implementation of FFT based on Cooley-Turkey's recursive algorithm. Using that index-type, we get the following benefits:

• Size of the input and output lists is guaranteed to be equal and this checking is done at the type level statically, therefore shouldn't increase the run time.
• Pattern matching is safer since we are now sure that input lists are of equal sizes.

We also want to check the following:

• How easy would it be to write an efficient FFT implementation using Concoqtion and explore more of Concoqtion features needed to achieve this.
• Performance of the Concoqtion implementation of FFT.

Project phases

• Gather information about FFT and its implementations
• Look at Prof. Taha's papers (A Methodology for Generating Verified Combinatorial Circuits, Relating FFTW and Split-Radix) and see how it's implemented there.
• Implement Cooley-Turkey's FFT algorithm with input list of size 2^n.
• Test it on different lists.
• Test it's performance and compare it to the non-indexed implementation.
• Analyze results and report them in class with discussion on difficulties we encountered.

Other project ideas

• Compile-time dimension checking for matrix operations.
• Implement functions simulating the functionality of certain hardware circuit families using indexed types. For example we could think of N-bit adders or N-bit multipliers where N is the type index.

Braun trees

Types

Regular Braun Tree Type

Definition:

type 'a btree =
    |Leaf
    |Parent of 'a * 'a btree * 'a btree;;

Dependently-Typed Braun Tree Type

Old Definition: This definition causes matching problems in the insert function and needs a lemma to be added to prove that Type S (S (m + m)) is equal to (S m + S m). An alternative way to avoid this is using Dan's definition using multiplication.

type ('n:'(nat),'a) dbtree =
    |DLeaf :('(0),'a) dbtree
    |DParent1 of let 'n:'(nat) in 'a * ('(n),'a) dbtree *('(n),'a) dbtree : ('(S (n+n)),'a) dbtree
    |DParent2 of let 'n:'(nat) in 'a * ('(S n),'a) dbtree *('(n),'a) dbtree: ('(S (S (n+n))),'a) dbtree;;

New Definition:

This definition is based on Dan's definition:

type ('n:'(nat),'a) dbtree =
    |DLeaf :('(0),'a) dbtree
    |DParent1 of let 'n:'(nat) in 'a * ('(n),'a) dbtree *('(n),'a) dbtree : ('(S (n*2)),'a) dbtree
    |DParent2 of let 'n:'(nat) in 'a * ('(S n),'a) dbtree *('(n),'a) dbtree: ('(S (S (n*2))),'a) dbtree;;

Functions

Map Function

Unsized

let rec map_bt f bt =
    match bt with
    |Leaf -> Leaf
    |Parent(x,bt1,bt2) -> Parent(f x, map_bt f bt1, map_bt f bt2);;

Sized

let rec map_dbt .|n:'(nat)| (f:'a ->'b) (dbt:('(n),'a) dbtree): ('(n),'b) dbtree =
    match dbt in ('(n),'t) dbtree  with
    |DLeaf -> DLeaf
    |DParent1 .|m:'(nat)| (x,dbt1,dbt2) -> DParent1 .|'(m)| ((f x), (map_dbt .|'(m)| f dbt1), (map_dbt .|'(m)| f dbt2))
    |DParent2 .|m:'(nat)| (x,dbt1,dbt2) -> DParent2 .|'(m)| ((f x), (map_dbt .|'(S m)| f dbt1), (map_dbt .|'(m)| f dbt2));;

Get_size and Diff Functions

Unsized

This version runs in O(n)

let rec getSize_bt1 bt =
    match bt with
    |Leaf -> 0
    |Parent(x,bt1,bt2) -> (getSize_bt1 bt1) + (getSize_bt1 bt2) + 1;; 

Another Definition for Regular Braun Trees:

This version makes use of the diff function and runs in O(log^2 n)

let rec getSize_bt2 bt =
    let rec diff bt m = 
        (match bt with
        | Leaf -> 0
        | Parent(x,bt1,bt2) -> 
        if m = 0 then 1 
             else
                (if m mod 2 = 1 then 
                     diff bt1 (m-1)/2 
                 else
                     diff bt2 (m-2)/2))
    in match bt with
    |Leaf -> 0
    |Parent(x,bt1,bt2) -> let n = (getSize_bt2 bt2) in 1+2*n+(diff bt1 n);; 

Sized

Runs in O(log n) without even needing the diff function

let rec getSize_dbt .|n:'(nat)| (dbt:('(n),'a) dbtree): int =
    match dbt in int with
    |DLeaf -> 0
    |DParent1 .|m:'(nat)| (x,dbt1,dbt2) -> 1 + (2 * (getSize_dbt .|'(m)| dbt2))
    |DParent2 .|m:'(nat)| (x,dbt1,dbt2) -> 2 + (2 * (getSize_dbt .|'(m)| dbt2));;

Insert Function

Unsized

let rec insert_bt1 x bt =
    match bt with
    |Leaf -> Parent(x,Leaf,Leaf)
    |Parent(r,bt1,bt2) ->
        if (getSize_bt2 bt1) > (getSize_bt2 bt2) then
            Parent(r,bt1,(insert_bt1 x bt2))
        else
            Parent(r,(insert_bt1 x bt1),bt2);;

Another Definition for Regular Braun Trees:

This definition is based on the standard cons for braun trees. It is easier to implement since it always insert the new element as the root and adds the element that was initially the root to the right tree and then swaps the left and right branches.

let rec insert_bt2 x bt =
    match bt with
    |Leaf -> Parent(x,Leaf,Leaf)
    |Parent(r,bt1,bt2) -> Parent(x,(insert_bt2 r bt2),bt1);;

Sized

let rec insert_dbt1 .|n:'(nat)| (x:'a) (dbt:('(n),'a) dbtree): ('(S n),'a) dbtree =
    match dbt in ('(S n),'a) dbtree  with
    |DLeaf -> DParent1 .|'(0)| (x,DLeaf,DLeaf)
    |DParent1 .|m:'(nat)| (r,dbt1,dbt2) -> DParent2 .|'(m)| (r, (insert_dbt1 .|'(m)| x dbt1), dbt2)
    |DParent2 .|m:'(nat)| (r,dbt1,dbt2) -> DParent1 .|'(S m)| (r, dbt1, (insert_dbt1 .|'(m)| x dbt2));;

Another Definition for Dependtly-typed Braun Trees:

Based on swaping the left and right branches

let rec insert_dbt2 .|n:'(nat)| (x:'a) (dbt:('(n),'a) dbtree): ('(S n),'a) dbtree =
    match dbt in ('(S n),'a) dbtree  with
    |DLeaf -> DParent1 .|'(0)| (x,DLeaf,DLeaf)
    |DParent1 .|m:'(nat)| (r,dbt1,dbt2) -> DParent2 .|'(m)| (x, (insert_dbt2 .|'(m)| r dbt2), dbt1)
    |DParent2 .|m:'(nat)| (r,dbt1,dbt2) -> DParent1 .|'(S m)| (x, (insert_dbt2 .|'(m)| r dbt2), dbt1);;

Note both versions for dependly typed braun trees work correctly now after changing the dependtly-typed braun tree definition to use multiplication, before that change both versions returned the following error:

Output:

   
File "bt.ml", line 42, characters 41-98:
Type [(m : nat) (n := S (S (m + m)) : nat)] |-
  ('(S n), 'e1) dbtree was expected but
  ('(S (S m + S m)), 'e1) dbtree was inferred for the branch expression.

Fold Function

Unsized

let rec fold_bt i step bt =
    match bt with
    |Leaf -> i
    |Parent(r,bt1,bt2) -> step r (fold_bt (fold_bt i step bt2) step bt1);;

Sized

let rec fold_dbt .|n:'(nat)| (i:'a) (step:'b ->'a -> 'a) (dbt:('(n),'b) dbtree): 'a =
    match dbt in 'a  with
    |DLeaf -> i
    |DParent1 .|m:'(nat)| (r,dbt1,dbt2) -> step r (fold_dbt .|'(m)| (fold_dbt .|'(m)| i step dbt2) step dbt1)
    |DParent2 .|m:'(nat)| (r,dbt1,dbt2) -> step r (fold_dbt .|'(S m)| (fold_dbt .|'(m)| i step dbt2) step dbt1);;

Note this function compiles and works correctly but it gives the following unjustified warning:

Output:

File "bt.ml", line 81, characters 16-18:
Warning: Unspecified return type for the extended match expression.
val fold_dbt :
  (forall n:'(nat) . 'a -> ('b -> 'a -> 'a) -> ('(n), 'b) dbtree -> 'a) =
  <forall>

Lists

Walid: This section looks quite good! Here are a few suggestions that would improve it:

• Write unsized definitions before each sized version.
• Add text describing own experience writing these functions (hard, easy, interesting, and way).
• Put timings in appropriate table, and explain what conclusions can be drawn from these tests.

Types

Sized List Type

This was straight forward but using (m+1) instead of (S m) makes things much more complex and cause many functions defined on sized lists to fail. Also using (1+m) which is equivalent to (S m) as far as I understand leads to a much more complex output involving fix application.

Definition:

type ('n:'(nat),'a) slist =
| Nil : ('(0),'a) slist
| Cons of let 'm:'(nat) in 'a * ('(m),'a) slist : ('(S m),'a) slist;;

Output:

type ('a:'(nat), 'b:'(OCamlType)) slist =
    Nil:('(0), 'b) slist
  | Cons of  let 'm:'(nat)  in  'b * ('(m), 'b) slist : ('(S m), 'b) slist

Option Type

This type is used to represent an optional return value of a certain type.

Definition:

type 'a option = 
|None
|Some of 'a;;

Output:

type 'a:'(OCamlType) option = None:'a option | Some of   'a : 'a option

Existsize Type

This type is used to represent the existential quantifier

Definition:

type 'a existsize = E of let 'n:'(nat) in ('(n),'a) slist;;

Output:

type 'a:'(OCamlType) existsize =
    E of  let 'n:'(nat)  in  ('(n), 'a) slist : 'a existsize

Functions

Map Function

Both versions for Unsized and Sized lists look very similar and were easy to write.

Unsized

let rec mapn f l = 
    match l with
    | []->[]
    | h::t -> (f h)::(mapn f t);;

Output:

val mapn : ('a -> 'b) -> 'a list -> 'b list = <fun>

Sized

let rec maps .|m:'(nat)| (f:'a ->'b) (la:('(m),'a) slist): ('(m),'b) slist =
    (match la in ('(m),'t) slist with
     |Nil -> Nil
     |Cons .|n:'(nat)| (lah,lat) -> Cons .|'(n)| ((f lah), (maps .|'(n)| f lat)));; 

Output:

val maps :
  (forall m:'(nat) . ('a -> 'b) -> ('(m), 'a) slist -> ('(m), 'b) slist) =
  <forall>

Zip Function

The sized version has the nice property that we are sure from the typing information that both lists are equal. Therefore we only needed two branches in the match statement, while in the unsized version we need three at least. Also in the unsized version, there are different ways to handle the case where both lists are not equal. The one I picked is just to trim the resulting list to be of length equal to the minimum of input lists lengths ignoring the remaining elements of the longer list. Other approaches would have been to raise an error or to try to append the shorter list with dummy values. Note that all these problems are not encountered in case of the sized version because of the static guarantees on the list sizes.

Unsized

let rec zipn l1 l2 = 
    match (l1,l2) with
    |(_,[])->[]
    |([],_)->[]
    |(h1::t1,h2::t2) -> (h1,h2)::(zipn t1 t2);;

Output:

val zipn : 'a list -> 'b list -> ('a * 'b) list = <fun>

Sized

let rec zips .|m:'(nat)| (la:('(m),'a) slist) (lb:('(m),'b) slist): ('(m),('a*'b)) slist=
    (match (la,lb) in ('(m),('t1*'t2)) slist with
    |(Nil,Nil) -> Nil
    |(Cons .|n:'(nat)| (lah,lat),Cons .|n:'(nat)| (lbh,lbt)) -> Cons .|'(n)| ((lah,lbh),(zips .|'(n)| lat lbt)));; 

Output:

val zips :
  (forall m:'(nat) .
      ('(m), 'a) slist -> ('(m), 'b) slist -> ('(m), 'a * 'b) slist) =
  <forall>

Add_twice Function

This is a very simple function that takes an element and a list and inserts that element twice in the head of the list. Both the sized and unsized versions are similar.

Unsized

let add_twicen x xs =
  x::(x::xs);;

Output:

val add_twicen : 'a -> 'a list -> 'a list = <fun>

Sized

let add_twices .|m:'(nat)| x xs =
  Cons .|'(S m)| (x, Cons .|'(m)| (x, xs));;

Output:

val add_twices :
  (forall m:'(nat) . 'a -> ('(m), 'a) slist -> ('(S (S m)), 'a) slist) =
  <forall>

Append Function

The standard append function, implemented in a similar fashion for both sized and unsized lists.

Unsized

let rec appendn l1 l2 =
    match l1 with
    | []-> l2
    | h::t -> h::(appendn t l2);;

Output:

val appendn : 'a list -> 'a list -> 'a list = <fun>

Sized

let rec appends .|m:'(nat), n:'(nat)| (l1 : ('(m), 'a) slist) (l2 : ('(n), 'a) slist): ('(m+n), 'a) slist =
    (match l1 as ('i:'(nat),'t) slist in ('(i+n),'t) slist with
    | Nil -> l2
    | Cons .| m1:'(nat)| (x,xs) -> Cons .| '(m1+n) | (x, appends .|'(m1),'(n)| xs l2));;

Output:

val appends :
  (forall m:'(nat) , n:'(nat) .
      ('(m), 'a) slist -> ('(n), 'a) slist -> ('(m + n), 'a) slist) =
  <forall>

Generate Function

To be able to test functions with long lists, I wrote this generate function that generates a list of integers given a start value, and end value and a step. The sized version was a little more complex and required the use of existential type. It's use in a recursive call required unwrapping the E constructer and wrapping again.

Unsized

let rec generaten st en stp =
    if (en<st) then [] else
        st::(generaten (st+stp) en stp);;

Output:

val generaten : int -> int -> int -> int list = <fun>

Sized

let rec generates (st:int) (en:int) (stp:int): 'a existsize =
    if (en<st) then (E .|'(0)| Nil) else
   (match (generates (st+stp) en stp) in 'c existsize with
       | E .|n:'(nat)| sl -> E .|'(1+n)| (Cons .|'(n)| (st,sl)) ) ;;

Output:

val generates : int -> int -> int -> int existsize = <fun>

Size_It Function

The size_it function that takes a list and returns an existential type encapsulating a sized list. So we could think of it as a function that converts an unsized list into a sized one.

Definition:

let rec size_it (la: 'a list): 'a existsize =
    (match la in 'b existsize with
    |[] -> E .|'(0)| Nil
    |h::t -> (match (size_it t) in 'c existsize with 
        | E .|n:'(nat)| sl -> E .|'(1+n)| (Cons .|'(n)| (h,sl))));;

Output:

val size_it : 'a list -> 'a existsize = <fun>

Unsize_It Function

The unsize_it should do the inverse of what the size_it function does. It should be able to convert a sized list into an unsized one. I have tried two versions of it, only the first one is working. The first one takes an slist and returns a list, while the second one take an existsize and returns a list. The second is a more accurate inverse to the size_it function.

Definition 1 (working):

let rec unsize_it1 .|m:'(nat)| (la:('(m),'a) slist): 'a list =
    (match la in 't list with
    |Nil -> []
    |Cons .|n:'(nat)| (lah,lat) -> lah::(unsize_it1 .|'(n)| lat));; 

Output:

val unsize_it1 : (forall m:'(nat) . ('(m), 'a) slist -> 'a list) = <forall>

Definition 2 (potential bug):

let rec unsize_it2 (ela:'a existsize): 'a list =
    (match ela as 'a existsize in 'a list with
    |E .|n:'(nat)| slist -> 
        (match   slist in 'a list with 
        |Nil -> []
        |Cons .|n:'(nat)| (lah,lat) -> lah::unsize_it2 (E .|'(n)| lat)));; 

Output:

Error while checking body of the context-refined branch:
  (n : nat) (a : OCamlType) (n := S n : nat)
  This expression has type ('(_UNBOUND_REL_3), 'a) slist
  but is here used with type ('(_UNBOUND_REL_1), 'b) slist

Sample Tests

The following is a list of sample interactions with concoqtion interpreter after loading the above definitions except for unsize_it2 that is not working:

let g n = if n then 0 else 1;;
val g : bool -> int = <fun>

let h x = (x mod 2) = 0;;
val h : int -> bool = <fun>

let l1 = Cons .|'(2)|(true, Cons .|'(1)| (false, Cons .|'(0)| (false, Nil)));;
val l1 : ('(3), bool) slist = Cons (true, Cons (false, Cons (false, Nil)))

let l1'= unsize_it1 .|'(3)| l1;;
val l1' : bool list = [true; false; false]

let l2 = maps .|'(3)| g l1;;
val l2 : ('(3), int) slist = Cons (0, Cons (1, Cons (1, Nil)))

let l2'= unsize_it1 .|'(3)| l2;;
val l2' : int list = [0; 1; 1]

let l3 = zips .|'(3)| l1 l2;;
val l3 : ('(3), bool * int) slist =
  Cons ((true, 0), Cons ((false, 1), Cons ((false, 1), Nil)))

let l3'= unsize_it1 .|'(3)| l3;;
val l3' : (bool * int) list = [(true, 0); (false, 1); (false, 1)]

let l4 = add_twices .|'(3)| true l1;;
val l4 : ('(5), bool) slist =
  Cons (true, Cons (true, Cons (true, Cons (false, Cons (false, Nil)))))

let l4'= unsize_it1 .|'(5)| l4;;
val l4' : bool list = [true; true; true; false; false]

let l5 = appends .|'(3),'(5)| l1 l4;;
val l5 : ('(3 + 5), bool) slist =
  Cons (true, Cons (false, Cons (false, Cons (true, Cons (true, Cons (true, Cons (false, Cons (false, Nil))))))))

let l5'= unsize_it1 .|'(8)| l5;;
val l5' : bool list = [true; false; false; true; true; true; false; false]

let l6 = generates 20 45 6;;
val l6 : int existsize =
  E (Cons (20, Cons (26, Cons (32, Cons (38, Cons (44, Nil))))))

let l7 = size_it [1;5;6;70];;
val l7 : int existsize = E (Cons (1, Cons (5, Cons (6, Cons (70, Nil)))))

let bigl = generates 1 10000 1;;
val bigl : int existsize =
  E
   (Cons (1,
     Cons (2,
      Cons (3,
       Cons (4,
        Cons (5,
         Cons (6,
          Cons (7, ..)))))))

let bigl' = generaten 1 10000 1;;
val bigl' : int list =
  [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21;
   22; 23; 24; ...]

Timing

Trxtime.init_times ();;
Trxtime.timenew "Regular zip"  (fun _ -> zipn l2' l2');;
Trxtime.timenew "Sized zip"   (fun _ -> (zips .|'(3)| l2 l2));;
Trxtime.timenew "Regular map"  (fun _ -> mapn g l1');;
Trxtime.timenew "Sized map"   (fun _ -> (maps .|'(3)| g l1));;
Trxtime.timenew "Regular append"  (fun _ -> appendn l2' l2');;
Trxtime.timenew "Sized append"  (fun _ -> (appends .|'(3),'(3)| l2 l2));;
Trxtime.timenew "Regular zip (big)"  (fun _ -> zipn bigl' bigl');;
let _ =match bigl as 'a existsize in unit with
    | E .|n:'(nat)| sl->
        let _ = Trxtime.timenew
            "Sized zip (big)" (fun _ -> zips .|'(n)| sl sl) in ();;
Trxtime.timenew "Regular map (big)"  (fun _ -> mapn h bigl');;
let _ =match bigl as 'a existsize in unit with
    | E .|n:'(nat)| sl->
        let _ = Trxtime.timenew
            "Sized map (big)" (fun _ -> maps .|'(n)| h sl) in ();;
Trxtime.timenew "Regular append (big)"  (fun _ -> appendn bigl' bigl');;
let _ =match bigl as 'a existsize in unit with
    | E .|n:'(nat)| sl->
        let _ = Trxtime.timenew
            "Sized append (big)" (fun _ -> appends .|'(n),'(n)| sl sl) in ();;
Trxtime.print_times ();;

I have run the timing test 4 times and I got very similar results each time. The following table summarizes the obtained results. It can be seen that in all cases (for small and big lists and for all tested functions) Sizing does not add any overhead but it does not save time neither. The difference in timing between both of them is very close to zero and should be ignored.

Function	Unsized (small lists)	Sized (small lists)	Unsized (big lists)	Sized (big lists)
zip	8.081659E-04	8.002251E-04	4.679529	4.712732
map	6.514416E-04	6.411777E-04	3.342658	3.308475
append	4.559612E-04	4.896012E-04	1.814624	1.829979