sorting in monad

Stream: Is there code for X?

[Marcus Rossel]

Is there a way to sort a List or Array with a comparison function of the form α → α → m Bool for some monad m?

[Adam Topaz]

It's easy enough to implement a quicksort:

def List.qsortM [Monad m] (comp : α → α → m Bool) : List α → m (List α )
  | [] => return []
  | x :: xs => do
    let fst ← (xs.filterM fun t => comp t x)
    let lst ← (xs.filterM fun t => comp x t)
    return fst ++ [x] ++ lst

[Adam Topaz]

(this isn't correct if the list has repetitions)

[Eric Wieser]

That's surely just not correct at all as it doesn't recurse?

[Adam Topaz]

oops!

[Adam Topaz]

partial
def List.qsortM [Monad m] (comp : α → α → m Bool) [BEq α] : List α → m (List α )
  | [] => return []
  | x :: xs => do
    let fst ← (xs.filterM fun t => comp t x)
    let lst ← (xs.filterM fun t => return (← comp x t) || x == t)
    return (← fst.qsortM comp) ++ [x] ++ (← lst.qsortM comp)

[Adam Topaz]

okay, I think that last version might actually be correct

[Adam Topaz]

At least the following single test comes up correctly:

#eval List.qsortM (m := IO) (fun a b : Nat => do IO.sleep 1 ; return a < b) [1,45,2,7,1,2]

[Eric Wieser]

I think you probably want a List.partitionM out of that

[Adam Topaz]

I didn't know that exists.

[Adam Topaz]

That's indeed nicer:

partial
def List.qsortM [Monad m] (comp : α → α → m Bool) [BEq α] : List α → m (List α )
  | [] => return []
  | x :: xs => do
    let (fst, lst) ← xs.partitionM fun t => comp t x
    return (← fst.qsortM comp) ++ [x] ++ (← lst.qsortM comp)

#eval List.qsortM (m := IO) (fun a b : Nat => do IO.sleep 1 ; return a < b) [1,45,2,7,1,2]

[Eric Wieser]

Does having something like

@[inline] def partitionM' [Monad m] (p : α → m Bool) (as : List α) :
    m {tf : List α × List α // tf.1 ++ tf.2 ~ as} :=
  return (← loop as ([], [])).map id fun x => by simp
where
  @[specialize] loop : (as : List α) → (acc : List α × List α) →
      m ({tf : List α × List α // tf.1 ++ tf.2 ~ as ++ acc.1 ++ acc.2})
  | [],    (bs, cs) => return ⟨(bs.reverse, cs.reverse), .append (by simp) (by simp)⟩
  | a::as, (bs, cs) => do
    match ← p a with
    | true  => pure <| (← loop as (a::bs, cs)).map id (fun x h => h.trans <| by aesop)
    | false => pure <| (← loop as (bs, a::cs)).map id (fun x h => h.trans <| by
      dsimp
      sorry)

help show termination?

[Eric Wieser]

You can't prove that the partition is lawful, because p might be "flip a coin"; but you could prove it doesn't change the length of the list, which might be enough to terminate

[Eric Wieser]

Yeah, I think that works:

def List.qsortM {α m} [Monad m] (comp : α → α → m Bool) : (l : List α) → m {l' : List α // l' ~ l}
  | [] => return ⟨[], .refl _⟩
  | x :: xs => do
    let ⟨(fst, lst), hp⟩ ← (xs.partitionM' fun t => comp t x)
    have : fst.length ≤ xs.length := sorry
    have : lst.length ≤ xs.length := sorry
    let fst ← fst.qsortM comp
    let lst ← lst.qsortM comp
    return ⟨(fst) ++ [x] ++ (lst), sorry⟩
termination_by xs => xs.length