RFC: Generalize Array.binSearch with partition-point-style API

Proposal

The "partition point" in the title comes from Rust's slice.partition_point. In short, given a unary boolean predicate f, this function finds the first index i in an array as where f(as[0]), ..., f(as[i-1]) are true and f(as[i]), ... are false.

This is best expressed by the following signature:

def partitionPoint {n : Nat} (f : Fin n -> Bool) : Fin (n + 1)

This function can act as a building block for implementing binSearch, but it is also useful for other uses involving (parametric) binary search as well, such as implementing mathematical functions, say Nat.isqrt.

Also, as far as I can tell, the current binSearch does not specify which element is chosen if multiple items in as are equal. A partitionPoint-based implementation guarantees that the leftmost one will be chosen.

Proposed APIs:

def partitionPoint {n : Nat} (f : Fin n → Bool) : Fin (n + 1)
def Vector.partitionPoint {α : Type u} {n : Nat} (vec : Vector α n) (pred : α → Bool) : Fin (n + 1)
def Array.partitionPoint {α : Type u} (as : Array α) (pred : α → Bool) : Fin (as.size + 1)
-- reimplementations of five functions in Init.Data.Array.BinSearch
def Nat.partitionPoint (pred : Nat → Bool) (lo : Nat) (hi : Nat) : Nat
def Int.partitionPoint (pred : Int → Bool) (lo : Int) (hi : Int) : Int

example implementation.

Community Feedback

Zulip thread

Start with Init.Data.Array.BinSearch and the linked example implementation. Compare the current binSearch behavior with the proposed partitionPoint APIs, including duplicate handling and the Nat and Int variants. Done means the API design is agreed and the required generalizations are implemented consistently.