Quickselect in Unison

quickselect.u

{{
  ``List.selectBy o k as`` yields the same results as ``List.at k sorted`` 
  where ''sorted'' is a sorted version of ''as'', but in (expected) linear time
  without fully sorting the list.

  ```
  List.selectBy Universal.ordering 2 [4,1,3,2,5]
  ```

  ```
  List.selectBy Universal.ordering 2 [1,2,5,4,3]
  ```

  This implementation has quadratic performance if the list is already sorted.
}}
List.selectBy : (a -> a -> Ordering) -> Nat -> [a] -> Optional a 
List.selectBy o n = cases
  [] -> None 
  (pivot +: as) ->
    as' = List.filter (a -> Ordering.ltBy o a pivot) as 
    match List.size as' with
      s | s == n    -> Some pivot
        | s < n     -> List.selectBy o (Nat.drop n (s+1)) (List.drop s as) 
        | otherwise -> List.selectBy o n as'