Provably correct permutation in less than O(n^2)

Question

Written in Haskell, here is the data type that proves that one list is a permutation of another:

data Belongs (x :: k) (ys :: [k]) (zs :: [k]) where
  BelongsHere :: Belongs x xs (x ': xs)
  BelongsThere :: Belongs x xs xys -> Belongs x (y ': xs) (y ': xys)

data Permutation (xs :: [k]) (ys :: [k]) where
  PermutationEmpty :: Permutation '[] '[]
  PermutationCons :: Belongs x ys xys -> Permutation xs ys -> Permutation (x ': xs) xys

With a Permutation, we can now permute a record:

data Rec :: (u -> *) -> [u] -> * where
  RNil :: Rec f '[]
  (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)

insertRecord :: Belongs x ys zs -> f x -> Rec f ys -> Rec f zs
insertRecord BelongsHere v rs = v :& rs
insertRecord (BelongsThere b) v (r :& rs) = r :& insertRecord b v rs

permute :: Permutation xs ys -> Rec f xs -> Rec f ys
permute PermutationEmpty RNil = RNil
permute (PermutationCons b pnext) (r :& rs) = insertRecord b r (permute pnext rs)

This works fine. However, permute is O(n^2) where n is the length of the record. I'm wondering if there is a way to get it to be any faster by using a different data type to represent a permutation.

For comparison, in a mutable and untyped setting (which I know is a very different setting indeed), we could apply a permutation to a heterogeneous record like this in O(n) time. You represent the record as an array of values and the permutation as an array of new positions (no duplicates are allowed and all digits must be between 0 and n). Applying the permutation is just iterating that array and indexing into the record's array with those positions.

I don't expect that an O(n) permutation is possible in a more rigorously typed settings. But it seems like O(n*log(n)) might be possible. I appreciate any feedback, and let me know if I need to clarify anything. Also, answers to this can use Haskell, Agda, or Idris depending on what it feels easier to communicate with.

Answer 1

A faster simple solution is to compare the sorted permutation of the permutations.

1. Given permutation A and B.

2. Then there exist the sorted permutations,

   As = sort(A) Bs = sort(B)

3. As is a permutation of A and Bs is a permutation of B.

4. If As == Bs then A is a permutation of B.

Thus the order of this algorithm is O(n log(n)) < O(n²)

And this is leading to the optimal solution.

Using a different storage of permutation yields O(n)

Using the statements from above, we are changing the storage format of each permutation into

• the sorted data
• the original unsorted data

To determine if a list is a permutation of another one, simple a comparison of the sorted data is necessary -> O(n).

This answers the question correctly, but the effort is hidden in creating the doubled data storage ^^ So it will depend on the use if this is a real advantage or not.