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.