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 nth 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.