The limits of Hindley-Milner

The simplest thing in the world. Concatenate two pairs of lists component-wise:

# fun (a, x) (b, y) -> (a @ b, x @ y) ;;
- : 'a list * 'b list -> 'a list * 'b list -> 'a list * 'b list = <fun>

Why, let's abstract out the concatenation part and call it thread, so that it lifts a binary function to operate on pairs component-wise:

# let thread f (a, x) (b, y) = (f a b, f x y) ;;
val thread : ('a -> 'b -> 'c) -> 'a * 'a -> 'b * 'b -> 'c * 'c = <fun>

Aaaaaargh! Hindley-Milner doesn't let f to have different types in different application sites, so it forces both components of each pair to be equal. I'd wish at least for thread to have the type

val thread : ('a . 'a -> 'a -> 'a) -> 'a * 'b -> 'a * 'b -> 'a * 'b

Is there any way to do this with polymorphic records?

Ring Laws

This is a really basic derivation of elementary facts about rings, just for the record. I follow Milne's definition of a ring (R, +, 0, -, ⋅ 1) as a commutative group (R, +, 0, -) equipped with an additional operation ⋅ and a distinguished 1 ∈ R such that (R, ⋅, 1) is a monoid, and ⋅ distributes over + both on the left and on the right: for all a, b, c ∈ R

(a + b)⋅c = a⋅c + b⋅c
a⋅(b + c) = a⋅b + a⋅c

Lemma for any a, b ∈ R, a⋅0 = 0 = 0⋅b

   a⋅0 = 0
⇐ { Cancellation on the left }
   a⋅b + a⋅0 = a⋅b + 0
≡ { Distributivity on the right }
   a⋅(b + 0) = a⋅b + 0
≡ { Group neutral, twice }
   a⋅b = a⋅b
≡
   true

The other direction is analogous:

   0⋅b = 0
⇐ { Cancellation on the right }
   0⋅b + a⋅b = 0 + a⋅b
≡ { Distributivity on the right }
   (0 + a)⋅b = 0 + a⋅b
≡ { Group neutral, twice }
   a⋅b = a⋅b
≡
   true

Theorem for any a, b ∈ R, (-a)⋅b = -(a⋅b) = a⋅(-b)

   (-a)⋅b = -(a⋅b)
⇐ { Cancellation on the right }
   (-a)⋅b + a⋅b = -(a⋅b) + a⋅b
≡ { Distributivity on the right, group inverse }
   (-a + a)⋅b = 0
≡ { Group inverse }
   0⋅b = 0
≡ { Lemma }
   true

The other direction is analogous:

   a⋅(-b) = -(a⋅b)
⇐ { Cancellation on the left }
   a⋅b + a⋅(-b) = a⋅b + -(a⋅b)
≡ { Distributivity on the left, group inverse }
   a⋅(b + -b) = 0
≡ { Group inverse }
   a⋅0 = 0
≡ { Lemma }
   true

Also, the following is immediate:

Theorem If 1 = 0, then R = {0}

Proof: note that, for arbitrary a, b ∈ R:

   a
= { Definition }
   a⋅1
= { Hypothesis }
   a⋅0
= { Lemma }
   0
= { Lemma }
   0⋅b
= { Hypothesis }
   1⋅b
= { Definition }
   b

which shows that there is at most one element in R.

Proof-directed Debugging: A Real Example

I was reading this excellent introduction to the K programming language (go ahead, get immersed into it. I'll wait for you) when I got piqued by the strange function where:

  &1 2 3 4     / where: returns the number of units specified
0 1 1 2 2 2 3 3 3 3

  &0 1 1 0 0 1 / where: an important use to get the indices of the 1s
1 2 5

Beyond the need (or not) for such a function, my immediate thought was, How would I write that in OCaml? Sadly, it seems I've become monolingual enough that I have to translate most of what I "hear" into my own internal language. The complaint is neither here nor there, the point is that I reasoned pretty operationally: "I have 1 zeroes, 2 ones, 3 twos and 4 threes", hence:

let where l =
  let rec go n l = function
  | []      -> l
  | x :: xs -> go (succ n) (rep_append x n l) xs

where n is the index of the current element x, and rep_append appends a list of x repeated n times onto l:

  and rep_append e n l =
    if n == 0 then l else
    rep_append e (pred n) (e :: l)
  in
  List.rev (go 0 [] l)

with an accumulating parameter tacked in by tail-recursive reflex. I smelled something wrong when the compiler told me that:

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

"Polymorphic?" I thought, and I tried:

# where [1;2;3;4] ;;
- : int list = [2; 3; 3; 4; 4; 4]

Yes, wrong, but…

Of course, I didn't debug the function: the type was too wrong, and it was too obvious a clue that I needed look no further than go. Type-checking by hand, I saw that, at the end, the returned list has type α list; that must be because rep_append returns an α list. Type-checking that, its result type is α list because it appends e to an α list, so that e must have type α instead of int. That variable takes the value from x, the head of the argument list, but that is the number of times to repeat n, that very element's index.

The arguments are swapped: I wrote above rep_append appends a list of x repeated n times, when I should've written rep_append appends a list of n repeated x times. The correct function is:

let where l =
  let rec go n l = function
  | []      -> l
  | x :: xs -> go (succ n) (rep_append n x l) xs
  and rep_append e n l =
    if n == 0 then l else
    rep_append e (pred n) (e :: l)
  in
  List.rev (go 0 [] l)

(the difference is in go's call to rep_append) whose type:

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

is satisfactory. The function works correctly, too, but that was to be expected.

This is a typical example of proof-directed debugging. That is, a concrete answer to the question, What good is a strong statically-typed language? It's not only that the types prevent you from connecting the pieces together when they don't fit, even though that's 90% of their usefulness. It is also, and especially, the fact that the type of a function is a proof that it does what you think it does. If the type is wrong, the function must be wrong too, automatically, and you don't need to run it to know that.

Much as with a real proof, the trick is to work backwards to see where did an error creep in. A classical example are the trick "proofs" that purport to demonstrate that 1 = -1 or some such, "proofs" that crucially depend on dividing by zero. Working mathematicians everywhere are confronted daily with this, and therein lies the rub.

A crucial objection to the discipline of programming with a strong, statically-typed language is the view that "you need a degree in Mathematics to program in it". It is often repeated that it is "more productive" (easier, in non-obfuscated terms) to program in a dynamic language, and to debug in run-time, or using test-driven development.

The pragmatics of using a statically-typed language are not as onerous as that might suggest. Unfortunately you really have to try it for yourself to see that (but the same is true of the extreme and agile methodologies.) It looks difficult, and it is difficult to program with a strict type system if you're not used to it. But, and this is important, the best languages (i.e., not Java) lend you a very helpful hand: you don't have to prove any theorems, because the compiler does it for you. I checked a proof, I didn't have to write one. That's the compiler's job. And this particular check, that every term has a given type, is not very difficult once you have the final term; you just have to acquire the knack of working back the types of everything until you get to the source.

So, don't just take my word for it, give it a spin. You'll just have to trust me in that strong statically-typed languages are an effective alternative to TDD and agile methodologies.

By the way, that function is ridiculously operational. What would SPJ do? Easy: just be lazy!:

let where l = concat % map (fun (i, x) -> take x $ all i) % index $ l

That is (from right to left): index the list's elements; convert each pair of an index and a repetition count into the corresponding list, and flatten the result. Of course, this requires a couple of definitions:

let (%) f g x = f (g x)

let ($) f x = f x

let rec iota =
  let rec go l i =
    if i == 0 then l else
    let i = pred i in
    go (i :: l) i
  in go []

let all e = let rec l = e :: l in l

let rec take n l =
  if n == 0 then [] else
  match l with
  | []      -> []
  | x :: xs -> x :: take (pred n) xs

let index l = combine (iota (length l)) l

all but the last of which are entirely general. This goes to show that the Haskeller's smug remark that OCaml's standard prelude is rather poor is not really smug at all but painfully true.

Edit: Aaaaargh! I made the same mistake twice. It's obvious that I can't think and code at the same time. The second version of the function where is now correct.

Stream of Consciousness

Wouldn't you like to write code like this:

reading "ebooks/345.txt" (
   lines
|> skip_until (matches "^\\*\\*\\* START OF")
|> skip
|> filter is_empty
|> words
|> fmap String.uppercase
|> take 20
|> to_list
)

and have it spit:

- : string list =
["DRACULA"; "BY"; "BRAM"; "STOKER"; "1897"; "EDITION"; "TABLE"; "OF";
 "CONTENTS"; "CHAPTER"; "1"; "JONATHAN"; "HARKER'S"; "JOURNAL"; "2";
 "JONATHAN"; "HARKER'S"; "JOURNAL"; "3"; "JONATHAN"]

(yes, it's the Project Gutemberg ebook for Bram Stoker's Dracula, text version; a suitably large corpus to run tests with). That would read: "Safely open the named file as input; parse it into lines, skip until finding the line that matches the regular expression; skip that line. Avoid empty lines, and split the remainder into words. Change the words to upper case, and take the first twenty and make a list of those." Well, this can be done with very nice code. But first, I'd like to do away with the somewhat "normal" bits.

Regular expressions in OCaml live in the Str module; they're low-level and inconvenient to use. A little wrapping-up makes them more palatable:

let matches patt =
  let re = Str.regexp patt in
  fun str -> Str.string_match re str 0

Note that I close over the compilation of the regular expression, so that repeated calls to matches with the same regexp don't waste effort. Of course, is_empty is simply:

let is_empty = matches "^[\t ]*$"

The mysterious "piping arrow" is nothing more than function composition in disguise:

let (|>) f g x = g (f x)

This is the reverse (or categorical) composition; its more popular sibling (one could say, its twin) is:

let (%) f g x = f (g x)

The magic sauce in the program is the use of OCaml's imperative streams. They are like lists, but with a lazy tail which is accessed by destructively taking the head. Like lazy lists, they allow for computation with infinite data, and they use just as much as they need. Unlike lazy lists, they don't support persistence, that is, the ability to keep reference to arbitrary versions of a value. For stream processing of text files they're a perfect match. The idea is to work with functions from streams to streams, or stream transformers. This is made very pleasing by the CamlP4 syntax extension for streams and stream parsers. To use it, you must compile your code with camlc -pp camlp4o, or #load "camlp4o.cma" (or #camlp4o if you're using findlib) in your source file, as explained in the manual.

By far the simplest transformer is the one that skips the head of a stream, and returns the (now headless) result:

let skip str = match str with parser
| [< '_ >] ->  str
| [< >]    -> [< >]

Here the single quote indicates that we're talking about a concrete stream element, as opposed to a substream. It's natural to extend this to a transformer that keeps dropping elements as long as they satisfy a test or predicate p:

let rec skip_while p str = match str with parser
| [< 'x when p x >] -> skip_while p str
| [< >]             -> str

This is the first pattern common to all transformers: return the passed in stream once we're done consuming, or chopping off, elements at its head. This is signalled by the use of the empty pattern [< >] which matches any stream. Of course the opposite filter is also handy and comes for free:

let skip_until p = skip_while (not % p)

We now know how skip_until (matches "^\\*\\*\\* START OF") |> skip works. A variation in the beheading game is to drop a number of elements from the stream:

let rec drop n str = match str with parser
| [< '_ when n > 0 >] -> drop (pred n) str
| [< >]               -> str

(note that this function is purposefully partial). The converse is to take a finite number of elements from a stream:

let rec take n str = match str with parser
| [< 'x when n > 0 >] -> [< 'x; take (pred n) str >]
| [< >]               -> [< >]

(note that this function is also purposefully partial). This is the second pattern common to all transformers: insert a substream on the right side of a matching by recursively invoking the transformer. Similar to this code is the filtering of a stream to weed out the elements satisfying a predicate:

let rec filter p str = match str with parser
| [< 'x when p x >] ->        filter p str
| [< 'x          >] -> [< 'x; filter p str >]
| [< >]             -> [< >]

The fact that in the first matching the recursive call to filter is outside a stream bracket pair means that it will eagerly call itself recursively until it finds an element not matching the predicate.

It's not too difficult to devise a fold over the elements of a stream:

let rec fold f e str = match str with parser
| [< 'x >] -> fold f (f e x) str
| [<    >] -> e

Of course, infinite streams cannot be folded over in finite time, but that's to be expected. This lets me write useful operations in a really concise way:

let length str = fold (fun n _ -> succ n) 0 str

let to_list str = List.rev (fold (fun l x -> x :: l) [] str)

With this, a pipeline like skip_until (matches "^\\*\\*\\* START OF") |> skip |> filter is_empty |> take 20 |> to_list just works, if only we had something to feed it. It could be handy to zip two streams together. Unfortunately, I can find no straightforward way to synchronize the advance of both streams, as there isn't a parallel match of two stream parsers. If you run camlp4o on a file containing the definitions so far, you'll see that the syntax gets rewritten (or expanded) to direct OCaml code that calls into the functions marked For system use only, not for the casual user in stream.mli. It is possible to emulate the result of a hypothetical stream parser doing the zipping by writing directly:

let rec zip str str' =
  match Stream.peek str, Stream.peek str' with
  | Some x, Some y ->
    Stream.junk str;
    Stream.junk str';
    Stream.icons (x, y) (Stream.slazy (fun () -> zip str str'))
  | _  -> Stream.sempty

With a simple stream like:

let nat () = Stream.from (fun i -> Some i)

(why is it a function? Also, note Conal Elliot's remark in his recent post about streams being functions over the natural numbers), a transformer for numbering a stream is as easy as (nat |> zip) (). Another way to build streams is to use the syntax:

let rec repeat e = [< 'e; repeat e >]

Stream expressions are not only used in parsers, as the right hand side of the matchings in the preceding functions hint at. This is possibly the simplest infinite stream you can have.

As it is well-known to Haskellers, streams have algebraic and categorical structure. For instance, they are functors; in other words, they can be mapped over their elements with a function that transforms them pointwise:

let rec fmap f str = match str with parser
| [< 'x >] -> [< 'f x; fmap f str >]
| [<    >] -> [< >]

In this case, the call to f is lazy, and not performed until the head of the resulting stream is requested. This can be good or not; for a strict evaluation of the head, a let binding must be used.

Streams also form a monad, entirely analogous to the list monad. The unit simply returns the one-element stream:

let return x = [< 'x >]

The bind concatenates the streams resulting from the application of a function to the each element in turn:

let rec bind str f = match str with parser
| [< 'x >] -> [< f x; bind str f >]
| [<    >] -> [< >]

Note that the difference between fmap and bind is a single quote! This is a direct consequence of the fact that every monad is a functor, via the identity fmap f x = bind x (return . f). Now words is straightforward:

let words =
  let re = Str.regexp "[\n\t ]+" in fun str ->
  bind str (Str.split re  |>  Stream.of_list)

It only remains one last piece of the puzzle: how does an input channel get transformed into a stream of lines? With a transformer (a parser, actually), of course. This is a rather simple one (especially compared to the imperative monstrosity it replaced; you don't want to know), once you dissect it into its components:

let lines =
  let buf = Buffer.create 10 in
  let get () = let s = Buffer.contents buf in Buffer.clear buf; s
  in
  let islf = parser
  | [< ''\n' >] -> ()
  | [< >]       -> ()
  in
  let rec read str = match str with parser
  | [< ''\n' >] ->           [< 'get (); read str >]
  | [< ''\r' >] -> islf str; [< 'get (); read str >]
  | [< 'c    >] -> Buffer.add_char buf c; read str
  | [<       >] -> [< >]
  in read

The characters in a line are accumulated in the buf buffer. Once a line is complete, get resets the buffer and returns its contents. The sub-parser islf tries to eat the LF in a CRLF pair. Since it includes an empty match, it cannot fail. The recursive parser read scans for a LF, or for a CR or CRLF terminator, accumulating characters until a complete line is included in the result stream. Invoking islf it in the right-hand side of the CR match in read is safe, in the sense that it cannot lead to back-tracking.

At last we get to the point where we can read from a file. For that Stream.of_channel directly and efficiently turns the contents of a file into a stream of characters:

let reading file k =
  let inch = open_in_bin file in
  try
    let res = k (Stream.of_channel inch) in
    close_in inch; res
  with e -> close_in inch; raise e

where k is the continuation that is safely wrapped in an exception handler that closes the file even in the event of an error. Safe input-output in the face of exceptions is an idiom borrowed from LISP, the well-known WITH-OPEN-FILE.

You could find various ways to exercise this small DSL; by way of example, a word count:

reading "ebooks/345.txt" (
   lines
|> skip_until (matches "^\\*\\*\\* START OF")
|> skip
|> filter is_empty
|> words
|> length
)
- : int = 163718

Numbering the first lines in the book:

reading "ebooks/345.txt" (
   lines
|> skip_until (matches "^\\*\\*\\* START OF")
|> skip
|> filter is_empty
|> fmap String.uppercase
|> zip (nat ())
|> take 10
|> to_list
)
- : (int * string) list =
[(0, "DRACULA"); (1, "BY"); (2, "BRAM STOKER"); (3, "1897 EDITION");
 (4, "TABLE OF CONTENTS"); (5, "CHAPTER");
 (6, "  1  JONATHAN HARKER'S JOURNAL");
 (7, "  2  JONATHAN HARKER'S JOURNAL");
 (8, "  3  JONATHAN HARKER'S JOURNAL");
 (9, "  4  JONATHAN HARKER'S JOURNAL")]

Which of course is not very accurate, as the first line should be numbered 1, not 0, and the line numbers don't correspond to the text but to the filtered stream. Let's try something else: define the arrow parts of the pair projection functions:

let first  f (x, y) = (f x, y)
and second g (x, y) = (x, g y)

Now, number the lines as read, and then apply the processing to the second component of the paired-up lines:

reading "ebooks/345.txt" (
   lines
|> zip (nat ())
|> skip_until (snd |> matches "^\\*\\*\\* START OF")
|> skip
|> filter (snd |> is_empty)
|> (fmap % second) String.uppercase
|> take 10
|> to_list
)
- : (int * string) list =
[(34, "DRACULA"); (36, "BY"); (38, "BRAM STOKER"); (41, "1897 EDITION");
 (46, "TABLE OF CONTENTS"); (49, "CHAPTER");
 (51, "  1  JONATHAN HARKER'S JOURNAL");
 (52, "  2  JONATHAN HARKER'S JOURNAL");
 (53, "  3  JONATHAN HARKER'S JOURNAL");
 (54, "  4  JONATHAN HARKER'S JOURNAL")]

I hope this helps in reducing Haskell envy a little bit.

(One Flew Over The) Cuckoo's Hash

In a conversation over reddit, reader nostrademons suggested Cuckoo Hashing as a hash scheme with constant-time worst-case look-ups. References to the algorithm abound, but implementations are scarce, so I set out to write code. It turned out to be more difficult than I anticipated.

The original article describing Cuckoo Hashing explains the basic scheme better than the Wikipedia article does, in my opinion. It uses, however, two hash tables with probes going first to one and then to the other. A later article by the inventor shows a simpler scheme with only one key space. This paper is straightforward, and I set out to write code under its specifications. Instead of a hash map I preferred writing a hash set; it is possible to build the former with the latter storing key-value pairs.

This requires parameterizing the hash table with not only a data type but with an equality predicate and a hash function over that type; in effect this makes the hash table not polymorphic but an existential type, witnessed by those functions:

type 'a hash = {
  equals  : 'a -> 'a -> bool;
  hash    : 'a -> int;
  mutable index : int;
  mutable count : int;
  mutable table : 'a option array;
}

Of index I will say more later, but count is the number of elements stored in table, where the presence or absence of an element at a given position is given by the use of an option. Thanks to one of the (few) strange corners of OCaml's type system I can make both parameters optional by relying on the polymorphic equality and hash functions built-in to the standard library:

let create ?(equals=(=)) ?(hash=Hashtbl.hash) size =
  { equals = equals; hash = hash; index = 1; count = 0; table = Array.make size None }

Note that create and not make is the builder function name in the standard module Hashtbl. The easy part of implementing a hash table are the administrative functions dealing with the specifics of an imperative data type. Clearing a table is very simple:

let clear h =
  h.index <- 1;
  h.count <- 0;
  Array.fill h.table 0 (Array.length h.table) None

And simpler still is to copy a table into another:

let copy h =
  { h with table = Array.copy h.table }

Iterating over the elements in the table is also straightforward:

let iter f h =
  Array.iter (function Some w -> f w | _ -> ()) h.table

With that, a left fold is equally natural:

let fold f e h =
  let res = ref e in
  iter (fun w -> res := f !res w) h;
  !res

The number of elements stored in the table is given by:

let length h = h.count

Again, the name copies the one given to the analogous function in Hashtbl. What about that index lurking in the table? To explain it, I must take a detour.

Hashing is hard

The second paper by Pagh I linked to above assumes that:

We have access to hash functions h₁ and h₂ such that any function value h_i(x) is equal to a particular value in {1, …, r} with probability 1/r, and the function values are independent of each other […] Note that this is only possible if hash functions are somehow chosen in a random fashion. However, in this lecture note we will not describe how to do this.

And herein lies the first rub. How to choose two functions at random? The first paper speaks of a universal family of hash functions, which is no more and no less than a set of functions indexed by some mechanism with the property that the results of each member in the family is independent of each other. I couldn't find much data about how to build such a family, but I wasn't too diligent about it. What I did find was that cryptographic hashes are a good approximation to a universal family when keyed by the index.

A suitable index is readily available as the i for each of the two probes into the Cuckoo table. Independent of this, I had read about a new cryptographic hash family by Schneier et al., the Skein hash. What struck me about it is that it uses a really simple Feistel network to build the mixing rounds:

let ror i x = (x lsr (31 - i)) lor (x lsl i)

let round r (x, y) = let s = x + y in s, s lxor (ror r y)

With some fudging of the values given in that paper, I built a 4-round shuffle:

let shuffle k x = snd (round 22 (round 19 (round 30 (round 7 (k, x)))))

Now each of the two hashes would be keyed by a "random" number and fed to the shuffle:

let keys  = [| 599290962; 771645345 |]

(If you look up those numbers, you'll see they're not that random, and they have something to do with the largest prime 2³⁰ - 35 that fits in an OCaml 31-bit machine integer). With that, the indexed hash looks like this:

let hash i h x =
  let p = h.hash x in
  let q = shuffle keys.(i) p in
  let r = (p + h.index * q)  land  0x3fffffff in
  r mod Array.length h.table

And again, what's with the index? Well, there's another rub in Pagh's papers, of which I will say more later on; suffice to say that it serves as a way to build a double hash (indeed, multiple) in the case that insertion fails. This results in a multi-parametric hash family h(k, j, i), where k is the key, j is the index or hashing "round", and i selects one of both Cuckoo hashes.

I tested these hash functions for collisions with a smallish dictionary of words and found it satisfactory. I haven't found a simple, certified implementation of a hash family, and the few references that I've looked up were vague and inconclusive, or relied heavily on strong cryptographic primitives. This is the first failure of Pagh's "algorithm", in that it is under-specified. This hash might fail to fulfill the paper's preconditions as I quoted above, and so this code is not fit for productive usage!

The good: deletions

The surprise came when I had to implement deletion from the table. When I wrote on reddit, I was under the impression that it would need lazy deletion to skip over deleted entries. This turned out to be false, as I found by implementing the table with a variant type denoting both empty and missing slots, and seeing that both paths were identical. Further thought convinced me that, indeed, insert below does not inspect slots, and so there is no need to mark them as deleted as opposed to simply empty. So, the following code, even if not shown in the paper, posed no problem:

let remove h v =
  try for i = 0 to 1 do
    let x = hash i h v in
    match h.table.(x) with
    | Some w when h.equals v w ->
      h.table.(x) <- None; raise Exit
    | _ -> ()
  done with Exit -> ()

As you will see, it is exactly analogous to the look-up below.

The ugly: look-ups

The raison d'être of the Cuckoo scheme is constant-time lookup:

let mem h v =
  try for i = 0 to 1 do
    let x = hash i h v in
    match h.table.(x) with
    | Some w when h.equals v w -> raise Exit
    | _ -> ()
  done; false with Exit -> true

This tries twice to find the element v, first by hashing it with hash 0, then with hash 1. By the postcondition of insertion, it is guaranteed that, if not found in two tries the key is simply not stored in the table. The code looks needlessly imperative, with an exception replacing a short-circuiting or, but it is symmetrical to that for deletion above, and what you would write with imperative loops and breaks. Now for the last hurdle.

The bad: insertions

Pagh shows how to perform the basic shuffle of elements around the table so that the two-probe look-up succeeds. What he doesn't show is how to grow the table, or what to do if insertion finds a loop in the random graph induced by the hashes. He glosses over this with:

This is continued until the procedure finds a vacant position or has taken too long. In the latter case, new hash functions are chosen, and the whole data structure is rebuilt ("rehashed") … In this case the insertion procedure will loop n times before it gives up and the data structure is rebuilt ("rehashed") with new, hopefully better, hash functions.

(emphasis mine). This is where I started looking for implementations, to see how they resolved this oversight. I found none, and so here's my attempt. If the hash function above is good (random) enough, this procedure terminates; as I can't guarantee that the hash I've given above is universal, this function can very well fail, although with an out-of-memory exception and not an infinite loop. Caveat emptor!

First, I'll bound the number of attempts at rehashing with a new set of hash functions before giving up and growing the table:

let add h v =
  let attempts = ref 0 in

I use an auxiliary function go; insert is a wrapper for it that gets it started with an initial hash value and a number of attempts equal to the size of the table:

  let rec insert v =
    go (Array.length h.table) (hash 0 h v) v

This function go takes the number n of attempts left, the current index pos and the value v to insert. If there aren't any more attempts left, there's no other choice than to rehash and try again to insert the value that failed. Otherwise, the current slot's content gets exchanged with the value to be inserted, and the old value, if any, is inserted recursively with the first hash that changes its position:

  and go n pos v =
    if n = 0 then begin rehash h; insert v end else
    let x = h.table.(pos) in
    h.table.(pos) <- Some v;
    match x with
    | None   -> ()
    | Some w ->
      let j = hash 0 h w in
      go (pred n) (if pos = j then hash 1 h w else j) w

This is essentially the inner loop of the algorithm insert given in the paper. It is now necessary to flesh out the mysterious rehash.

The first paper analyzes the algorithm in depth, and it shows that, given that the hashes are universal and independent, a fill factor of less than 0.5 implies that the probability of a cycle is less than the number of entries in the table, and so by the pigeonhole it cannot happen. To account for the imperfect universality of the hashes, I try at most 5 attempts at rehashing, with successively higher values of index. I've found empirically that odd values of the multiplier work best. If the maximum number of attempts is reached, or the table is over-full, I simply double its size. Then, I iterate over the old table, successively inserting the found values in the new.

  and rehash h =
    let table  = h.table in
    let length = Array.length table in
    let size   =
      if !attempts < 5 && 2 * h.count < length
      then begin
        h.index <- h.index + 2;
        incr attempts;
        length
      end else begin
        attempts := 0;
        2 * length
      end in
    h.table <- Array.make size None;
    Array.iter (function Some v -> insert v | _ -> ()) table

It is here that a pathologically bad hash family could lead to problems: insert calls rehash that calls insert that could call rehash again that… Here the procedure would double the table again and again, until it exceeds the limits of OCaml arrays. With that, the insertion is carried out if the entry is not already present in the table:

  in if not (mem h v) then begin
    insert v;
    h.count <- h.count + 1
  end

As you can see, the correctness of the algorithm relies on the statistical properties of the hash family, which in my view is a flimsier foundation than linear chaining. This makes the latter attractive in the presence of hash functions of arbitrary, and not always good, quality: at worst you have an O(n) look-up, instead of non-termination.

Trying it out

This said, the code works surprisingly well. To test it, I've found a list of the 500 most frequent English words:

let words = [
"the";"of";"to";"and";"a";"in";"is";"it";"you";"that";
"he";"was";"for";"on";"are";"with";"as";"I";"his";"they";
"be";"at";"one";"have";"this";"from";"or";"had";"by";"not";
"but";"some";"what";"there";"we";"can";"out";"other";"were";"all";
"your";"when";"up";"use";"word";"how";"said";"an";"each";"she";
"which";"do";"their";"time";"if";"will";"way";"about";"many";"then";
"them";"would";"write";"like";"so";"these";"her";"long";"make";"thing";
"see";"him";"two";"has";"look";"more";"day";"could";"go";"come";
"did";"my";"sound";"no";"most";"number";"who";"over";"know";"water";
"than";"call";"first";"people";"may";"down";"side";"been";"now";"find";
"any";"new";"work";"part";"take";"get";"place";"made";"live";"where";
"after";"back";"little";"only";"round";"man";"year";"came";"show";"every";
"good";"me";"give";"our";"under";"name";"very";"through";"just";"form";
"much";"great";"think";"say";"help";"low";"line";"before";"turn";"cause";
"same";"mean";"differ";"move";"right";"boy";"old";"too";"does";"tell";
"sentence";"set";"three";"want";"air";"well";"also";"play";"small";"end";
"put";"home";"read";"hand";"port";"large";"spell";"add";"even";"land";
"here";"must";"big";"high";"such";"follow";"act";"why";"ask";"men";
"change";"went";"light";"kind";"off";"need";"house";"picture";"try";"us";
"again";"animal";"point";"mother";"world";"near";"build";"self";"earth";"father";
"head";"stand";"own";"page";"should";"country";"found";"answer";"school";"grow";
"study";"still";"learn";"plant";"cover";"food";"sun";"four";"thought";"let";
"keep";"eye";"never";"last";"door";"between";"city";"tree";"cross";"since";
"hard";"start";"might";"story";"saw";"far";"sea";"draw";"left";"late";
"run";"don't";"while";"press";"close";"night";"real";"life";"few";"stop";
"open";"seem";"together";"next";"white";"children";"begin";"got";"walk";"example";
"ease";"paper";"often";"always";"music";"those";"both";"mark";"book";"letter";
"until";"mile";"river";"car";"feet";"care";"second";"group";"carry";"took";
"rain";"eat";"room";"friend";"began";"idea";"fish";"mountain";"north";"once";
"base";"hear";"horse";"cut";"sure";"watch";"color";"face";"wood";"main";
"enough";"plain";"girl";"usual";"young";"ready";"above";"ever";"red";"list";
"though";"feel";"talk";"bird";"soon";"body";"dog";"family";"direct";"pose";
"leave";"song";"measure";"state";"product";"black";"short";"numeral";"class";"wind";
"question";"happen";"complete";"ship";"area";"half";"rock";"order";"fire";"south";
"problem";"piece";"told";"knew";"pass";"farm";"top";"whole";"king";"size";
"heard";"best";"hour";"better";"true";"during";"hundred";"am";"remember";"step";
"early";"hold";"west";"ground";"interest";"reach";"fast";"five";"sing";"listen";
"six";"table";"travel";"less";"morning";"ten";"simple";"several";"vowel";"toward";
"war";"lay";"against";"pattern";"slow";"center";"love";"person";"money";"serve";
"appear";"road";"map";"science";"rule";"govern";"pull";"cold";"notice";"voice";
"fall";"power";"town";"fine";"certain";"fly";"unit";"lead";"cry";"dark";
"machine";"note";"wait";"plan";"figure";"star";"box";"noun";"field";"rest";
"correct";"able";"pound";"done";"beauty";"drive";"stood";"contain";"front";"teach";
"week";"final";"gave";"green";"oh";"quick";"develop";"sleep";"warm";"free";
"minute";"strong";"special";"mind";"behind";"clear";"tail";"produce";"fact";"street";
"inch";"lot";"nothing";"course";"stay";"wheel";"full";"force";"blue";"object";
"decide";"surface";"deep";"moon";"island";"foot";"yet";"busy";"test";"record";
"boat";"common";"gold";"possible";"plane";"age";"dry";"wonder";"laugh";"thousand";
"ago";"ran";"check";"game";"shape";"yes";"hot";"miss";"brought";"heat";
"snow";"bed";"bring";"sit";"perhaps";"fill";"east";"weight";"language";"among";
]

One possibility is to preallocate enough space for them so as to avoid growing the table:

# let h = create 1000 ;;
val h : '_a hash =
  {equals = <fun>; hash = <fun>; index = 1; count = 0;
   table =
    [|None; None; None; None; None; None; None; None; None; None; None; None;
      None; None; None; None; None; None; ...|]}
# List.iter (add h) words ;;
- : unit = ()
# Array.length h.table ;;
- : int = 1000
# h.index ;;
- : int = 1

This shows that it never needed a rehash. The other possibility is to start small, and let the algorithm grow as needed:

# let h = create 16 ;;
val h : '_a hash =
  {equals = <fun>; hash = <fun>; index = 1; count = 0;
   table =
    [|None; None; None; None; None; None; None; None; None; None; None; None;
      None; None; None; None|]}
# List.iter (add h) words ;;
- : unit = ()
# Array.length h.table ;;
- : int = 1024
# h.index ;;
- : int = 3

Now, both rehashing and growing were necessary. Of course, the table does contain the entries:

# length h ;;
- : int = 500
# List.filter (not % mem h) words ;;
- : string list = []

Acknowledgements: to nostrademons that, as I've come to expect from reddit users, made me think more and harder than I would otherwise had.