title: Provably correct permutation in less than O(n^2)
body: <p>Written in Haskell, here is the data type that proves that one list is a permutation of another:</p>
  
  <pre><code>data Belongs (x :: k) (ys :: [k]) (zs :: [k]) where
    BelongsHere :: Belongs x xs (x ': xs)
    BelongsThere :: Belongs x xs xys -&gt; Belongs x (y ': xs) (y ': xys)
  
  data Permutation (xs :: [k]) (ys :: [k]) where
    PermutationEmpty :: Permutation '[] '[]
    PermutationCons :: Belongs x ys xys -&gt; Permutation xs ys -&gt; Permutation (x ': xs) xys
  </code></pre>
  
  <p>With a <code>Permutation</code>, we can now permute a record:</p>
  
  <pre><code>data Rec :: (u -&gt; *) -&gt; [u] -&gt; * where
    RNil :: Rec f '[]
    (:&amp;) :: !(f r) -&gt; !(Rec f rs) -&gt; Rec f (r ': rs)
  
  insertRecord :: Belongs x ys zs -&gt; f x -&gt; Rec f ys -&gt; Rec f zs
  insertRecord BelongsHere v rs = v :&amp; rs
  insertRecord (BelongsThere b) v (r :&amp; rs) = r :&amp; insertRecord b v rs
  
  permute :: Permutation xs ys -&gt; Rec f xs -&gt; Rec f ys
  permute PermutationEmpty RNil = RNil
  permute (PermutationCons b pnext) (r :&amp; rs) = insertRecord b r (permute pnext rs)
  </code></pre>
  
  <p>This works fine. However, permute is <code>O(n^2)</code> where <code>n</code> 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.</p>
  
  <p>For comparison, in a mutable and untyped setting (which I know is a <strong>very</strong> different setting indeed), we could apply a permutation to a heterogeneous record like this in <code>O(n)</code> 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.</p>
  
  <p>I don't expect that an <code>O(n)</code> permutation is possible in a more rigorously typed settings. But it seems like <code>O(n*log(n))</code> 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.</p>