> Here's an insertion sort that I believe to be stable:

[weaversa]

Here's an insertion sort that I believe to be stable:

sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
sortBy le xs =
  if `n == (0 : Integer) then xs
  else drop`{1 - min 1 n} (insertBy le (xs@0) (sortBy le (drop`{min 1 n} xs)))

insertBy : {a, n} (fin n) => (a -> a -> Bit) -> a -> [n]a -> [n+1]a
insertBy le x0 ys = xys.0 # [last xs]
  where
    xs : [n+1]a
    xs = [x0] # xys.1
    xys : [n](a, a)
    xys = [ if le x y then (x, y) else (y, x) | x <- xs | y <- ys ]

The implementation would be a bit nicer if we implemented #701.

Should we add basically this implementation to the Prelude and later consider the question of making it a primitive?

Originally posted by @robdockins in #1032 (comment)

[weaversa]

How about adding this to the prelude?

[robdockins]

I'm in favor.

[brianhuffman]

I'll make a PR for it. I'll also add some tests that check that it is in fact a stable sort.

[yav]

Should we perhaps put it in another module? The Prelude is getting very large...

[brianhuffman]

Sorting seems like a pretty basic sequence operation that belongs in the same module as other basic sequence operations like reverse and transpose.

If you think the number of prelude functions is getting too big, there are some other collections of specialist functions that I think would make sense to be grouped separately: the GF(2) polynomial operations (pmult, pdiv, and pmod) or our collection of higher-order functions like maps, folds, scans, etc, which used to be in their own separate module.

But really I don't think there's much of a drawback in having a big prelude, other than maybe :browse output getting a bit long.

If we're going to start putting a bunch of stuff in separate modules, then we are going to need to do a better job of making that stuff more discoverable and easier to use. Right now, if you want to use a function from one of our extra modules like Float or Array, you can use :m Float or :m Array to get easy access to those functions at the REPL. But if you want to use functions from both of those modules at once, :m Float Array just gives you an Invalid module name error message. If we moved sort into a separate module, then you wouldn't be able to sort a list of floats at the REPL without creating a new cryptol module in a file, which is rather a pain.