Cartesian product of arbitrarily many lists of different types

Question

Several similar questions have been asked and answered. One can find instances, for example:

1. Cartesian product of 2 lists in Haskell
2. Cartesian product over a list of lists in Haskell
3. How can I compute a Cartesian product iteratively?

However, neither of what I have found answered my question completely.

Question

In Haskell, is it possible and how to define a function cartesianProduct that takes arbitrarily (finitely) many lists of different types and outputs their cartesian product on the nose?

Background

For example, in the links above one can find a cartesianProd_2 that intakes two list of different types elegantly:

cartesianProd_2 :: [a] -> [b] -> [(a,b)]
cartesianProd_2 list_A list_B = [(x,y) | x<-list_A, y<-list_B]

One can easily generalizes this to cartesianProd_n, for some fixed integer n.

However, I hope I can define one that does

cartesianProd (list_1,list_2) == (cartesianProd_2 list_1 list_2)
cartesianProd (list_1,list_2,list_3) == (cartesianProd_3 list_1 list_2 list_3)

-- and so on .. notice that list_i is a list of elements of type i.

One immediate obstacle I encountered is that I don't even know what type of cartesianProd is! Its domain is a tuple of (lists of different types)! What should I do then?

Edit

If it is not possible in Haskell, please include a (pointer to a) proof.

Answer 1

If you are curious how to manipulate type-level data structures to solve the problem as stated, read on. If you have a practical problem to solve, skip all this nonsense and skip to the In Reality section.

This can be done. It takes a bit of type-level machinery to get us off the ground. Ideally I would like the following signature:

cartesianProduct :: Tuple (Map [] ts) -> [Tuple ts]

Here ts is a type-level list of types, and Map is a type-level version of map on lists. Tuple takes a list of types and gives a type which is equivalent to a tuple of those types. Let's say [Int, Char] for example, then this signature would reduce to:

cartesianProduct :: Tuple [ [Int], [Char] ] -> [Tuple [Int, Char]]
          -- morally, at least, equivalent to
                 :: ([Int], [Char]) -> [(Int, Char)]

Which hopefully you can see matches our intention. So let's get going:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, GADTs #-}

type family Map f xs where
    Map f '[] = '[]
    Map f (x ': xs) = f x ': Map f xs

data Tuple ts where
    Nil :: Tuple '[]
    Cons :: t -> Tuple ts -> Tuple (t ': ts)

This is using a number of advanced features. Type families, data kinds, and GADTs are the key words.

Ideally this should be enough:

cartesianProduct :: Tuple (Map [] ts) -> [Tuple ts]
cartesianProduct Nil = [Nil]
cartesianProduct (Cons xs xss) = [ Cons x ys | x <- xs, ys <- xss ]

Sadly, GHC can't figure it out

• Could not deduce: ts ~ (t0 : ts0)
  from the context: Map [] ts ~ (t : ts1)

It doesn't know that Map is injective¹ (even though it obviously is), so it can't figure out what ts should be when the input type is Tuple (Map [] ts) and the pattern is Nil. The technique here is to use a singleton, which is a type that helps the typechecker out of these situations.

data ListS ts where
    NilS :: ListS '[]
    ConsS :: ListS (t ': ts)

Notice that for a given list of types ts, there is only one possible ListS that could inhabit ListS ts (thus "singleton"). If we add this singleton as a parameter to our function, then the typechecker knows that, if the pattern is NilS then ts must be [] (and similarly for cons):

cartesianProduct :: ListS ts -> Tuple (Map [] ts) -> [Tuple ts]
cartesianProduct NilS Nil = [Nil]
cartesianProduct (ConsS s) (Cons xs xss) = [ Cons x ys | x <- xs, ys <- xss ]

Which passes the typechecker. Using it requires a bit of work:

example :: [Tuple '[Int, Char]]
example = cartesianProduct (ConsS (ConsS NilS)) (Cons [1,2] (Cons ['a','b'] Nil))

unTuple2 :: Tuple '[a,b] -> (a,b)
unTuple2 (Cons x (Cons y Nil)) = (x,y)

ghci> map unTuple2 example
[(1,'a'),(1,'b'),(2,'a'),(2,'b')]

It is a shame that we have to manually convert into a real tuple to see it working. But deriving a Show instance for Tuple is going to be another big hassle.

In Reality

However, the fact that we have to use unTuple* at the end of this madness, which knows precisely how many types we have, should be a hint that we should be able to do without, with a bit of a reframing of our problem. And indeed there is such a reframing, and that is the good ol' list applicative.

ghci> (,) <$> [1,2] <*> ['a','b']
[(1,'a'),(1,'b'),(2,'a'),(2,'b')]
ghci> (,,) <$> [1,2] <*> ['a','b'] <*> [True, False]
[(1,'a',True),(1,'a',False),(1,'b',True),(1,'b',False),(2,'a',True) (2,'a',False),(2,'b',True),(2,'b',False)]

Applicative notation works on arbitrarily many lists, as long as you can simultaneously provide an n-ary function to combine the elements (here the tupling functions (,) and (,,) play that role, but it could be any function, e.g. (\x y -> x + 2*y) <$> [1,2] <*> [3,4]). And in practice, this is almost certainly the way a problem requiring n-ary heterogenous cartesian products would be solved. The type-level fanciness discussed in this answer is seldom required and often just makes things unnecessarily complicated.

---

¹I attempted a new injectivity annotation to fix this

type family Map f xs = r | r -> xs where
    Map f '[] = '[]
    Map f (x ': xs) = f x ': Map f xs

But it was no help. Seems like it should have worked.