# Enumerating Permutations

by Phil Freeman on 2011/12/28

Consider the following Haskell function which enumerates permutations of a given length:

``````{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}

import Data.List

perms 0 = [[]]
perms n = [ insertAt i n p | p <- perms (n - 1), i <- [0..n-1] ]

insertAt 0 x xs = x:xs
insertAt n x (x':xs) = x':xs' where xs' = insertAt (n - 1) x xs
``````

The goal of this post is to derive a partial inverse `indexOfPerm` to the indexing function `perms n !!` as an exercise in equational reasoning in Haskell. That is, we seek a function such that for all `i`:

``````-- indexOfPerm :: Int -> [Int] -> Int
-- indexOfPerm n (perms n !! i) = i
``````

This will serve as a specification of the function `indexOfPerm`.

Expanding the definition of perms at zero gives the following:

``````-- indexOfPerm 0 []
--   { Definition of perms }
--   = indexOfPerm 0 (perms 0 !! 0)
--   { By assumption }
--   = 0
``````

Expanding the recursive definition of `perms` gives the following:

``````-- indexOfPerm n (perms n !! (j * n + k))
--  { Definition of perms }
--  = indexOfPerm n (insertAt j n (perms (n - 1) !! k))
--  { Let xs = insertAt j n (perms (n - 1) !! k) }
--  = indexOfPerm n xs
--  { By assumption }
--  = j * n + k
``````

Suppose we can find a function `extract` which satisfies the following:

``````-- extract :: Int -> [Int] -> (Int, [Int])
-- extract n (insertAt i n xs) = (i, xs)
``````

Now calculate as follows:

``````-- extract n xs
--   { Definition of xs }
--   = extract n (insertAt j n (perms (n - 1) !! k) )
--   { Definition of extract }
--   = (j, perms (n - 1) !! k)
--   { Let xs' = perms (n - 1) !! k) }
--     so that k = indexOfPerm (n - 1) xs' }
--   = (j, xs')
--
-- indexOfPerm n xs
--   { From earlier }
--   = j * n + k
--   { Expressing k in terms of xs' }
--   = j * n + indexOfPerm (n - 1) xs'
``````

We can now define `indexOfPerm` as follows:

``````indexOfPerm 0 [] = 0
indexOfPerm n xs = n * (indexOfPerm (n - 1) xs') + j
where (j, xs') = extract n xs
``````

It remains to compute the function `extract`. Expanding the definition of `insertAt` at zero gives:

``````-- extract x (x:xs)
--   { Definition of insertAt }
--   = extract x (insertAt 0 xs)
--   { By assumption }
--   = (0, xs)
``````

Expanding the recursive definition of `insertAt` gives:

``````-- extract x (x':xs)
--   { Assume xs = insertAt i x xs'
--     so that (i, xs') = extract x xs }
--   = extract x (x':insertAt i x xs')
--   { Definition of insertAt }
--   = extract x (insertAt (i + 1) x x':xs'))
--   { By assumption }
--   = (i + 1, x':xs')
``````

Now we can define `extract` as follows:

``````extract x (x':xs) | x == x'    = (0, xs)
| otherwise  = (i + 1, x':xs')
where (i, xs') = extract x xs
``````

One can check that the relation that we are interested in between `insertAt` and `extract` actually holds.

## Generating Permutations

We can now combine `perms` and `indexOf` to give a function `nextPerm` which generates the next permutation in the list `perms n`:

``````fact 0 = 1
fact n = n * fact (n - 1)

nextPerm' n xs = perms n !! ((1 + indexOfPerm n xs) `mod` (fact n))
``````

However, we can rewrite this function by fusing the definition of `perms` with the definition of `indexOfPerm`:

``````-- nextPerm 0 []
--   { Definition of nextPerm }
--   = perms 0 !! ((1 + indexOfPerm 0 []) mod (fact 0))
--   { Definition of indexOfPerm }
--   = perms 0 !! (1 mod 1)
--   { Definition of perms }
--   = []
``````

The recursive case is only slightly more tricky. We divide into two cases.

``````-- nextPerm n xs
--     { Definition of nextPerm }
--     = perms n !! ((1 + indexOfPerm n xs) mod (fact n))
--     { Let (j, xs') = extract n xs }
--     = [ insertAt i n p | p <- perms (n - 1), i <- [0..n- 1] ] !! ((n * (indexOfPerm (n - 1) xs') + j + 1) mod (n * fact (n - 1)))
``````

The value `j` is the index of `n` in `xs`, so that `0 < j < n`. The first case is `j < n - 1`:

``````-- nextPerm n xs
--    { Assume j < n - 1 }
--     = insertAt (j + 1) n (perms (n - 1) !! (indexOfPerm (n - 1) xs'))
--     { By earlier assumption }
--     = insertAt (j + 1) n xs'
``````

The second case is when `j = n - 1`:

``````-- nextPerm n xs
--    { Assume j = n - 1 }
--     = [ insertAt i n p | p <- perms (n - 1), i <- [0..n-1] ] !! ((n * (1 + indexOfPerm (n - 1) xs')) mod (n * fact (n - 1)))
--     { By earlier assumption }
--     = insertAt 0 n (perms (n - 1) !! (1 + indexOfPerm (n - 1) xs'))
--     { Definition of nextPerm }
--     = insertAt 0 n (nextPerm (n - 1) xs')
``````

Thus we arrive at our final definition of `nextPerm`:

``````nextPerm 0 [] = []
nextPerm n xs | j == n - 1  = insertAt 0 n (nextPerm (n - 1) xs')
| otherwise   = insertAt (j + 1) n xs'
where (j, xs') = extract n xs
``````

## A Better Data Structure

The inverse `indexOfPerm` is only a partial function, because `perms n` returns a collection of lists of size `n`. In addition, the types of lists does not enforce the invariant that each element `perms n` is a permutation of `[1..n]`.

Using the `-XPolyKinds` GHC extension, we can express a type of permutations, indexed by size, allowing us to strengthen the type of `nextPerm`, specifying that `nextPerm` preserves the size of a permutation.

The following type definition will be lifted to the kind level, generating two constructors `Z :: Nat` and `S :: Nat -> Nat`

``````data Nat = Z | S Nat
_1 = S Z
_2 = S \$ S Z
_3 = S \$ S \$ S Z
_4 = S \$ S \$ S \$ S Z

showNat :: Nat -> String
showNat n = show (show' n 0) where
show' :: Nat -> Int -> Int
show' Z m = m
show' (S n) m = show' n (m + 1)

instance Show Nat where
show = showNat
``````

The type `Leq n` of natural numbers less than or equal to `n`. The type is parameterised over the kind `Nat`.

``````data Leq :: Nat -> * where
LeqZero :: Leq n
LeqSucc :: Leq n -> Leq (S n)
``````

We can embed numbers less than or equal to `n` into numbers less than or equal to `n + 1` for every `n`:

``````embed :: Leq n -> Leq (S n)
embed LeqZero = LeqZero
embed (LeqSucc n) = LeqSucc (embed n)
``````

We can convert to and from regular integers:

``````leqToInt :: Leq n -> Int
leqToInt LeqZero = 0
leqToInt (LeqSucc n) = 1 + leqToInt n

intToLeq :: Int -> EqNat n -> Leq n
intToLeq 0 n = LeqZero
intToLeq n (EqSucc m) = LeqSucc (intToLeq (n - 1) m)

showLeq :: Leq n -> String
showLeq n = show (show' n 0) where
show' :: Leq n -> Int -> Int
show' LeqZero m = m
show' (LeqSucc n) m = show' n (m + 1)

instance Show (Leq n) where
show = showLeq
``````

The type of natural numbers equal to `n`, that is, a singleton type for each natural number:

``````data EqNat :: Nat -> * where
EqZero :: EqNat Z
EqSucc :: EqNat n -> EqNat (S n)

eq1 = EqSucc EqZero
eq2 = EqSucc \$ EqSucc EqZero
eq3 = EqSucc \$ EqSucc \$ EqSucc EqZero
eq4 = EqSucc \$ EqSucc \$ EqSucc \$ EqSucc EqZero
``````

We can convert the sole inhabitant of each singleton type to its natural number representation:

``````eqToInt :: EqNat n -> Int
eqToInt EqZero = 0
eqToInt (EqSucc n) = 1 + eqToInt n

showEq :: EqNat n -> String
showEq n = show (show' n 0) where
show' :: EqNat n -> Int -> Int
show' EqZero m = m
show' (EqSucc n) m = show' n (m + 1)

instance Show (EqNat n) where
show = showEq
``````

We will need the following helper method, which returns the value of `n` in the type of numbers less than or equal to `n`:

``````maxLeq :: EqNat n -> Leq n
maxLeq EqZero = LeqZero
maxLeq (EqSucc n) = LeqSucc (maxLeq n)
``````

We can turn collect the list of all numbers in `Leq n` recursively:

``````for :: EqNat n -> [Leq n]
for EqZero = [LeqZero]
for (EqSucc n) = LeqZero : map LeqSucc (for n)
``````

Finally, we define the type of permutations, again parameterised by the kind `Nat` and containing two type constructors: the empty permutation and the permutation obtained by inserting the value `n + 1` into a permutation of the list `[1..n]`:

``````data Perm :: Nat -> * where
Empty :: Perm Z
Insert :: Leq n -> Perm n -> Perm (S n)

showPerm :: Perm n -> String
showPerm p = "(" ++ concat (intersperse "," (map show (toList p 0))) ++ ")" where
toList :: Perm n -> Int -> [Int]
toList Empty m = []
toList (Insert n p) m = let (l, r) = splitAt (leqToInt n) (toList p (m + 1)) in l ++ [m] ++ r

instance Show (Perm n) where
show = showPerm
``````

Note now that invalid permutations are no longer inhabitants of the type `Perm n` for any `n`: to insert value `n` into a permutation of `[1..n-1]`, we have to specify a position to insert which is in the range `[0..n]`, and this is enforced by the type `Perm n`! One cannot, for example, represent a list with a duplicate element - the elements are not even mentioned explicitly.

The rank of a permutation is the size of the set it permutes:

``````rank :: Perm n -> EqNat n
rank Empty = EqZero
rank (Insert n p) = EqSucc (rank p)
``````

The identity permutation is easily defined by recursion:

``````identity :: EqNat n -> Perm n
identity EqZero = Empty
identity (EqSucc n) = Insert LeqZero (identity n)
``````

The method `perms` translates easily to this new setting:

``````perms1 :: EqNat n -> [Perm n]
perms1 EqZero = [Empty]
perms1 (EqSucc n) = [ Insert i xs | xs <- perms1 n, i <- for n ]
``````

We can create a permutation from its list representation by repeatedly extracting the highest element:

``````fromList :: EqNat n -> [Int] -> Perm n
fromList EqZero [] = Empty
fromList (EqSucc n) xs = Insert (intToLeq i n) (fromList n (map (flip (-) 1) (delete 0 xs)))
where Just i = elemIndex 0 xs
``````

We can also translate the function `indexOfPerm` without difficulty:

``````indexOfPerm1 :: Perm n -> EqNat n -> Int
indexOfPerm1 Empty EqZero = 0
indexOfPerm1 (Insert n p) (EqSucc m) = (indexOfPerm1 p m) * (1 + eqToInt m) + leqToInt n
``````

The following function emulates the indexing function `perms r !!`, returning the `n`th permutation in the set of permutations of a given rank:

``````nth :: Int -> EqNat n -> Perm n
nth 0 EqZero = Empty
nth m (EqSucc n) = Insert (intToLeq k n) (nth j n)
where (j, k) = divMod m (1 + eqToInt n)
``````

As before, we can combine `nth` with `indexOfPerm1` to step to the next permutation:

``````nextPerm1' :: Perm n -> Perm n
nextPerm1' p = let r = rank p in nth (indexOfPerm1 p r - 1) r
``````

Finally, we can perform the same fusion as before, and express `nextPerm1` directly without the need for helper functions `nth` and `indexOfPerm1`.

``````nextPerm1 :: Perm n -> Perm n
nextPerm1 Empty = Empty
nextPerm1 (Insert LeqZero p) = Insert (maxLeq (rank p)) (nextPerm1 p)
nextPerm1 (Insert (LeqSucc n) p) = Insert (embed n) p
``````

Note here that we have also removed the dependence on the intermediate type `Int`, representing the index of the permutation, and we are left with a type which conveys some valuable information about the function `nextPerm1`:

``````-- nextPerm1 :: forall (n :: Nat). Perm n -> Perm n
``````

That is, `nextPerm1` preserves the rank of its argument.

Compile the source in this post with GHC 7.4 or later.