Rank-2 polymorphism and non-uniform types, revisited

I've committed a number of errors and inaccuracies in my last post that warrant clarification. The most egregious and urgent is that the definition I gave for length is utterly wrong: the type encodes the length from the inside out, so that its "most significant bit" is the inner constructor. The recursion must take the form of a right fold, not of a left fold as I wrote. The correct function is then:

type length = { length : 'a . 'a vec -> int }

let length v =
  let rec length = { length = function
    Nil         -> 0
  | One (_, ps) -> 1 + length.length (Zero ps)
  | Zero    ps  -> 2 * length.length ps
  } in length.length v

Second, the option -rectypes is not necessary in OCaml 3.11.0 in order to use non-uniform recursion with this technique. The language permits non-uniform type definitions just fine. But, as Okasaki remarks, "[a]lthough Standard ML allows the definition of non-uniform recursive datatypes, the type system disallows most of the interesting functions on such types." (Okasaki, Chris. Purely Functional Data Structures, p. 143). What -rectype does is to disable the so-called occurs check in the typechecking algorithm that forces an error if a type is found to be defined in terms of itself when reconstructing the type of an expression via unification. This is why the types resulting in the compilation of a function using non-uniform recursion have the form E[α] as α, for a type expression E.

Third, I spoke of the type of a non-uniform parameter as being existential, which is technically true in this particular case but not the usual characterization of such a type. The way in which the type t→∀α.E[α] is more commonly described is as rank-2:

A type is said to be of rank 2 if no path from its root to a ∀ quantifier passes to the left of 2 or more arrows, when the type is drawn as a tree. For example, (∀X.X→X)→Nat is of rank 2, as are Nat→Nat and Nat→(∀X.X→X)→Nat→Nat, but ((∀X.X→X)→Nat)→Nat is not.

(Pierce, Benjamin C. Types and Programming Languages, p. 359)

A type definition type α t = … is a function from α to the declared type, so it counts as an arrow. Furthermore, there is an encoding of existential types in terms of rank-2 types that for this application suffices. This is the source of my confusion. Abstract signatures implement existential types in OCaml, which is why I said that this technique can be applied by means of a module. Also, OCaml allows rank-2 polymorphism in exactly two places: in record type declarations and in class declarations. So I missed a third way to encode non-uniform recursion in OCaml, namely via objects.

In a comment to the last post, bluestorm shows examples of the three encodings, using local module definitions to tidy up the global namespace of types and record labels. I want to compare the efficiency of the three approaches. The following function serves as a simple timing loop:

let test lap f e =
  let now = Sys.time () in
  let rec go cnt =
    let dt = Sys.time () -. now in
    if dt > lap then dt /. float cnt else
    (ignore (f e); go (succ cnt))
  in go 0

(the toplevel in my machine has an overhead of 4.9µs to execute the empty loop). Note that the result of the function is thrown away; fortunately, OCaml is a strict language. The test would measure the time it takes for different versions of index to find an element. This will require some test data. The simplest way to build a long list is with range:

let range m n =
  let rec go l i =
    if i < m then l else
    go (cons i l) (pred i)
  in go Nil n

Now everything works as expected:

# length (range 1 500_000) ;;
- : int = 500000

The first version of index uses records to encode the rank-2 type:

let index1 n v =
  let module Index = struct
    type index = { index : 'a . int -> 'a vec -> 'a }
    let rec index = { index = fun n l -> match l with
      Nil                    -> failwith "index"
    | One (x, ps) when n = 0 -> x
    | One (x, ps)            -> index.index (n - 1) (Zero ps)
    | Zero    ps             ->
      let (l, r) = index.index (n / 2) ps in
      if n mod 2 = 0 then l else r
    }
  end in Index.index.Index.index n v

(Malkovich Malkovich Malkovich). This is what I wrote in the last post, but now using a local module to encapsulate the type definitions, as per bluestorm's suggestion. The second version uses an object to encode the rank-2 type:

let index2 n v =
  let index = object (self)
    method index : 'a . int -> 'a vec -> 'a =
      fun n l -> match l with
        Nil                    -> failwith "index"
      | One (x, ps) when n = 0 -> x
      | One (x, ps)            -> self#index (n - 1) (Zero ps)
      | Zero    ps             ->
        let (l, r) = self#index (n / 2) ps in
        if n mod 2 = 0 then l else r
  end in index#index n v

Objects in OCaml are always self-recursive. The third version uses a recursive module to encode the non-uniform recursion by forcing the type of the second argument to remain generic:

let index3 n v =
  let module M = struct
    module rec Index : sig
      val index : int -> 'a vec -> 'a
    end = struct
      let index n l = match l with
        Nil                    -> failwith "index"
      | One (x, ps) when n = 0 -> x
      | One (x, ps)            -> Index.index (n - 1) (Zero ps)
      | Zero    ps             ->
        let (l, r) = Index.index (n / 2) ps in
        if n mod 2 = 0 then l else r
    end
  end in M.Index.index n v

(alas, local modules cannot be recursive). Now, in order to eliminate interference by the garbage collector, I predeclare my test data:

let data = range 1 1_000_000 ;;

I test each function for two seconds:

# test 2. (index1 999_999) data ;;
- : float = 1.45106870782848256e-05
# test 2. (index2 999_999) data ;;
- : float = 1.60240840297084448e-05
# test 2. (index3 999_999) data ;;
- : float = 1.91896990107750189e-05

The encoding using an object is 10% slower than the one using a record, which is to be expected as the open recursion is performed through a method table. On the other hand, the encoding using a recursive module is almost 25% slower than the one using a record, which is completely unexpected as I would believe the call to be statically resolved. Note also that there is no need to use a local module if the code is in a module bound by an abstract signature. All in all, this shows that these lists are extremely fast: It takes less than 15µs to find the last element in the list.