Merge sort on a List<Int> — top-down, purely functional
Demonstrates: splitting a list into halves, recursive sort, and the two-pointer merge of two sorted lists into one. Stable and O(n log n).
A Soma program from the algorithms part of the verified corpus: 64 lines, cells MergeSort, MergeSortTests. It passes soma check with soma 3.2.4.
How it is built
The cell MergeSort declares 2 signals in its face: sort(xs: List) -> List and merge_lists(a: List, b: List) -> List. Handlers: merge_lists (line 16) and sort (line 40).
The file also holds 1 test cell (MergeSortTests) with 8 assertions, run by soma test.
The source
merge_sort.cell
// Merge sort on a List<Int> — top-down, purely functional.
// Demonstrates: splitting a list into halves, recursive sort, and the
// two-pointer merge of two sorted lists into one. Stable and O(n log n).
//
// soma run examples/corpus/algorithms/merge_sort.cell sort "[38,27,43,3,9,82,10]"
// soma test examples/corpus/algorithms/merge_sort.cell
cell MergeSort {
face {
signal sort(xs: List) -> List
signal merge_lists(a: List, b: List) -> List
}
// NOTE: named merge_lists, not merge — `merge` is a builtin (map union)
// that would shadow a handler called from a test cell.
on merge_lists(a: List, b: List) {
let out = list()
let i = 0
let j = 0
while i < len(a) && j < len(b) {
if a[i] <= b[j] {
out = push(out, a[i])
i = i + 1
} else {
out = push(out, b[j])
j = j + 1
}
}
while i < len(a) {
out = push(out, a[i])
i = i + 1
}
while j < len(b) {
out = push(out, b[j])
j = j + 1
}
return out
}
on sort(xs: List) {
let n = len(xs)
if n <= 1 { return xs }
let mid = floor(n / 2)
let left = list()
let right = list()
for i in range(0, mid) { left = push(left, xs[i]) }
for i in range(mid, n) { right = push(right, xs[i]) }
return merge_lists(sort(left), sort(right))
}
}
cell test MergeSortTests {
rules {
assert to_string(sort([38, 27, 43, 3, 9, 82, 10])) == to_string([3, 9, 10, 27, 38, 43, 82])
assert to_string(sort([5, 4, 3, 2, 1])) == to_string([1, 2, 3, 4, 5])
assert to_string(merge_lists([1, 3, 5], [2, 4, 6])) == to_string([1, 2, 3, 4, 5, 6])
assert to_string(sort(list())) == to_string(list())
assert to_string(sort([1])) == to_string([1])
assert len(merge_lists([1, 2], list())) == 2
assert merge_lists([1, 2], list())[0] == 1
assert merge_lists([1, 2], list())[1] == 2
}
}What the toolchain says
$ soma check merge_sort.cell
warning: inside MergeSort.sort, `sort(…)` with 1 argument(s) calls the handler ITSELF (recursion), not the builtin sort() — a handler shadows a builtin of the same name and arity. For an empty list write []
--> merge_sort.cell:48:28
|
48 | return merge_lists(sort(left), sort(right))
| ^
warning: inside MergeSort.sort, `sort(…)` with 1 argument(s) calls the handler ITSELF (recursion), not the builtin sort() — a handler shadows a builtin of the same name and arity. For an empty list write []
--> merge_sort.cell:48:40
|
48 | return merge_lists(sort(left), sort(right))
| ^
✓ 2 warning(s), no errors.$ soma test merge_sort.cell
test MergeSortTests ...
✓ assert to_string(sort([38, 27, 43, 3, 9, 82, 10])) == to_string([3, 9, 10, 27, 38, 43, 82])
✓ assert to_string(sort([5, 4, 3, 2, 1])) == to_string([1, 2, 3, 4, 5])
✓ assert to_string(merge_lists([1, 3, 5], [2, 4, 6])) == to_string([1, 2, 3, 4, 5, 6])
✓ assert to_string(sort(list())) == to_string(list())
✓ assert to_string(sort([1])) == to_string([1])
✓ assert len(merge_lists([1, 2], list())) == 2
✓ assert merge_lists([1, 2], list())[0] == 1
✓ assert merge_lists([1, 2], list())[1] == 2
8 tests: 8 passed, 0 failed$ soma verify merge_sort.cell
Verifying merge_sort.cell...
MergeSort/termination:
⚠ handler `merge_lists`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
⚠ handler `sort`: recursive call without provable decreasing argument
0 passed, 2 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK$ soma run merge_sort.cell sort "[38,27,43,3,9,82,10]"
[3, 9, 10, 27, 38, 43, 82]