The n-ary cartesian product (on lists) returns the cartesian product of a list of list, rather than just two lists: product [[1]; [2;3]; [4;5]] is [[1;2;4]; [1;2;5]; [1;3;4]; [1;3;5]]. The result is the empty list as soon of one of the input lists is empty. But what is the product of the empty list of lists?

I first answered this question with mathematical considerations that, while working on set theory, will fell familiar to anyone having worked with dependent types. But there is a direct, much simpler answer in the code.

The motivation for this post was a bug report on the bugtracker of the Batteries library project, in which user wistery-k noticed the BatList.n_cartesian_product function incorrectly failed on empty lists.

A view from the theory

What is the n-ary cartesian product? In the result list of the product of [[1]; [2;3]; [4;5]], each list corresponds to a choice, in each of the input lists, of one element. For example the result list [1;3;4] corresponds to taking the only element of the first list, the second element of the second list, and the first element of the third list. All such possible choices of one element in each list is represented in the output.

To reason about this function, we should therefore model those element choices. A natural choice is to represent lists as families over a set of indices. For example, [3;4] could be modeled by a function from the parameter set {0,1} to the elements, mapping 0 to 3 and 1 to 4.

In order to prevent using an index into a list as an index into another list by mistake, we will rather use abstract sets of indices – the usual technique of type abstraction. We will designate the input lists by a parameter in an abstract index set, I, and each element of the i-th input list by an index in another abstract index set, J i. Notice that J is here an indexed family of index sets. Finally, to each pair of an index i in I (we’ll write i : I) in the outer list and j : J i in the i-th inner list corresponds an element elem i j (if we really see lists as functions from indices to elements, elem is just the input list of lists). All list elements have the same type A – a finer-grained choice would not help us here.

In this context, a “choice” of an element for each lists of the input can be represented as a function from the index (i : I) of a list to the index (in J i) of its chosen element: they live in the dependent function space (i : I) -> J i. The n-ary cartesian product is a list with one element for such a choice; in other terms, it is a list indexed by (i : I) -> J i taken as an index set. For each such choice function, we return a list of elements, one per list of the input list of lists, that a family of type I -> A.

Putting it all together: if we represent lists as indexed families, the n-ary cartesian product has the following type and formal implementation (I’m using parenthesis and braces interchangeably to make it easier to see the delimiter nesting).

product : ((i : I) -> {J i -> A})
       -> ({(i : I) -> J i} -> (I -> A))
product elem = (fun choice -> (fun i -> elem i (choice i))

We take a family over I of families over J of elements of type A (a list of lists), and return a family over choice functions (i:I) -> J i of families over I (a lists of lists).

This gives us a firm formal standing to understand the behavior of the n-ary cartesian product on lists. We can first check that it coincides with our intuition in two well-understood edge cases, namely the product of a list of singletons, and the product of a list of a single list. We’ll then see what this tells us of the n-ary product of no lists at all.

A singleton list can be modeled as being indexed by a singleton index set, which we will write {*} (* is an unnamed and un-interesting element). If we pass as input to product an I-indexed list of singleton, this means that each J i is {*}: we start from a value of type I -> ({*} -> A), and return a ({(I -> {*}) -> (I -> A). As there is only one function from I to {*}, that constantly returns *, there is only one possible choice, so our return list has to have only one element, which is indexed over I: it is the list of elements of our input singleton lists. product [[1]; [2]; [3]] is [1; 2; 3].

The motivated reader can check that the return type corresponding to a single input list, that is {*} -> (J * -> A), conversely tells us that we will get as return a J*-indexed list of singletons: product [[1;2;3]] is [[1]; [2]; [3]].

Finally, a product of no list should take an input with type (x : ∅) → ((j : J x) -> A), with one family J x for each element x of the empty set, that is no J families at all. Correspondingly, the return value should map choice functions (x : ∅) -> J x into lists of the form ∅ -> A. There is exactly one such choice function: it is a function whose graph is the empty set, that maps no element from its input type to elements of its output type (or, as a list of chosen indices, the empty list). And the list returned for this choice, of the form ∅ -> A, can only be the empty list. So product [] should return [[]].

A simpler counting argument

The length of the n-ary cartesian product is the product of the length of all input lists. Our example with input lists of sizes 1, 2 and 2 returned 4 lists as output. The length of the n-ary product of no lists should be the 0-ary product of sizes, namely the neutral element for multiplication, 1.

Finally, taking an empty 'a list list as input, there is only one way to return a value of type 'a list list that has one element: this element has to be the empty list [], so the complete result must be [[]] – enforced by parametricity.

(I’m not fond of those counting arguments, because they are fundamentally based on forgetting which kind of objects we’re really working with, studying only cardinality rather than the actual lists. This can often set our intuition on the right track, but can also be misleading in some edge cases where different fields would make different choices of simplifications, such as the much-debated question of how should exponentiation be extended to define 0^0.)

The view from the code

The buggy implementation was the following:

let rec n_cartesian_product = function
| [] -> assert false
| [l] -> (fun i -> [i]) l
| h :: t ->
    let rest = n_cartesian_product t in
      ( (fun i -> (fun r -> i :: r) rest) h)

A correct implementation (which was provided by wistery-k) should be of the following form:

let rec n_cartesian_product = function
| [] -> (* ? *)
| h :: t ->
    let rest = n_cartesian_product t in
      ( (fun i -> (fun r -> i :: r) rest) h)

The key point is that the value returned for [] should allow to express the former base case [l] as an instance of the general case h :: t. There is only one choice with this property, and it is [[]].

No theoretical considerations make as strong an argument as this one: the right answer is the one that makes the code elegant.