A take at updating Cryptol's sort function from insertion sort to merge sort

[weaversa]

Here we provide an implementation for sort that is much more computationally efficient than the current one. For example, sorting 3000 Integers takes ~4 seconds where the current implementation takes over a minute.

There are two variations on merging two sorted lists to choose from. They seem similar in terms of runtime and time it takes to prove a property.

[weaversa]

I imagine that one of the two definitions of merge (or perhaps another candidate) would be preferred and moved under the scope of sortBy, removing the private block.

[robdockins]

Are these sorts still stable? I know that was an important design consideration for the first version.

EDIT: some limited testing suggests that these are stable sorts.

[robdockins]

On my machine, I'm seeing that the new sorts take about half the time as the current sort to sort a random [3000]Integer sequence. That's not the 15x speedup you seem to be seeing, though. I'm not sure what makes the difference.

[weaversa]

@robdockins Perhaps you didn't update the recursive calls to sortBy when you pulled out a standalone version to compare? Here's a standalone version:

/**
 * Sort a sequence of elements. Equivalent to 'sortBy (<=)'.
 */

sort' : {a, n} (Cmp a, fin n) => [n]a -> [n]a
sort' = sortBy' (<=)

/**
 * Sort a sequence according to the given less-than-or-equal relation.
 * The sorting is stable, so it preserves the relative position of any
 * pair of elements that are equivalent according to the order relation.
 */
sortBy' : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
sortBy' le ((xs : [n/2]a) # (ys : [n/^2]a)) = merge le xs' ys'
  where
    xs' = if `(n/2)  == 1 then xs else sortBy' le xs
    ys' = if `(n/^2) == 1 then ys else sortBy' le ys

private

  merge : {a, n, m} (fin n, fin m)
   => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a
  merge le xs ys = take zs.0
    where
      zs =
        [ if i == `n          then (ys@j, i  , j+1)
           | j == `m          then (xs@i, i+1, j  )
           | le (xs@i) (ys@j) then (xs@i, i+1, j  )
          else                     (ys@j, i  , j+1)
        | (_, i, j) <- [(undefined, 0, 0)] # zs
        ]

  merge' : {a, n, m} (fin n, fin m)
   => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a
  merge' le xs ys =
      if `n == 0 \/ `m == 0 then xs # ys
       | le (xs@0) (ys@0)
      then drop`{1 - min 1 n} ([xs@0] # merge' le (drop`{min 1 n} xs) ys)
      else drop`{1 - min 1 m} ([ys@0] # merge' le xs (drop`{min 1 m} ys))

[robdockins]

Well guessed, that's exactly what I did. Rookie mistake!

This seems like a great improvement to me. I guess I have a slight preference for merge over merge' based only on the look of it.

[weaversa]

Inlining the merge function seems to have sped things up even more.

[weaversa]

Should I update the failing tests by hand, or is there an automated way to do that?

[robdockins]

No automation for that, unfortunately, other than copy/paste the suggested command line.

[weaversa]

@robdockins The CI passes and I don't envision any more work being done. Is there anything else you (or perhaps @brianhuffman) would like to see before considering a merge?

[robdockins]

I'm happy. Any thoughts @brianhuffman ?

[yav]

Seems reasonable to me. At some point we should really decide on the complexity of @, but probably not in this thread.