## On the n-ary cartesian product

- February 23, 2013

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] -> List.map (fun i -> [i]) l
| h :: t ->
let rest = n_cartesian_product t in
List.concat
(List.map (fun i -> List.map (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
List.concat
(List.map (fun i -> List.map (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*.