I am reading the code in Base. https://github.com/janestreet/base/blob/master/src/array.ml has
module Insertion_sort : Sort = struct
let sort arr ~compare ~left ~right =
(* loop invariant:
[arr] is sorted from [left] to [pos - 1], inclusive *)
for pos = left + 1 to right do
(* loop invariants:
1. the subarray arr[left .. i-1] is sorted
2. the subarray arr[i+1 .. pos] is sorted and contains only elements > v
3. arr[i] may be thought of as containing v
Note that this does not allocate a closure, but is left in the for
loop for the readability of the documentation. *)
let rec loop arr ~left ~compare i v =
let i_next = i - 1 in
if i_next >= left && compare (get arr i_next) v > 0
then (
set arr i (get arr i_next);
loop arr ~left ~compare i_next v)
else i
in
let v = get arr pos in
let final_pos = loop arr ~left ~compare pos v in
set arr final_pos v
done
;;
end
Questions:
- What does the comment “is left in the loop” refer to?
- What is the advantage to having
let rec loop arr ~left ~compare i v
whenarr
,left
,compare
, andv
are constant? That is, why is the loop not simplylet rec loop i
?