Enumerating Permutations

perm.lhs

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE PolyKinds #-}

> import Data.List

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

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)

Returns the list of all natural numbers in the type of numbers less than or equal to n

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

The type of permutations is parameterised over the kind Nat and contains 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

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

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

The set of all permutations of a given size

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

Creates a permutation from its list representation

> 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 

Returns the index of a permutation of size n in the list perms n

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

Returns the nth permutation in the set of permutations of rank r, should be equivalent to perms r !!

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

Returns the next permutation in the set of permutations by using indexOf and nth

> nextPerm' :: Perm n -> Perm n
> nextPerm' p = let r = rank p in nth (indexOf p r - 1) r

Returns the next permutation in the set of permutations in amortized constant time by folding nth with indexOf

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