Sort

I'm working with Daniel Adler on this one.

Implementations and obstacles

Sized bubble sort

We started out by implementing sort on sized lists. Dan took insertion and quick sort, while I tried bubble and merge sort. Bubble sort is pretty easy:

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


(* Unsized version.  *)
let ububble (ls:'a ulist) (leq: 'a -> 'a -> bool) : 'a ulist =
  let rec recurse ls prev: 'a ulist * bool =
    match ls with
      | UNil -> (UCons (prev, UNil), false)
      | UCons (key, rest) ->
          if leq prev key then
            let (rest, xchgp) = recurse rest key in
              (UCons (prev, rest), xchgp)
          else
            let (rest, xchgp) = recurse rest prev 
            in
              (UCons (key, rest), true)
  and repeat ls =
    match ls with
      | UCons (key, rest) ->
          let (ls, xchgp) = recurse rest key in
            if xchgp then
              repeat ls
            else
              ls
      | UNil -> ls
  in
    repeat ls
;;


(* Sized version.  *)
let sbubble .|n:'(nat)| (ls:('a, '(n)) slist) (leq:'a -> 'a -> bool)
                      : ('a, '(n)) slist =
  let rec recurse .|n:'(nat)| (ls:('a, '(n)) slist) (prev:'a)
                            : ('a, '(S n)) slist * bool =
    match ls as ('a, 'n:'(nat)) slist in ('a, '(S n)) slist * bool with
      | Nil -> (Cons .|'(0)| (prev, Nil), false)
      | Cons .|m:'(nat)| (key, rest) ->
          if leq prev key then
            let (rest, xchgp) = recurse .|'(m)| rest key in
              (Cons .|'(S m)| (prev, rest), xchgp)
          else
            let (rest, xchgp) = recurse .|'(m)| rest prev in
              (Cons .|'(S m)| (key, rest), true)
  and repeat .|n:'(nat)| (ls:('a, '(n)) slist) : ('a, '(n)) slist =
    match ls as ('a, 'k:'(nat)) slist in ('a, '(k)) slist with
      | Cons .|m:'(nat)| (key, rest) ->
          let (ls, xchgp) = recurse .|'(m)| rest key in
            if xchgp then
               repeat .|'(S m)| ls
            else
              ls
      | Nil -> Nil
  in
    repeat .|'(n)| ls
;;

If you take a close look, the sized version is exactly the same as the unsized version with size specification. I straightforwardly added size parameters; then it typechecked, it ran, it did the job. Great.

Verified Bubble Sort

coq
  Require Arith.
  Theorem le_n_S : forall n m, n <= m -> S n <= S m.
  Proof.
    induction 1; auto.
  Qed.

  Theorem le_refl : forall n, n <= n.
  Proof.
    induction n; eauto.
  Qed.

  Theorem le_0_n : forall n, 0 <= n.
  Proof.
    induction n; auto.
  Qed.
end

type ('n:'(nat)) snat =
  | Zero : '(0) snat
  | Succ of let 'n:'(nat) in
      '(n) snat : '(S n) snat
and nlist =
  | NNil
  | NCons of let 'n:'(nat) in ('(n) snat * nlist)
and ('lb:'(nat)) olist =
  | ONil
  | OCons of let 'car:'(nat) 'cdrb:'(nat) 'ordproof:'(car <= cdrb) in
      ('(car) snat * '(cdrb) olist) : '(car) olist
and ('n:'(nat), 'm:'(nat)) leq_carrier =
  | True of let 'n:'(nat) 'm:'(nat) 'proof:'(n <= m) in
      unit : ('(n), '(m)) leq_carrier
  | False
and exists_olist =
  | E of let 'lb:'(nat) in '(lb) olist
;;

let rec leq .|n:'(nat), m:'(nat)| (x:'(n) snat) (y:'(m) snat)
                                : ('(n), '(m)) leq_carrier =
  match x, y in ('(n), '(m)) leq_carrier with
    | Zero, _ -> True .|'(0), '(m), '(le_0_n m)| ()
    | Succ .|n2:'(nat)| x2, Zero -> False
    | Succ .|n2:'(nat)| x2, Succ .|m2:'(nat)| y2 ->
        match leq .|'(n2), '(m2)| x2 y2
            as ('n3:'(nat), 'm3:'(nat)) leq_carrier
            in ('(S n3), '(S m3)) leq_carrier with
          | True .|n3:'(nat), m3:'(nat), p:'(n3 <= m3)| () ->
              True .|'(S n3), '(S m3), '(le_n_S n3 m3 p)| ()
          | False -> False
;;

coq
  Theorem le_rewrite : forall n n2 m m2 : nat,
              (n <= m) -> (n = n2) -> (m = m2) -> (n2 <= m2).
   intros.
   rewrite <- H0.
   rewrite <- H1.
   trivial.
  Qed.
  Implicit Arguments le_rewrite.
end

let rec ensure_sorted (ls : nlist) : exists_olist =
  let tack_on .|x:'(nat), l:'(nat)| (new_car:'(x) snat)
                                    (car : '(l) snat)
                                    (new_cdr : '(l) olist) =
    (match leq .|'(x), '(l)| new_car car
                             as ('x2:'(nat), 'l2:'(nat)) leq_carrier
                             in (* forall eqx:'(x = x2) eql:'(l = l2). *)
                               exists_olist with
      | True .|x3:'(nat), l3:'(nat), p:'(x3 <= l3)| () ->
          E .|'(x3)| (OCons .|'(x), '(l), '(le_rewrite p (refl_equal x) (refl_equal l))| (new_car, new_cdr))
      | False -> assert false)
  in
    match ls in exists_olist with
      | NNil -> E .|'(0)| ONil
      | NCons .|n:'(nat)| (car, cdr) ->
          match ensure_sorted cdr in exists_olist with
            | E .|m:'(nat)| new_cdr ->
                match new_cdr in exists_olist with
                  | ONil ->
                      E .|'(n)| (OCons .|'(n), '(n), '(le_refl n)| (car, ONil))
                  | OCons .|m2:'(nat), sth:'(nat), p:'(m2 <= sth)| (cadr, _) ->
                      tack_on .|'(n), '(m)| car cadr new_cdr
;;

let bubble (ls : nlist) : exists_olist =
  let rec recurse.|n:'(nat)| ls (prev: '(n) snat) : nlist * bool =
    match ls in nlist * bool with
      | NNil -> (NCons .|'(n)| (prev, NNil), false)
      | NCons .|m:'(nat)| (key, rest) ->
          (match leq .|'(n), '(m)| prev key in nlist * bool with
             | True .|n:'(nat), m:'(nat), p:'(n <= m)| () ->
                 let (rest, xchgp) = recurse .|'(m)| rest key in
                   (NCons .|'(n)| (prev, rest), xchgp)
             | False ->
                 let (rest, xchgp) = recurse .|'(n)| rest prev 
                 in
                   (NCons .|'(m)| (key, rest), true)
          )
  and repeat ls =
    match ls in nlist with
      | NCons .|n:'(nat)| (key, rest) ->
          let (ls, xchgp) = recurse .|'(n)| rest key in
            if xchgp then
              repeat ls
            else
              ls
      | NNil -> ls
  in
    ensure_sorted (repeat ls)
;;

We restricted our attention to lists of snats, to keep things relatively simple. nlist is the list of snats, which we introduced because we can't seem to instantiate the usual OCaml list in such a way that we can put different snat values in there:

[Zero; Succ .|'(0)| Zero] (* type error; '(0) snat \neq '(1) snat *)
[E .|'(0)| Zero; E .|'(1)| (Succ .|'(0)| Zero)] (* works, but very clumsy *)

The sort function (named bubble) takes an nlist and returns an olist. An olist is a list that is guaranteed to be sorted (in this case in ascending order), where each cons takes a proof that the car is no less than the lower bound of the cdr.

There's a problem with this type, however; olist is completely sorted and nlist is completely not sorted (as guaranteed properties go). It's an all or nothing, and the intermediate data structure of a bubble sort can't be expressed, because it's only partially sorted. While it's true that the list becomes gradually sorted starting from the tail, if we just build the result list element by element (which must be done on a separate list from the input or intermediate structure), we'd end up with insertion sort. So instead of doing that, I wrote a post-hoc checker (ensure_sorted) that takes an nlist as input, which must be sorted, and changes it into an olist.

This worked fine, but is deeply unsatisfactory. Since the ensure_sorted function must check that the input is sorted along the way, it must raise an error if it gets bad (unsorted) input. But appending this code to the sorting function is just as lame as adding an assertion at the end; if there is a bug in the sorting code, we crash. Thus, as static guarantees, we gained close to nothing. The output type guarantees that it's sorted (if the thread of execution survives up to that point), so it might be useful for feeding it to other functions that need sorted input (e.g. binary search; except not with lists), but that's about it.

Sized Merge Sort

Now we have a problem. We need to split up the input list into two equal-length (or off by 1 for odd-length lists) on every recursion step, so we want to represent the list's length as an exponentially encoded natural number:

type 'n:'(nat) xnat =
  | Z : '(0) xnat
  | Even of let 'n:'(nat) in
      '(n) xnat : '(2 * n) xnat
  | Odd of let 'n:'(nat) in
      '(n) xnat : '(S (2 * n)) xnat
;;

The question is, how do we build it, given a linear representation of the length? Obviously, if we try to build it top-down, we need exponential induction, which defeats the purpose. But on the other hand, to build it bottom-up, we need to type this function:

take_n : ('a, '(m)) slist -> '(n) xnat -> ('a, '(m-n)) slist

This has two problems: First, since coq's subtraction isn't a proper inverse of addition, we need to pass in a proof of '(m >= n), which I wasn't sure how to do. Emir suggested that I can start off the sorting algorithm with '(n >= n), and propagate the ordering by supplying new proofs each time. [I don't know how better to phrase this sentence. Hopefully I can improve it later...] Once that's taken care of, I need to tie the run-time modular arithmetic that tests the parity of the input length with the typing information. That's also not clear how to do.

Joseph suggested an alternative strategy, which is to convert the length to an unsafe representation (like an unsized list or int), build the xnat, and return it wrapped with `option'.

At any rate, I couldn't think of a resolution over a weekend, and besides I feel (as Dan agreed) being led astray from the primary objective of verifying sort. Therefore, I decided to initially leave out merge sort, leaving the possibly that I may give it a second look later.

Lambda-Calculus Interpreter

Simply Typed, Tagless

The untyped interpreter has two major sources of overhead. The first is gratuitous construction of closures at the OCaml-level, when evaluating a lambda. This can be eliminated by staging. The other source, which is the target of indexed typing, is the match performed on an operator object (to ensure that it's a function) before applying it.

Here's my initial try.

coq
  Inductive typ: Set :=
          | Int: typ
          | Fun: typ -> typ -> typ.
  Inductive environment: Set :=
          | Empty: environment
          | Ext: typ -> environment -> environment.

  Fixpoint eval_typ (t:typ) : OCamlType :=
    match t with
      | Int => OCaml_int
      | Fun x y => OCaml_Arr (eval_typ x) (eval_typ y)
    end.
  Fixpoint eval_env (e:environment) : OCamlType :=
    match e with
      | Empty => OCaml_unit
      | Ext t e2 => OCaml_Tuple (OCaml_List_cons (eval_typ t) (OCaml_List_cons (eval_env e2) OCaml_List_nil))
      end.
end;;

type ('env:'(environment), 't:'(typ)) texp =
  | TInt of let 'env:'(environment) in int : ('(env), '(Int)) texp
  | TVar0 of let 't2:'(typ) 'env:'(environment) in
      unit : ('(Ext t2 env), '(t2)) texp
  | TVarS of let 't:'(typ) 't2:'(typ) 'env:'(environment) in
      ('(env), '(t)) texp : ('(Ext t2 env), '(t)) texp
  | TLam of let 'arg:'(typ) 'ret:'(typ) 'env:'(environment) in
      ('(Ext arg env), '(ret)) texp : ('(env), '(Fun arg ret)) texp
  | TApp of let 'arg:'(typ) 'ret:'(typ) 'env:'(environment) in
      ('(env), '(Fun arg ret)) texp * ('(env), '(arg)) texp
        : ('(env), '(ret)) texp
;;

let rec teval .|ctx:'(typ), env:'(environment)|
   (expr:('(env), '(ctx)) texp) (env:'(eval_env env)) : '(eval_typ ctx) =
  match expr in '(eval_typ ctx) with
    | TInt .|e:'(environment)| x -> x
    | TVar0 .|t:'(typ), e:'(environment)| () ->
        (match env in '(eval_typ ctx) with
           | (x, _) -> x
           | _ -> assert false)
    | TVarS .|t2:'(typ), e:'(environment)| exp ->
        teval .|'(ctx), '(e)| exp
               (match env in '(eval_env e) with
                  | (_, x) -> x
                  | _ -> assert false)
    | TLam .|arg:'(typ), ret:'(typ), e:'(environment)| body ->
        (fun (x:'(eval_typ arg)) ->
           teval .|'(ctx), '(Ext arg env)| body (x, env))
    | TApp .|arg:'(typ), ret:'(typ), e:'(environment)| (op, arg) ->
        (teval .|'(Fun arg ret), '(e)| op env)
          (teval .|'(arg), '(e)| arg env)
;;

This apparently makes concoqtion go into an infinite loop. Ctrl-C reveals that it's caught inside ctypes.ml:

$ ../ometaconc/bin/conc <eval.ml 
[hit ^C]
EXCEPTION:
  Anomaly: assert failure
  (file "typing/ctype.ml", line 3642, characters 132-138). Please report.

Using fst instead of a match eliminates the problem:

let rec teval .|ctx:'(typ), env:'(environment)|
   (expr:('(env), '(ctx)) texp) (env:'(eval_env env)) : '(eval_typ ctx) =
  match expr in '(eval_typ ctx) with
    | TInt .|e:'(environment)| x -> x
    | TVar0 .|t:'(typ), e:'(environment)| () ->
        (match env in '(eval_typ ctx) with
           | (x, _) -> x
           | _ -> assert false)
    | TVarS .|t2:'(typ), e:'(environment)| exp ->
        teval .|'(ctx), '(e)| exp
               (match env in '(eval_env e) with
                  | (_, x) -> x
                  | _ -> assert false)
    | TLam .|arg:'(typ), ret:'(typ), e:'(environment)| body ->
        (fun (x:'(eval_typ arg)) ->
           teval .|'(ctx), '(Ext arg env)| body (x, env))
    | TApp .|arg:'(typ), ret:'(typ), e:'(environment)| (op, arg) ->
        (teval .|'(Fun arg ret), '(e)| op env)
          (teval .|'(arg), '(e)| arg env)
;;

Now it works:

(teval .|'(Fun Int Int), '(Empty)|
    (TApp .|'(Int), '(Fun Int Int), '(Empty)|
        (TLam .|'(Int), '(Fun Int Int), '(Empty)|
            (TLam .|'(Int), '(Int), '(Ext Int Empty)|
                (TVarS .|'(Int), '(Int), '(Ext Int Empty)|
                    (TVar0 .|'(Int), '(Empty)| ()))),
        (TInt .|'(Empty)| 1)))
      ())
2
;;

which is

((eval
  ((lambda (x)
     (lambda (y) x))
   1))
 2)

in scheme, outputs:

- : int = 1

miserable failure

For a change, I tried implementing it without eval_type, to no avail:

coq
  Inductive environment: Set :=
          | Empty: environment
          | Ext: OCamlType -> environment -> environment.

  Fixpoint eval_env (e:environment) : OCamlType :=
    match e with
      | Empty => OCaml_unit
      | Ext t e2 => OCaml_Tuple (OCaml_List_cons t (OCaml_List_cons (eval_env e2) OCaml_List_nil))
      end.
end;;

type ('env:'(environment), 't) texp =
  | TInt of let 'env:'(environment) in int : ('(env), int) texp
  | TVar0 of let 't2 'env:'(environment) in
      unit : ('(Ext t2 env), '(t2)) texp
  | TVarS of let 't 'dummy 'env:'(environment) in
      ('(env), '(t)) texp : ('(Ext dummy env), '(t)) texp
  | TLam of let 'arg 'ret 'env:'(environment) in
      ('(Ext arg env), '(ret)) texp : ('(env), '(OCaml_Arr arg ret)) texp
  | TApp of let 'arg 'ret 'env:'(environment) in
      ('(env), '(OCaml_Arr arg ret)) texp * ('(env), '(arg)) texp
        : ('(env), '(ret)) texp
;;


let rec teval .|env:'(environment), t:'(OCamlType)|
    (exp:('(env), '(t)) texp) (env:'(eval_env env)) : '(t) =
   match exp as ('env:'(environment), 't) texp  in '(t) with
     | TInt .|e:'(environment)| x -> x
     | TVar0 .|t, e:'(environment)| () ->
         (match env in '(t) with
            | (fst, _) -> fst
            | _ -> assert false)
     | TVarS .|t2, dummy, e:'(environment)| body ->
         teval .|'(e), '(t)| body
                             (match env in '(t) with
                                | (_, en) -> en
                                | _ -> assert false)
     | TLam .|arg, ret, e:'(environment)| body ->
         (fun (x:'(arg)) ->
            teval .|'(Ext arg e), '(t)| body (x, env))
     | TApp .|arg, ret, e:'(environment)| (op, arg) ->
         (teval .|'(e), '(OCaml_Arr arg ret)| op env)
           (teval .|'(e), '(arg)| arg env)
;;

Output:
Starting Concoqtion
MetaOCaml Concoqtion (Ocaml 3.08.0)

#                     environment is defined
environment_rect is defined
environment_ind is defined
environment_rec is defined
#                         eval_env is recursively defined
type ('a:'(environment), 'b:'(OCamlType)) texp =
    TInt of  let 'env:'(environment)  in  int : ('(env), int) texp
  | TVar0 of  let 't2:'(OCamlType)  'env:'(environment)  in  
            unit : ('(Ext t2 env), '(t2)) texp
  | TVarS of
             let 't:'(OCamlType)  'dummy:'(OCamlType)  'env:'(environment) 
                    in 
            ('(env), '(t)) texp : ('(Ext dummy env), '(t)) texp
  | TLam of
            let 'arg:'(OCamlType)  'ret:'(OCamlType)  'env:'(environment) 
                   in 
           ('(Ext arg env), '(ret)) texp : 
           ('(env), '(arg) -> '(ret)) texp
  | TApp of
            let 'arg:'(OCamlType)  'ret:'(OCamlType)  'env:'(environment) 
                   in 
           ('(env), '(arg) -> '(ret)) texp * 
           ('(env), '(arg)) texp : ('(env), '(ret)) texp
#                                           
Characters 304-312:
Error while unifying the type of the argument of match 
  '((fix eval_env (e0 : environment) : OCamlType :=
       match e0 with
       | Empty => OCaml_unit
       | Ext t0 e2 =>
           OCaml_Tuple
             (OCaml_List_cons t0
                (OCaml_List_cons (eval_env e2) OCaml_List_nil))
       end) env)
  and pattern type '(OCaml_Tuple
                       (OCaml_List_cons ?1294
                          (OCaml_List_cons ?1295 OCaml_List_nil))):
  This pattern matches values of type 'a * 'b
  but is here used to match values of type
    '((fix eval_env (e : environment) : OCamlType :=
         match e with
         | Empty => OCaml_unit
         | Ext t e2 =>
             OCaml_Tuple
               (OCaml_List_cons t
                  (OCaml_List_cons (eval_env e2) OCaml_List_nil))
         end) _UNBOUND_REL_6)
# 

It's choking on the coq functions. Could this be the problem Joseph mentioned last time?

Untyped, Tags

No-brainer; same deal as comp 311.

exception Error of string;;

type exp =
  | Int of int
  | Var of int
  | Lam of exp
  | App of exp * exp
and value =
  | VInt of int
  | VFun of (value -> value)
;;


let env_ext env v = v::env;;

let env_lookup = List.nth;;

let rec uteval env exp =
  match exp with
    | Int i -> VInt i
    | Lam e -> VFun (fun v -> uteval (env_ext env v) e)
    | Var n -> env_lookup env n
    | App (op, arg) ->
        match uteval env op with
          | VFun f -> f (uteval env arg)
          | _ -> raise (Error "Non-function at operator position.")
;;

szip without context refinement

value restriction

This code violates vaue restriction because we're doing computation inside the /\:

type ('a, 'n:'(nat)) slist =
  | Nil : ('a, '(0)) slist
  | Cons of let 'm:'(nat) in 'a * ('a, '(m)) slist : ('a, '(1 + m)) slist
and 'a ulist =
  | UNil
  | UCons of 'a * 'a ulist
;;

let cast .|a:'(nat),b:'(nat),p:'(a=b)| (x:'a) :'b = Obj.magic x;;

(* szip without context refinement.  *)
let rec szip .|l:'(nat)| (l1:('a, '(l)) slist) (l2:('b, '(l)) slist)
                       : ('a * 'b, '(l)) slist =
  (match (l1, l2) as ('a, 'l1:'(nat)) slist * ('b, 'l2:'(nat)) slist
                  in forall p:'(l1=l2). ('a * 'b, '(l2)) slist with
     | Nil, Nil -> /\ p:'(0=0). Nil
     | Cons .|i:'(nat)| (x, xs), Cons .|j:'(nat)| (y, ys) ->
         /\ p:'(i=j).
           let xs = cast .|'(i), '(j), '(p)| xs in
             Cons .|'(j)| ((x, y), szip .|'(j)| xs ys)
  ) .|'(refl_equal l)| ()
;;

output:
Characters 426-520:
  ...........let xs = cast .|'(i), '(j), '(p)| xs in
               Cons .|'(j)| ((x, y), szip .|'(j)| xs ys)
Value restriction violated. The expression
    let xs =
     ((cast .|'((i))| .|'((j))| .|'((p))|) xs) in
       (Cons ((x, y), ((szip .|'((j))|) xs ys))) must be a value.

We work around with eta conversion as usual.

let cast .|a:'(nat),b:'(nat),p:'(a=b)| (x:'a) :'b = Obj.magic x;;

(* szip without context refinement.  *)
let rec szip .|l:'(nat)| (l1:('a, '(l)) slist) (l2:('b, '(l)) slist)
                       : ('a * 'b, '(l)) slist =
  (match (l1, l2) as ('a, 'l1:'(nat)) slist * ('b, 'l2:'(nat)) slist
                  in forall p:'(l1=l2). unit -> ('a * 'b, '(l2)) slist with
     | Nil, Nil -> /\ p:'(0=0). fun () -> Nil
     | Cons .|i:'(nat)| (x, xs), Cons .|j:'(nat)| (y, ys) ->
         /\ p:'(i=j). fun () ->
           let xs = cast .|'(i), '(j), '(p)| xs in
             Cons .|'(j)| ((x, y), szip .|'(j)| xs ys)
  ) .|'(refl_equal l)| ()
;;

Braun trees

A Braun tree is an AVL tree with the additional restriction that the left subtree have greater than or equal number of items as the right.

The tree we implement here guarantees that sizing constraint but doesn't have any notion of ordering (at the type level) so it's not very practically useful as a tree.

type

Here's the type for the indexed braun tree type.

type ('m:'(nat), 'a) braun =
  | BBranch of let 'n:'(nat) in          (* diff = 0.  *)
      'a * ('(n), 'a) braun * ('(n), 'a) braun : ('(S (n + n)), 'a) braun
  | LBranch of let 'n:'(nat) in          (* diff = 1. *)
      'a * ('(S n), 'a) braun * ('(n), 'a) braun : ('(S (S (n + n))), 'a) braun
  | Null : ('(0), 'a) braun
;;

copy

This function creates a tree of n elements (all elements equal). This runs in O(n) time, naively allocating a structure for each node.

let rec copy (x:'a) n : 'a existsbraun =
  if n = 0 then
    E .|'(0)| Null
  else if (n mod 2) = 1 then
    match copy x (n / 2) in 'a existsbraun with
      | E .|k:'(nat)| t ->
          E .|'(S (k + k))| (BBranch .|'(k)| (x, t, t))
 else
   match copy x (n / 2 - 1) in 'a existsbraun with
     | E .|k:'(nat)| t ->
         E .|'(S (S (k + k)))| (LBranch .|'(k)| (x, insert .|'(k)| x t, t))
;;

copy2

The more efficient copy that uses O(log (n)) time and space. This is done by reusing subtrees as much as possible.

We need the temporary results to be wrapped in one existential in order to impose a condition on their types.

type 'a existspair =
  | Ep of let 'm:'(nat) in
      (('(S m), 'a) braun * ('(m), 'a) braun)
;;

let copy2 x n =
  let aux .|a, l:'(nat)| x =
        cast .|'(OCaml_braun (S (S l + S l)) a),
               '(OCaml_braun (S (S (S (l + l)))) a),
               '(tree_size_cast a (S (S l + S l)) (S (S (S (l + l)))) (pull_out l))| x
  in
  let rec copy2 x n =
    match n with
      | 0 -> Ep .|'(0)| (BBranch .|'(0)| (x, Null, Null), Null)
      | n when n mod 2 = 0 ->
          (match copy2 x (n/2 - 1) in 'a existspair with
             | Ep .|m:'(nat)| (l, r) ->
                 let bigger = aux .|'a, '(m)| (BBranch .|'(S m)| (x, l, l))
                 in
                 Ep .|'(S (S (m+m)))| (bigger,
                                       LBranch .|'(m)| (x, l, r))
          )
      | n ->
          (match copy2 x ((n-1)/2) in 'a existspair with
             | Ep .|m:'(nat)| (l, r) ->
                 Ep .|'(S (m+m))| (LBranch .|'(m)| (x, l, r),
                                   BBranch .|'(m)| (x, r, r))
          )
  in
    match copy2 x n in 'a existsbraun with
      | Ep .|m:'(nat)| (_, r) -> E .|'(m)| r
;;

copy2 "ahya" 12;;

gives

E
 (LBranch ("ahya",
   LBranch ("ahya",
    BBranch ("ahya", BBranch ("ahya", Null, Null),
     BBranch ("ahya", Null, Null)),
    LBranch ("ahya", BBranch ("ahya", Null, Null), Null)),
   BBranch ("ahya", LBranch ("ahya", BBranch ("ahya", Null, Null), Null),
    LBranch ("ahya", BBranch ("ahya", Null, Null), Null))))

diff

This is trivial, because the nodes carry the diff information:

let diff t =
  match t as ('k:'(nat), 'a) braun in int with
    | BBranch .|n:'(nat)| (_, _, _) -> 0
    | LBranch .|m:'(nat)| (_, _, _) -> 1
;;

insert

For the insertion, naïvely implementing

(* FLAWED version *)
let rec insert .|n:'(nat)| item (t:('(n), 'a) braun) : ('(S n), 'a) braun =
  match t in ('(S n), 'a) braun with
    | BBranch .|k:'(nat)| (b_val, l, r) ->
        LBranch .|'(k)| (item, insert .|'(k)| b_val r, l)
    | LBranch .|k:'(nat)| (b_val, l, r) ->
        BBranch .|'(S k)| (item, insert .|'(k)| b_val r, l)
    | Null ->
        BBranch .|'(0)| (item, Null, Null)
;;

fails, because concoqtion can't discover some basic arithmetical facts on its own:

Characters 1017-1068:
Type [(k : nat) (n := S (S (k + k)) : nat)] |- 
  ('(S n), 'c1) braun was expected but ('(S (S k + S k)), 'c1) braun
  was inferred for the branch expression. 

So we introduce a casting operator:

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

The cast is a safe-guarding wrapper to the type-cheating primitive Obj.magic, which is an identity function with the type 'a -> 'b, i.e. converts any type to any type. The interface file says Obj.magic is not for the casual user, and sure enough, you can abuse it to content yourself with some sweet messages like

jun@debian /dvl/metaocaml/MetaOCaml_308_alpha_027-C-07
$ ./ometaconc/bin/conc
Starting Concoqtion
MetaOCaml Concoqtion (Ocaml 3.08.0)

# (Obj.magic "str") + 0;;
- : int = -608660854
# (Obj.magic 0) ^ "abc";;
Segmentation fault

Now that looks like a bare C cast, doesn't it. Finally, I need to prove to Coq that the two types are in fact equal. I've cheated a bit so far using tactics, but I'll try to write a non-tactical version later. Right now it's important that it works.

coq
  Lemma tree_size_cast : forall e, forall m n:nat, (m=n) ->
           (OCaml_braun m e) = (OCaml_braun n e).
    intro; intro; intro.
    intro H.
    rewrite -> H.
    trivial.
  Qed.

  Lemma pullr : forall l k:nat, S (k + l) = k + S l.
    intros.
    induction k.
    simpl; reflexivity.
    simpl; rewrite -> IHk.
    reflexivity.
  Qed.

  Lemma pull_out : forall k:nat, S (S k + S k) = S (S (S (k + k))).
    intros.
    simpl.
    rewrite <- (pullr k k).
    reflexivity.
  Qed.

end
let rec insert .|n:'(nat)| item (t:('(n), 'a) braun) : ('(S n), 'a) braun =
  let aux .|a, l:'(nat)| (x:('(S (S l + S l)), 'a) braun) =
        cast .|'(OCaml_braun (S (S l + S l)) a),
               '(OCaml_braun (S (S (S (l + l)))) a),
               '(tree_size_cast a (S (S l + S l)) (S (S (S (l + l)))) (pull_out l))| x
  in
  match t in ('(S n), 'a) braun with
    | BBranch .|k:'(nat)| (b_val, l, r) ->
        LBranch .|'(k)| (item, insert .|'(k)| b_val r, l)
    | LBranch .|k:'(nat)| (b_val, l, r) ->
        aux .|'a, '(k)| (BBranch .|'(S k)| (item, insert .|'(k)| b_val r, l))
    | Null ->
        BBranch .|'(0)| (item, Null, Null)
;;

But Daniel has a workaround about this equality issue. Replacing addition with multiplication somehow allows concoqtion to unify the type without assistance.

type equality by normalization

Here's Dan's type:

type ('n:'(nat),'a) tree =
  | BLeaf : ('(0), 'a) tree
  | BNodeL of let 'm:'(nat) in
          'a * ('(S m), 'a) tree * ('(m), 'a) tree
      : ('(S (S (m*2))), 'a) tree
  | BNode of let 'm:'(nat) in
          'a * ('(m), 'a) tree * ('(m), 'a) tree
      : ('(S (m*2)), 'a) tree
;;

The reason this works has to do with the way concoqtion decides type equality. It normalizes by unrolling inductively defined operators in the types as much as possible, and compares the results syntactically.

In the case of my type where the type of BBranch (BNode) is indexed by

'(S (m + m))

the typechecker needs compare

S S (S (k + k))

and

S (S k + S k)

Now, since coq's addition is defined inductively on the first argument, the S on the first argument can be pulled out:

plus = 
fix plus (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end
     : nat -> nat -> nat

(substituting S (S k + S k) into this definition, we can derive)

S (S k + S k) = S S (k + S k)

Since k cannot be broken down further, we're stuck. For the same reason, S S S (k + k) is already fully normalized. But

S S (k + S k) /= S S S (k + k)

as strings. However, with the multiplicative definition, the type checker is asked to compare

S S (k * 2) vs ((S k) * 2))

Since multiplication inducts on the first argument

mult = 
fix mult (n m : nat) {struct n} : nat :=
  match n with
  | O => 0
  | S p => m + mult p m
  end
     : nat -> nat -> nat

we can expand the latter as

((S k) * 2) = 2 + (k * 2) = S S (k * 2)

(the 2 + is expanded by applying the definition of plus).

delete

This function deletes the newest member from a braun tree. I used the new type that uses n*2 instead of n*n.

type ('m:'(nat), 'a) braun =
  | BBranch of let 'n:'(nat) in          (* diff = 0.  *)
      'a * ('(n), 'a) braun * ('(n), 'a) braun : ('(S (n * 2)), 'a) braun
  | LBranch of let 'n:'(nat) in          (* diff = 1. *)
      'a * ('(S n), 'a) braun * ('(n), 'a) braun : ('(S (S (n * 2))), 'a) braun
  | Null : ('(0), 'a) braun
and 'a existsbraun =
  | E of let 'n:'(nat) in ('(n), 'a) braun
;;

let rec delete .|m:'(nat)| (t:('(S m), 'a) braun) : ('(m), 'a) braun =
  match t in ('(m), 'a) braun with
    | LBranch .|n:'(nat)| (x, l, r) ->
        BBranch .|'(n)| (x, delete .|'(n)| l, r)
    | BBranch .|n:'(nat)| (x, l, r) ->
        match r in ('(n * 2), 'a) braun with
          | Null -> Null
          | LBranch .|k:'(nat)| _ ->
              LBranch .|'(S (k * 2))| (x, l, delete .|'(S (k * 2))| r)
          | BBranch .|k:'(nat)| _ ->
              LBranch .|'(k * 2)| (x, l, delete .|'(k * 2)| r)
;;

This only runs on the newest

(rudimentary) test

(*
(let ((counter 0) (end 10))
  (insert "let tmp0 = Null;;\n")
  (while (<= counter end)
    (setq counter (+ counter 1))
    (insert (concat "let tmp"
                    (number-to-string counter)
                    " = insert .|'("
                    (number-to-string (- counter 1))
                    ")| "
                    (number-to-string (- counter 1))
                    " tmp"
                    (number-to-string (- counter 1))
                    ";;\n"))))
*)
let tmp0 = Null;;
let tmp1 = insert .|'(0)| 1 tmp0;;
let tmp2 = insert .|'(1)| 2 tmp1;;
let tmp3 = insert .|'(2)| 3 tmp2;;
let tmp4 = insert .|'(3)| 4 tmp3;;
let tmp5 = insert .|'(4)| 5 tmp4;;
let tmp6 = insert .|'(5)| 6 tmp5;;
let tmp7 = insert .|'(6)| 7 tmp6;;
let tmp8 = insert .|'(7)| 8 tmp7;;
let tmp9 = insert .|'(8)| 9 tmp8;;
let tmp10 = insert .|'(9)| 10 tmp9;;
let tmp11 = insert .|'(10)| 11 tmp10;;

# val tmp11 : ('(11), int) braun =
  BBranch (11,
   BBranch (10, LBranch (8, BBranch (4, Null, Null), Null),
    LBranch (6, BBranch (2, Null, Null), Null)),
   BBranch (9, LBranch (7, BBranch (3, Null, Null), Null),
    LBranch (5, BBranch (1, Null, Null), Null)))

a note on quantifiers

proof of (A x. P(x) --> Q) = ((E x.P(x)) --> Q)

A is the universal quantifier (forall), and E is the particular existential quantifier (exists). They have the same meaning as in mathematics.

Given by Cherif:

Here, Q is a well-formed formula with no free occurrence of x.

We want to prove A x.P(x) --> Q iff (E x. P(x)) --> Q. We can do that by reducing both formulae to a canonical form and observing that they are structurally equal.

For any X and Y, X --> Y is equivalent to (not X) or Y. Thus

A x. P(x) --> Q <=> A x. (not P(x)) or Q <=> (A x. not P(x)) or Q

where the last step uses the fact that x is not used in Q, and

(E x. P(x)) --> Q <=> (not E x. P(x)) or Q <=> (A x. not P(x)) or Q

Thus (A x. P(x) --> Q) <=> ((E x. P(x)) --> Q).

Existential Import

The proof given above, with the parentheses, is correct in Boolean and free logic, but not Aristotelian logic---the difference between all the logics being existential import.

First some notation: We'll only consider symbolic logic, where everything is stated in symbols instead of English. In addition to A and E, I'll use S with a similar syntax (e.g. S x. P(x)), read "some". The single arrow "-->" means "implies"; a double arrow "=>" means "from which we may conclude". The difference is that

   P /\ P --> Q

is a statement that we know P and that P implies Q, but

   P /\ P --> Q => Q

describes a mental process where we start with P and P implies Q to conclude Q (modus ponens). The double arrow has lower precedence as a connective. I'll occasionally make use of LaTeX^? commands.

Quantification has two forms:

  A x. P(x) --- all x are P(x)

and

  S x. P(x) --- some x satisfy P(x).

The former is called universal quantification, because it talks about everything, and the latter is called a particular quantification (traditionally, they are subdivided into affirmatives and negatives, depending on if P affirms or denies something).

There are two sticky issues with the interpretation of statements involving quantification. First, what exactly is "all"? If it's absolutely everything, then we can't simply state things like

  A n. n + 1 > n

because n could be a complex number, or worse, a bag of M&Ms. Therefore, quantification is taken to implicitly range over a specific class of things---called the domain of discourse or universe---that are relevant to the discussion, for example the real numbers. In math, we sometimes clarify the domain with the \in symbol, thus writing like

  A \in \mathbb{R}. n + 1 > n.

Note that this wouldn't be a problem if we stated things in a natural language (as did Aristotle) rather than symbols, because then the x would have to be referred to by the domain it belongs to; for instance in English, we say "all alarm clocks fail on important days".

The next is whether the domain is allowed to be empty. Does "A x. P(x)" imply that such an x exists in the domain? What about S? A quantifier is said to have existential import when a statement using that quantifier is understood to imply the existence of an object that makes it true.

Aristotle, who first studied this form of logic as categorical syllogism, ruled that both universals and particulars have existential import, because if one is to assert something, he must be certain that such a thing exists to begin with. This is called Aristotelian logic. This entails some subtle problems, for example the benign-looking equality axiom

  A x. x == x

is false in some domains. For if this were always true,

  A God. God == God => E x. x == God

would be a valid inference. A proper statement would be

  (E x) --> (A x.x == x)

where the first (E x) is a condition that states the non-emptiness of the domain. (Note that all problems can be circumvented by being clairvoyant like this, and so this whole fuss about existential import is about intuitiveness and convenience.)

Wikipedia mentions that this was particularly problematic for medieval theologians who wanted to talk about things whose existence is not obvious. And also I imagine it was troublesome for mathematicians, because people were unsure of the genuineness of negative or complex numbers until as late as Descartes (he called negative numbers "false numbers" [1]). Some people thought it fit to say that neither universals or particulars had existential import. This is called *free logic*.

The convention now widely in use in mathematics was popularized by George Boole, whose choise was to give particulars existential import but not to universals. Hence we now use E as a particular quantifier instead of S. This is called Boolean logic.

The terms Aristotelian, Boolean, and free logic seem to be fairly standard, but Aristotelian and Boolean may be used to emphasize other aspects of their logic (especially Boolean logic, which was historically important in introducing symbolism and algebraic analysis to logical inference).

[1] Pesic, Peter. Abel's Proof: An Essay on the Sources and Meaning of Mathematical Unsolvability. MIT Press, 2003.

Lists

Walid: Very good job on this writeup, and on catching that bug! May main suggestion is to avoid the use of and unless you are defining mutually recursive types (or functions). Also, it would be good to collect all timings at end and to tabulate results.

Here's the type of my sized list. ulist is the unsized list, crafted for comparison.

type ('a, 'n:'(nat)) slist =
  | Nil : ('a, '(0)) slist
  | Cons of let 'm:'(nat) in 'a * ('a, '(m)) slist : ('a, '(1 + m)) slist
;;
type 'a ulist =
  | UNil
  | UCons of 'a * 'a ulist
;;

at_size (unsized -> sized conversion a la take_n)

code

let (>>=) prod consum =
  match prod with
    | None -> None
    | Some x -> consum x
;;

let rec at_size .|m:'(nat)| (n:'(m) snat) (ls:'a ulist) : ('a, '(m)) slist option =
   let tack_on .|k:'(nat)| x (ls:('a, '(k)) slist) : ('a, '(1+k)) slist option =
    match ls as ('a, 'n:'(nat)) slist in ('a, '(1+n)) slist option with
      | Nil -> Some (Cons .|'(0)| (x, Nil))
      | ls -> Some (Cons .|'(n)| (x, ls))
  in
    match n, ls in ('a, '(m)) slist option with
      | Zero, _ -> Some Nil
      | Succ .|m_1:'(nat)| _, UNil -> None
      | Succ .|m_1:'(nat)| l, UCons (x, xs) ->
          (at_size .|'(m_1)| l xs) >>= (tack_on .|'(m_1)| x)
;;

The >>= is monadic syntax borrowed from Haskell. I encountered a possible bug while tweaking it a little; see the "potential bug" subsection.

test:

at_size .|'(1)| (Succ .|'(0)| Zero) test_ulist;;
at_size .|'(1)| (Succ .|'(0)| Zero) UNil;;

output:

- : (int, '(1)) slist option = Some (Cons (5, Nil))
# - : ('_a, '(1)) slist option = None

potential bug

The following code exhibits an apparently incorrect behavior. When at_size is called, the match in that function is falling through to the last catch-all branch, even though individually matching values reveals that it should be caught by the third branch.

type 'a ulist =
  | UNil
  | UCons of 'a * 'a ulist
;;

type ('n:'(nat)) snat =
  | Zero : '(0) snat
  | Succ of let 'm : '(nat) in
      '(m) snat : '(S m) snat
;;

let rec at_size .|m:'(nat)| (n:'(m) snat) (ls:'a ulist) : int =
  match ls, n (* "as 'a ulist, 'n:'(nat) snat" crashes with transl_type_pattern (see below) *)
                  in int with
    | _, Zero -> 0              (* Doesn't happen if UNil, Zero and *)
                                (* UCons (_,_), Zero are matched separately *)
    | UNil, Succ .|m_1:'(nat)| _ -> 1
    | UCons (x, xs), Succ .|m_1:'(nat)| l -> 2
    | _, _ ->
        print_string "match failed\n";
        (match ls in unit with
           | UNil -> print_string "unil, ";
           | UCons (_,_) -> print_string "ucons, ";
           | _ -> print_string "unknown list, ");
        (match n in unit with
           | Zero -> print_string "0\n";
           | Succ .|x:'(nat)| _ -> print_string "> 0\n");
        (match ls, n in unit with
           | _, Zero -> print_string "_, zero\n"
           | UCons (x, xs), Succ .|x:'(nat)| _ -> print_string "cons, succ\n";
           | _, _ -> print_string "sth else\n");
        assert false;
;;

let test_ulist = UNil;;

(* Doesn't happen with at_size .|'(0)| *)
at_size .|'(1)| (Succ .|'(0)| Zero) UNil;;

(* Can't make this to compile; I get:

Error while unifying type scrutinee type
  '(OCaml_Tuple
      (OCaml_List_cons (OCaml_ulist ?10893)
         (OCaml_List_cons (OCaml_snat 1) OCaml_List_nil)))
  and pattern type '(OCaml_Tuple
                       (OCaml_List_cons ?10948
                          (OCaml_List_cons (OCaml_snat 0) OCaml_List_nil))):
  This pattern matches values of type '(1)
  but is here used to match values of type '(0)


  Adding "as 'a ulist, ('m:'(nat)) snat" results in
  transl_type_pattern being thrown:

EXCEPTION:
  Anomaly: uncaught exception Failure "Error in transl_type_pattern. Please report.".
  Please report.

*)

(*
match UNil, (Succ .|'(0)| Zero) in int with
  | _, Zero -> 0
  | UNil, Succ .|m:'(nat)| _ -> 0
  | UCons (_, _), Succ .|n:'(nat)| _ -> 0
  | _, _ -> assert false
;;
*)

Output (and how I ran the program):

jun@debian /dvl/metaocaml/MetaOCaml_308_alpha_027-C-07/scratch
$ ../ometaconc/bin/conc < test.ml
Starting Concoqtion
MetaOCaml Concoqtion (Ocaml 3.08.0)

#       type 'a:'(OCamlType) ulist =
    UNil:'a ulist
  | UCons of   'a * 'a ulist : 'a ulist
#           type 'a:'(nat) snat =
    Zero:'(0) snat
  | Succ of  let 'm:'(nat)  in  '(m) snat : '(S m) snat
#                                             val at_size : (forall m:'(nat) . '(m) snat -> 'a ulist -> int) = <forall>
#   val test_ulist : 'a ulist = UNil
#     match failed
unil, > 0
sth else
Exception: Assert_failure ("", 30, 9).
#   * * * * * * * * * * * * * * * * * * * *     * * * * * * *
jun@debian /dvl/metaocaml/MetaOCaml_308_alpha_027-C-07/scratch
$ ../ometaconc/bin/concc test.ml && ../ometaconc/bin/conc test.cmo

Cannot find Coq constant OCamlType (as path Concoqtion.OCamlType)
match failed
unil, > 0
sth else
Starting Concoqtion

In both cases, the match doesn't work as expected, and goes to the clause with assert false. Assertion failure is not reported for a non-interactive (bytecompiled) session (the exception is raised, the runtime just doesn't print a message in response).

size_it (unsized -> sized conversion)

The exists_slist type emulates an existential using forall, whose equivalence is discussed above.

type ('n:'(nat)) snat =
  | Zero : '(0) snat
  | Succ of let 'm : '(nat) in
      '(m) snat : '(S m) snat
and 'a exists_slist = E of let 'n:'(nat) in ('a, '(n)) slist
and exists_n = En of let 'n:'(nat) in '(n) snat
;;

let rec size_it = function
  | UNil -> E .|'(0)| Nil
  | UCons (x, xs) ->
      match size_it xs as 'a exists_slist in 'a exists_slist with
        | E .|m:'(nat)| (ls : ('a, '(m)) slist) ->
            E .|'(1+m)| (Cons .|'(m)| (x, ls))
;;

test:

test_ulist = fib_list 5;;
size_it test_ulist;;

fib_list n returns a list of the fibonacci numbers from F_n down to F_0.

output:

- : int exists_slist =
E (Cons (5, Cons (3, Cons (2, Cons (1, Cons (1, Cons (0, Nil)))))))

map

code

smap is the sized version. umap is for unsized. Both are recursive.

let rec smap .|l:'(nat)| f (ls:('a, '(l)) slist) : ('b, '(l)) slist =
  match ls as ('a, 'm:'(nat)) slist in ('a, '(m)) slist with
    | Nil -> Nil
    | Cons .|m:'(nat)| (car, cdr) ->
        Cons .|'(m)| (f car, smap .|'(m)| f cdr)
;;

let rec umap f = function
  | UNil -> UNil
  | UCons (x, xs) -> UCons (f x, umap f xs)
;;

test:

smap .|'(4)| ((+) 10) (Cons .|'(3)| (0, Cons .|'(2)| (1, Cons .|'(1)| (2, Cons .|'(0)| (3, Nil)))));;

outputs:

 - : (int, '(4)) slist = Cons (10, Cons (11, Cons (12, Cons (13, Nil))))

timing

I compared the times for smap, umap, and List.map. The code looked like:

Trx.init_times ();;
Trx.timenew "map" (fun () -> umap ((+) 10) test_ulist);;
Trx.timenew "smap" (fun () -> match test_slist as 'a exists_slist in unit with
   | E .|m:'(nat)| ls -> ignore (smap .|'(m)| ((+) 10) ls));;
Trx.timenew "List.map" (fun () -> List.map ((+) 10) test_olist);;
Trx.print_times ();;

I ran it 3 times in a row, byte-compiled beforehand. For small lists (5 elements), I got results like:

5 elements:
__ map ____________________ 524288x avg= 2.473216E-03 msec
__ smap ___________________ 524288x avg= 2.346551E-03 msec
__ List.map _______________ 524288x avg= 2.912481E-03 msec

For long lists (5000 elements), the results looked similar.

5000 elements:
__ map _______________________ 512x avg= 2.017765E+00 msec
__ smap ______________________ 512x avg= 2.014144E+00 msec
__ List.map __________________ 512x avg= 2.603986E+00 msec

The results were consistent up to the first decimal place, and re-ordering did not make any difference.

zip

code

Here's zip. The unsized version needs to check for inconsistent input and throw an exception if necessary.

let rec szip .|l:'(nat)| (l1:('a, '(l)) slist) (l2:('b, '(l)) slist)
                       : ('a * 'b, '(l)) slist =
  match (l1, l2) in ('a * 'b, '(l)) slist with
    | Nil, Nil -> Nil
    | Cons .|i:'(nat)| (x, xs), Cons .|i:'(nat)| (y, ys) ->
        Cons .|'(i)| ((x, y), szip .|'(i)| xs ys)
;;

exception Error;;
let rec uzip l1 l2 =
  match l1, l2 with
    | UNil, UNil -> UNil
    | UCons (x, xs), UCons (y, ys) ->
        UCons ((x, y), uzip xs ys)
    | _ -> raise Error
;;

test:

let ls = Cons .|'(3)| (0, Cons .|'(2)| (1, Cons .|'(1)| (2, Cons .|'(0)| (3, Nil))));;
szip .|'(4)| ls ls;;

output:

- : (int * int, '(4)) slist =
Cons ((0, 0), Cons ((1, 1), Cons ((2, 2), Cons ((3, 3), Nil))))

timing

The code is:

Trx.init_times ();;
Trx.timenew "zip" (fun () -> uzip test_ulist test_ulist);;
Trx.timenew "szip"
  (fun () -> match test_slist as 'a exists_slist in unit with
     | E .|m:'(nat)| ls -> ignore (szip .|'(m)| ls ls));;
Trx.print_times ();;

For both long and short lists, the two functions performed equally.

5 elements:
__ zip ____________________ 524288x avg= 1.986718E-03 msec
__ szip ___________________ 524288x avg= 1.998772E-03 msec

5000 elements:
__ zip _______________________ 512x avg= 3.419922E+00 msec
__ szip ______________________ 512x avg= 3.425808E+00 msec

Results were consistent up to the first decimal place and didn't fluctuate with reordering.

summary of timing results

Here's a tabulated summary of timing results.

Code	Average time	Comment
map (5 elements)	2.473216E-03 msec
smap (5 elements)	2.346551E-03 msec
List.map (5 elements)	2.912481E-03 msec
map (5000 elements)	2.017765E+00 msec
smap (5000 elements)	2.014144E+00 msec
List.map (5000 elements)	2.603986E+00 msec
zip (5 elements)	1.986718E-03 msec
szip (5 elements)	1.998772E-03 msec
zip (5000 elements)	3.419922E+00 msec
szip (5000 elements)	3.425808E+00 msec